proposition: Lemma pinsker_fun_p_eq c : pinsker_fun (Prob.p p) c (Prob.p q) = D(P || Q) - c * d(P , Q) ^ 2.
proof: Proof. pose a := Set2.a card_A. pose b := Set2.b card_A. set pi := P a. set pj := P b. set qi := Q a. set qj := Q b. have Hpi : pi = 1 - Prob.p p by rewrite /pi /P fdist_binaryxx. have Hqi : qi = 1 - Prob.p q by rewrite /qi /= fdist_binaryxx. have Hpj : pj = Prob.p p. by rewrite /pj /= fdist_binaryE eq_sym (negbTE (Set2.a_neq_b card_A)). have Hqj : qj = Prob.p q. by rewrite /qj /= fdist_binaryE eq_sym (negbTE (Set2.a_neq_b card_A)). transitivity (D(P || Q) - c * (`| Prob.p p - Prob.p q | + `| (1 - Prob.p p) - (1 - Prob.p q) |) ^ 2). rewrite /pinsker_fun /div Set2sumE -/a -/b -/pi -/pj -/qi -/qj Hpi Hpj Hqi Hqj. set tmp := (`| _ | + _) ^ 2. have -> : tmp = 4 * (Prob.p p - Prob.p q) ^ 2. rewrite /tmp (_ : 1 - Prob.p p - (1 - Prob.p q) = Prob.p q - Prob.p p); last by field. rewrite sqrRD (distRC (Prob.p q) (Prob.p p)) -mulRA -{3}(pow_1 `| Prob.p p - Prob.p q |). rewrite -expRS sqR_norm; ring. rewrite [X in _ = _ + _ - X]mulRA. rewrite [in X in _ = _ + _ - X](mulRC c). congr (_ - _). case/boolP : (p == 0%:pr) => [/eqP |] p0. rewrite p0 !mul0R subR0 addR0 add0R !mul1R /log /Rdiv. have [q1|q1] := eqVneq q 1%:pr. move/dominatesP : P_dom_by_Q => /(_ (Set2.a card_A)). rewrite -/pi -/qi Hqi q1 subRR => /(_ erefl). by rewrite Hpi p0 subR0 -R0E => ?; exfalso; lra. rewrite /log LogM; last 2 first. lra. by apply/invR_gt0; rewrite subR_gt0; apply/RltP/prob_lt1. rewrite LogV; last by apply/subR_gt0/RltP/prob_lt1. by rewrite Log_1. have [q0|q0] := eqVneq q 0%:pr. move/dominatesP : P_dom_by_Q => /(_ (Set2.b card_A)). rewrite -/pj -/qj Hqj q0 => /(_ erefl). rewrite Hpj => abs. have : p == 0%:pr by apply/eqP/val_inj. by rewrite (negbTE p0). rewrite /div_fct /comp /= (_ : id (Prob.p q) = Prob.p q) //. have [->|p1] := eqVneq p 1%:pr. rewrite subRR !mul0R /Rdiv /log LogM //; last first. apply/invR_gt0; by apply/RltP/prob_gt0. rewrite Log_1 /= mul1R LogV //; last by apply/RltP/prob_gt0. by rewrite !(add0R,mul1R,addR0,sub0R). rewrite /log LogM //; last 2 first. by apply/RltP/prob_gt0. by apply/invR_gt0/RltP/prob_gt0. rewrite LogV //; last by apply/RltP/prob_gt0. have [q1|q1] := eqVneq q 1%:pr. move/dominatesP : P_dom_by_Q => /(_ (Set2.a card_A)). rewrite -/pi -/qi Hqi q1 subRR => /(_ erefl). rewrite Hpi subR_eq0 => abs. have : p == 1%:pr by apply/eqP/val_inj. by rewrite (negbTE p1). rewrite /Rdiv LogM ?subR_gt0 //; last 2 first. by apply/RltP/prob_lt1. by apply/invR_gt0; rewrite subR_gt0; apply/RltP/prob_lt1. rewrite LogV; last by rewrite subR_gt0; apply/RltP/prob_lt1. ring. congr (_ - _ * _). by rewrite /var_dist Set2sumE // -/pi -/pj -/qi -/qj Hpi Hpj Hqi Hqj addRC. 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