proposition: Lemma pinsker_fun_increasing_on_0_to_1 (c : R) (Hc : c <= / (2 * ln 2)) : forall x y, 0 <= x < 1 -> 0 <= y < 1 -> x <= y -> pinsker_function_spec c x <= pinsker_function_spec c y.
proof: Proof. apply pderive_increasing_closed_open with (pderivable_pinsker_function_spec c). lra. move=> t Ht. rewrite derive_pt_pinsker_function_spec // /pinsker_function_spec'. apply (@leR_trans (/ ((1 - t) * ln 2) - 8 * t / (2 * ln 2))); last first. apply leR_add2l. rewrite leR_oppr oppRK -mulRA /Rdiv -[X in _ <= X]mulRA -/(Rdiv _ _). apply leR_wpmul2l; first lra. rewrite mulRC; apply leR_wpmul2l => //. by case: Ht. apply (@leR_trans ((2 - 8 * t * (1 - t)) / (2 * (1 - t) * ln 2))); last first. apply Req_le. field. split; [exact/eqP/ln2_neq0 | case: Ht => ? ? ?; lra]. apply divR_ge0; last first. rewrite mulRC mulRA. apply mulR_gt0. apply mulR_gt0 => //; lra. case: Ht => ? ?; lra. have H2 : -2 <= - 8 * t * (1 - t). rewrite !mulNR -mulRA. rewrite leR_oppr oppRK [X in _ <= X](_ : 2 = 8 * / 4); last by field. apply leR_wpmul2l; [lra | exact: x_x2_max]. move: H2 => /RleP; rewrite -mulRA RmultE mulNr lerNl opprK. by move=> /RleP; rewrite -!RmultE mulRA subR_ge0. 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