proposition: Lemma Pinsker_inequality : / (2 * ln 2) * d(P , Q) ^ 2 <= D(P || Q).
proof: Proof. pose A0 := [set a | (Q a <= P a)%mcR]. pose A1 := [set a | (P a < Q a)%mcR]. pose A_ := fun b => match b with 0 => A0 | 1 => A1 end. have cov : A_ 0 :|: A_ 1 = setT. rewrite /= /A0 /A1. have -> : [set x | (P x < Q x)%mcR] = ~: [set x | (Q x <= P x)%mcR]. by apply/setP => a; rewrite in_set in_setC in_set ltNge. by rewrite setUCr. have dis : A_ 0 :&: A_ 1 = set0. rewrite /A_ /A0 /A1. have -> : [set x | (P x < Q x)%mcR] = ~: [set x | (Q x <= P x)%mcR]. by apply/setP => a; rewrite in_set in_setC in_set ltNge. by rewrite setICr. pose P_A := bipart dis cov P. pose Q_A := bipart dis cov Q. have step1 : D(P_A || Q_A) <= D(P || Q). by apply partition_inequality; exact P_dom_by_Q. suff : / (2 * ln 2) * d(P , Q) ^2 <= D(P_A || Q_A). move=> ?; apply (@leR_trans (D(P_A || Q_A))) => //; exact/Rge_le. have -> : d( P , Q ) = d( P_A , Q_A ). rewrite /var_dist. transitivity (\sum_(a | a \in A0) `| P a - Q a | + \sum_(a | a \in A1) `| P a - Q a |). rewrite -big_union //; last by rewrite -setI_eq0 -dis /A_ setIC. apply eq_bigl => a; by rewrite cov in_set. transitivity (`| P_A 0 - Q_A 0 | + `| P_A 1 - Q_A 1 |). congr (_ + _). - rewrite /P_A /Q_A /bipart /= /bipart_pmf /=. transitivity (\sum_(a | a \in A0) (P a - Q a)). apply: eq_bigr => a; rewrite /A0 in_set => /RleP Ha. by rewrite geR0_norm ?subR_ge0. rewrite big_split /= geR0_norm; last first. rewrite subR_ge0; rewrite !ffunE. by apply leR_sumR => ?; rewrite inE => /RleP. by rewrite -big_morph_oppR // 2!ffunE addR_opp. - rewrite /P_A /Q_A /bipart /= !ffunE /=. have [A1_card | A1_card] : #|A1| = O \/ (0 < #|A1|)%nat. destruct (#|A1|); [tauto | by right]. + move/eqP : A1_card; rewrite cards_eq0; move/eqP => A1_card. by rewrite A1_card !big_set0 subRR normR0. + transitivity (\sum_(a | a \in A1) - (P a - Q a)). apply eq_bigr => a; rewrite /A1 in_set => Ha. by rewrite ltR0_norm // subR_lt0; exact/RltP. rewrite -big_morph_oppR // big_split /= ltR0_norm; last first. rewrite subR_lt0; apply ltR_sumR_support => // a. by rewrite /A1 in_set => /RltP. by rewrite -big_morph_oppR. by rewrite big_bool /= /bipart_pmf !ffunE /=. exact/(Pinsker_2_inequality card_bool)/bipart_dominates. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals Lra mathcomp(mathcomp_extra Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext logb ln_facts bigop_ext convex fdist divergence variation_dist partition_inequality