proposition: Lemma derive_pt_pinsker_fun p (Hp : 0 < p < 1) c q (Hq : 0 < q < 1) (pr : derivable_pt (pinsker_fun p c) q) : derive_pt (pinsker_fun p c) q pr = pinsker_fun' p c q.
proof: Proof. transitivity (derive_pt (pinsker_fun p c) q (@derive_pinsker_fun _ c Hp q Hq)). by apply proof_derive_irrelevance. rewrite /pinsker_fun /derive_pinsker_fun. case: Hp => Hp1 Hp2. case: Hq => Hq1 Hq2. rewrite !(derive_pt_minus,derive_pt_plus,derive_pt_comp,derive_pt_ln, derive_pt_const,derive_pt_mult,derive_pt_inv,derive_pt_id,derive_pt_div, derive_pt_pow). rewrite !(mul0R,mulR0,addR0,add0R,Rminus_0_l) /= (_ : INR 2 = 2) //. rewrite /pinsker_fun' /div_fct [X in _ = X]mulRBr. f_equal; last by field. rewrite (_ : id q = q)// 2!Rinv_div. have -> : p * (/ ln 2 * (q / p) * (p * (-1 / q²))) = - (p / q) * / ln 2. rewrite !mulRA /Rsqr. field. split; [exact/eqP/ln2_neq0 | split => ?; lra]. have -> : (1 - p) * (/ ln 2 * ((1 - q) / (1 - p)) * (- (-1 * (1 - p)) / (1 - q)²)) = (((1 - p) / (1 - q))) * / ln 2. rewrite /Rsqr. field. split; [exact/eqP/ln2_neq0 | split => ?; lra]. rewrite /inv_fct. field. by split; [exact/eqP/ln2_neq0 | split => ?; lra]. 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