proposition: Lemma Pinsker_inequality_weak : d(P , Q) <= sqrt (2 * D(P || Q)).
proof: Proof. rewrite -(sqrt_Rsqr (d(P , Q))); last exact/pos_var_dist. apply sqrt_le_1_alt. apply (@leR_pmul2l (/ 2)); first by apply invR_gt0; lra. apply (@leR_trans (D(P || Q))); last first. rewrite mulRA mulVR // ?mul1R; [| exact/gtR_eqF]. by apply/RleP; rewrite lexx. apply: (leR_trans _ Pinsker_inequality). rewrite (_ : forall x, Rsqr x = x ^ 2); last first. by move=> ?; rewrite /Rsqr /pow mulR1. apply leR_wpmul2r; first exact: pow_even_ge0. apply leR_inv => //; first exact/mulR_gt0. rewrite -[X in _ <= X]mulR1. apply leR_wpmul2l; first lra. rewrite [X in _ <= X](_ : 1%R = ln (exp 1)); last by rewrite ln_exp. by apply ln_increasing_le; [lra | exact leR2e]. 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