proposition: Lemma derive_pt_pinsker_function_spec c q0 (Hq0 : 0 <= q0 < 1) (pr : derivable_pt (pinsker_function_spec c) q0) : derive_pt (pinsker_function_spec c) q0 pr = pinsker_function_spec' c q0.
proof: Proof. rewrite (proof_derive_irrelevance _ (pderivable_pinsker_function_spec c Hq0)) //. rewrite /pinsker_function_spec. rewrite derive_pt_minus. rewrite derive_pt_opp. rewrite derive_pt_comp. rewrite derive_pt_Log. rewrite derive_pt_mult. rewrite derive_pt_pow. rewrite derive_pt_const. rewrite mul0R add0R /= /pinsker_function_spec' (_ : INR 2 = 2) //. field. split; [exact/eqP/ln2_neq0|case: Hq0 => ? ? ?; 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