proposition: Lemma derive_pinsker_fun (p : R) c : 0 < p < 1 -> pderivable (pinsker_fun p c) (fun q => 0 < q < 1).
proof: Proof. move=> [H0p Hp1] q /= [Hq1 Hq2]. rewrite /pinsker_fun. apply: derivable_pt_minus. apply derivable_pt_plus. apply derivable_pt_mult. exact: derivable_pt_const. apply derivable_pt_comp. apply derivable_pt_mult. apply derivable_pt_const. apply derivable_pt_inv. exact/eqP/gtR_eqF. apply derivable_pt_id. apply derivable_pt_Log. exact: divR_gt0. apply derivable_pt_mult. exact: derivable_pt_const. apply derivable_pt_comp. apply derivable_pt_div. apply derivable_pt_const. apply derivable_pt_Rminus. move=> abs; lra. apply derivable_pt_Log. by apply divR_gt0 => //; lra. apply derivable_pt_mult. exact: derivable_pt_const. by apply: derivable_pt_comp; [exact: derivable_pt_Rminus|exact: derivable_pt_pow]. 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