proposition: Lemma pinsker_fun_increasing_on_p_to_1 (c : R) (Hc : c <= / (2 * ln 2)) (p01 : 0 < Prob.p p < 1) : forall x y, Prob.p p <= x < 1 -> Prob.p p <= y < 1 -> x <= y -> pinsker_fun (Prob.p p) c x <= pinsker_fun (Prob.p p) c y.
proof: Proof. apply pderive_increasing_closed_open with (pinsker_fun_pderivable2 c p01). by case: p01. move=> t [pt t1]. rewrite /pinsker_fun_pderivable2. rewrite derive_pt_pinsker_fun //; last lra. rewrite /pinsker_fun' /div_fct. have X : 0 <= (/ (t * (1 - t) * ln 2) - 8 * c). have : forall a b, b <= a -> 0 <= a - b by move=> *; lra. apply. have Hlocal : 0 <= / ln 2 by exact/invR_ge0. have /eqP Hlocal2 : t * (1 - t) <> 0 by apply/eqP/gtR_eqF/mulR_gt0; lra. apply (@leR_trans (4 / ln 2)). apply (@leR_trans (8 * / (2 * ln 2))). apply/RleP. rewrite 2!RmultE ler_pM2l//; last first. by apply/RltP; rewrite (_ : 0%mcR = 0)//; lra. exact/RleP. rewrite invRM ?mulRA; last 2 first. exact/eqP. exact/ln2_neq0. by apply leR_wpmul2r => //; lra. rewrite invRM //; last exact/ln2_neq0. apply leR_wpmul2r => //. rewrite -(invRK 4) //=. apply leR_inv => //. by apply/mulR_gt0; lra. exact: x_x2_max. rewrite /inv_fct; 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