proposition: Lemma pinsker_fun_pderivable1 c (Hp' : 0 < Prob.p p < 1) : pderivable (fun x => - pinsker_fun (Prob.p p) c x) (fun q => 0 < q <= Prob.p p).
proof: Proof. move=> x [Hx1 Hx2]. apply derivable_pt_opp. apply: (@derive_pinsker_fun _ c Hp'). case: Hp' => Hp'1 Hp'2. split => //. lra. Defined.
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