proposition: Lemma axbary : ax_bary T.
proof: Proof. move=> n m d e g. set f : 'I_n * 'I_m -> 'I_#|[finType of 'I_n * 'I_m]| := enum_rank. set f' : 'I_#|[finType of 'I_n * 'I_m]| -> 'I_n * 'I_m := enum_val. set h := fun k i => f (k, i). set h' := fun i => snd (f' i). rewrite (_ : (fun i => _) = (fun i => <&>_(fdistmap (h i) (e i)) (g \o h'))); last first. apply funext => i. have {1}-> : g = (g \o h') \o h i. apply funext => j; by rewrite /h' /h /= /f' /f enum_rankK. rewrite axinjmap //. by move=> x y; rewrite /h => /enum_rank_inj []. rewrite axbarypart; first last. - move=> i j ij. apply/setP => x; rewrite !inE !fdistE. case/boolP: (i == (f' x).1) ij => [/eqP ->|] ij. rewrite [in X in _ && X]big_pred0 ?eqxx ?andbF //. move=> k; apply/eqP => hjk. move: ij; by rewrite -hjk /h /f /f' enum_rankK eqxx. rewrite big_pred0 ?eqxx //. move=> k; apply/eqP => hik. by move: ij; rewrite -hik /h /f /f' enum_rankK eqxx. set e' := fun j => fdistmap f (((fdistX (d `X e)) `(| j)) `x (fdist1 j)). have {2}-> : g = (fun j => <&>_(e' j) (g \o h')). apply funext => j; apply/esym/axidem => k //. rewrite inE /e' fdistE (big_pred1 (f' k)) /=; last first. by move=> i; rewrite 2!inE -{1}(enum_valK k) /f (can_eq enum_rankK). rewrite !fdistE. by have [<-//f'kj|] := eqVneq _ j; rewrite mulr0 eqxx. rewrite [RHS]axbarypart; last first. move=> i j ij; apply/setP => x. rewrite inE [RHS]inE. case/boolP: (_ \in _) => kx //. case/boolP: (_ \in _) => ky //. rewrite !(inE,fdistE) /= in kx ky *. rewrite (big_pred1 (f' x)) in kx; last first. by move=> a; rewrite -{1}(enum_valK x) !inE (can_eq enum_rankK) eq_sym. rewrite (big_pred1 (f' x)) in ky; last first. by move=> a; rewrite -{1}(enum_valK x) !inE (can_eq enum_rankK) eq_sym. move: kx ky; rewrite !fdistE. case/boolP: ((f' x).2 == i) ij => [/eqP <-|] ij; last by rewrite mulr0 eqxx. by case/boolP: ((f' x).2 == j) ij => [/eqP <-|] //; rewrite mulr0 eqxx. congr (<&>_ _ _); apply fdist_ext => k. rewrite /d1 !fdistE. under eq_bigr do rewrite fdistE big_distrr big_mkcond /=. rewrite exchange_big /=; apply eq_bigr => j _. rewrite !fdistE -big_mkcond /=. rewrite (big_pred1 (f' k)); last by move=> a; rewrite !inE -{1}(enum_valK k) /f (can_eq enum_rankK). set p := f' k => /=. have [->|Hj] := eqVneq j p.2; last first. rewrite big_pred0; first last. move=> i; apply/negbTE; apply: contra Hj. rewrite !inE -(enum_valK k) (can_eq enum_rankK). by rewrite (surjective_pairing (enum_val k)) => /eqP [] _ /eqP. by rewrite !fdistE eq_sym (negbTE Hj) !mulr0. rewrite (big_pred1 p.1) /=; last first. move=> i; rewrite !inE -(enum_valK k) (can_eq enum_rankK). by rewrite (surjective_pairing (enum_val k)) xpair_eqE eqxx andbT. have [Hp|Hp] := eqVneq (\sum_(i < n) d i * e i p.2)%R 0%R. rewrite Hp mul0r -RmultE. by move/psumr_eq0P : Hp => ->//= i _; rewrite RmultE mulr_ge0. rewrite [RHS]mulRC !fdistE jfdist_condE !fdistE /=; last first. by under eq_bigr do rewrite fdistXE fdist_prodE. rewrite /jcPr /proba.Pr (big_pred1 p); last first. by move=> i; rewrite !inE -xpair_eqE -!surjective_pairing. rewrite (big_pred1 p.2); last by move=> i; rewrite !inE. rewrite eqxx mulr1 fdist_sndE /= fdist_prodE. under eq_bigr do rewrite fdist_prodE /=. by rewrite -mulRA mulVR ?mulR1. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets) Reals mathcomp(Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext fdist jfdist_cond fsdist convex