proposition: Lemma Pinsker_2_inequality : / (2 * ln 2) * d(P , Q) ^ 2 <= D(P || Q).
proof: Proof. move: (charac_bdist P card_A) => [r1 Hp]. move: (charac_bdist Q card_A) => [r2 Hq]. rewrite Hp Hq. apply Pinsker_2_inequality_bdist. by rewrite -Hp -Hq. 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