proposition: Lemma pderivable_pinsker_function_spec c : pderivable (pinsker_function_spec c) (fun q => 0 <= q < 1).
proof: Proof. move=> q0 Hq0. rewrite /pinsker_function_spec. apply derivable_pt_minus. apply derivable_pt_opp. apply derivable_pt_comp. apply derivable_pt_Rminus. apply derivable_pt_Log. rewrite /= in Hq0. decompose [and] Hq0; clear Hq0; lra. by apply: derivable_pt_mult; [exact: derivable_pt_const|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