proposition: Lemma pinsker_fun_pos c : 0 <= c <= / (2 * ln 2) -> 0 <= pinsker_fun (Prob.p p) c (Prob.p q).
proof: Proof. move=> Hc. set a := Set2.a card_A. set b := Set2.b card_A. have [p0|p0] := eqVneq p 0%:pr. subst p. rewrite /pinsker_fun /div_fct /comp. rewrite !(mul0R,mulR0,addR0,add0R,Rminus_0_l,subR0). have [q1|q1] := eqVneq q 1%:pr. subst q. exfalso. move/dominatesP : P_dom_by_Q => /(_ a). by rewrite !fdist_binaryE !/onem subrr eqxx subr0 -R1E -R0E; lra. apply: leR_trans. apply: (@pinsker_function_spec_pos _ (Prob.p q) Hc); split=> //. by apply/RltP; rewrite -prob_lt1. rewrite /pinsker_function_spec. apply: Req_le. by rewrite mul1R div1R /log LogV; [field| rewrite subR_gt0; apply /RltP; rewrite -prob_lt1]. have [p1|p1] := eqVneq p 1%:pr. subst p. rewrite /pinsker_fun /div_fct /comp subRR mul0R addR0. have [q0|q0] := eqVneq q 0%:pr. subst q. exfalso. move/dominatesP : P_dom_by_Q => /(_ b). rewrite !fdist_binaryE /onem subrr eq_sym (negbTE (Set2.a_neq_b card_A)) /=. by move=> /(_ erefl)/eqP; rewrite oner_eq0. apply: leR_trans. have : 0 <= 1 - Prob.p q < 1. split; first by rewrite subR_ge0. by rewrite ltR_subl_addr -{1}(addR0 1) ltR_add2l; apply/RltP/ prob_gt0. exact: pinsker_function_spec_pos Hc. rewrite /pinsker_function_spec. apply Req_le. rewrite mul1R div1R /log LogV; [|by apply/RltP/prob_gt0]. rewrite /id (_ : 1 - (1 - Prob.p q) = Prob.p q) //; by field. have [q0|q0] := eqVneq q 0%:pr. subst q. rewrite /pinsker_fun /div_fct /comp. exfalso. move/dominatesP : P_dom_by_Q => /(_ b). rewrite !fdist_binaryE eq_sym (negbTE (Set2.a_neq_b card_A)) => /(_ erefl) p0_. by move/eqP : p0; apply; apply/val_inj; rewrite /= p0_. have [q1|q1] := eqVneq q 1%:pr. subst q. exfalso. move/dominatesP : P_dom_by_Q => /(_ a). rewrite !fdist_binaryE /onem subrr eqxx subR_eq0 => /(_ erefl) p1_. by move/eqP : p1; apply; apply/val_inj; rewrite /= -p1_. rewrite -(pinsker_fun_p p c). case: (Rlt_le_dec (Prob.p q) (Prob.p p)) => qp. apply pinsker_fun_decreasing_on_0_to_p => //. - lra. - by split; apply/RltP; [rewrite -prob_gt0 | rewrite -prob_lt1]. - by split; [apply/RltP/prob_gt0 | exact/ltRW]. - split; [by apply/RltP/prob_gt0 | ]. by apply/RleP; rewrite lexx. - exact/ltRW. apply pinsker_fun_increasing_on_p_to_1 => //. - lra. - by split; apply/RltP; [rewrite -prob_gt0 |rewrite -prob_lt1]. - by split; [by apply/RleP; rewrite lexx |apply/RltP/prob_lt1]. - by split => //; apply/RltP; rewrite -prob_lt1. 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