proposition: Lemma lb_entro_plus_eps : IZR (L_typ n' P epsilon') + 1 + epsilon' * (IZR (L_not_typ X n') + 1) < (`H P + epsilon) * INR n.
proof: Proof. move : (fdist_supp_lg_add_1_neq_0 P) => ?. rewrite /L_typ /L_not_typ. apply: (Rle_lt_trans _ (INR n'.+1 * (`H P + epsilon') + 1 + 1 + epsilon' * (log (INR #|[set: (n'.+1).-tuple X]|) + 1 + 1))). - apply: Rplus_le_compat. + by apply: Rplus_le_compat; [apply: ltRW; apply: (proj2 (ceilP _)) | apply: Rle_refl]. + apply: Rmult_le_compat_l; first by apply: Rlt_le; apply: eps'_pos. by apply: Rplus_le_compat; [apply: ltRW; apply: (proj2 (ceilP _)) | apply: Rle_refl]. - rewrite cardsT card_tuple log_pow_INR; last by apply: fdist_card_neq0; exact: P. rewrite -addRA -addRA -addRA addRC addRA addRC addRA -(Rinv_r_simpl_l (INR n) (1 + 1)); last first. by apply/eqP; rewrite INR_eq0'. rewrite (mulRC 2 _) -{1}mulRA -mulRDr -mulRA -mulRDr (mulRC epsilon' _) -mulRA. rewrite (mulRC _ epsilon') -mulRDr mulRC. apply: Rmult_lt_compat_r; first by apply: lt_0_INR; apply/ltP. rewrite -addRA -addRA; apply: Rplus_lt_compat_l. rewrite mulRDr (addRC (epsilon' * log (INR #|X|)) _) addRC addRA -addRA (addRC _ epsilon') -{2}(mulR1 epsilon') -mulRDr -addRA (addRC (epsilon' * (2 / INR n)) _) addRA addRC mulRC addRC /epsilon' -{1}(mulR1 3) -{3}(mulR1 3) -mulRDr /Rdiv {1}Rinv_mult // mulRA -mulRA -Rinv_l_sym // mulR1. apply: (Rle_lt_trans _ (epsilon / 4 + epsilon * / 3 + epsilon / 3)). * apply: Rplus_le_compat. - by apply: Rplus_le_compat; [apply: ltRW; apply: n0_eps4 | apply: Rle_refl]. - by rewrite mulRC /Rdiv (mulRC 2 _) mulRA mulRC mulRA; apply: ltRW; apply: n0_eps3. * rewrite /Rdiv -?mulRDr -{2}(mulR1 epsilon); apply: (Rmult_lt_compat_l _ _ _ eps_pos). by apply: elevenOverTwelve_le_One. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq natbin source_code