proposition: Lemma pinsker_fun_decreasing_on_0_to_p (c : R) (Hc : c <= / (2 * ln 2)) (p01 : 0 < Prob.p p < 1) : forall x y, 0 < x <= Prob.p p -> 0 < y <= Prob.p p -> x <= y -> pinsker_fun (Prob.p p) c y <= pinsker_fun (Prob.p p) c x.
proof: Proof. move=> x y Hx Hy xy. rewrite -[X in _ <= X]oppRK leR_oppr. move: x y Hx Hy xy. apply pderive_increasing_open_closed with (pinsker_fun_pderivable1 c p01). by case: p01. move=> t [t0 tp]. rewrite /pinsker_fun_pderivable1. rewrite derive_pt_opp. rewrite derive_pt_pinsker_fun //; last lra. rewrite /pinsker_fun' /div_fct. have Hlocal : 0 <= / ln 2 by exact/invR_ge0. have X : 0 <= (/ (t * (1 - t) * ln 2) - 8 * c). rewrite subR_ge0; apply (@leR_trans (4 / ln 2)). apply (@leR_trans (8 * / (2 * ln 2))). apply leR_wpmul2l => //; lra. rewrite invRM; last 2 first. by apply/eqP. exact/ln2_neq0. rewrite mulRA; apply leR_wpmul2r => //; lra. rewrite invRM; last 2 first. by apply/gtR_eqF/mulR_gt0; lra. exact/ln2_neq0. apply leR_wpmul2r => //. rewrite -(invRK 4). apply leR_inv => //. by apply/mulR_gt0 => //; lra. exact: x_x2_max. by rewrite /inv_fct -mulNR; apply mulR_ge0 => //; lra. 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