proposition: Lemma Pinsker_2_inequality_bdist : / (2 * ln 2) * d(P , Q) ^ 2 <= D(P || Q).
proof: Proof. set lhs := _ * _. set rhs := D(_ || _). rewrite -subR_ge0 -pinsker_fun_p_eq. apply pinsker_fun_pos with A card_A => //. by split; [exact/invR_ge0/mulR_gt0 | by apply/RleP; rewrite lexx]. 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