proposition: Lemma pinsker_fun_p c : pinsker_fun (Prob.p p) c (Prob.p p) = 0.
proof: Proof. rewrite /pinsker_fun /= /div_fct /comp subRR mul0R mulR0 subR0. have [->|p0] := eqVneq p 0%:pr. by rewrite mul0R !subR0 add0R mul1R div1R invR1 /log Log_1. have [->|p1] := eqVneq p 1%:pr. by rewrite divR1 /log Log_1 subRR mul0R mulR0 addR0. rewrite divRR; last by rewrite subR_eq0' eq_sym. by rewrite /log Log_1 divRR // /log Log_1; field. 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