proposition: Lemma Convn_permI3_p01 (d : {fdist 'I_3}) (g : 'I_3 -> A) : <|>_d g = <|>_(fdistI_perm d S3.p01) (g \o S3.p01).
proof: Proof. have : (d ord0 + d (lift ord0 ord0) = 0 \/ d (lift ord0 ord0) + d ord_max = 0 \/ (0 < d ord0 + d (lift ord0 ord0) /\ 0 < d (lift ord0 ord0) + d ord_max)). have : (0 <= d ord0 + d (lift ord0 ord0)) by apply addr_ge0. have : (0 <= d (lift ord0 ord0) + d ord_max) by apply addr_ge0. rewrite le0r => /orP -[/eqP|H]; first by auto. rewrite le0r => /orP -[/eqP|H']; first by auto. right; right; by auto. move=> [ H | [ H | [H1 H2] ] ]. have /eqP d1 : d ord_max = 1. rewrite -(FDist.f1 d) !big_ord_recl big_ord0 addr0 addrA H add0r. by congr (d _); exact/val_inj. rewrite fdist1E1 in d1. rewrite {1}(eqP d1) Convn_fdist1. by rewrite (eqP d1) fdistI_perm_fdist1 Convn_fdist1 /= permKV. have /eqP : d ord0 = 1. rewrite -(FDist.f1 d) !big_ord_recl big_ord0 addr0. rewrite (_ : lift ord0 (lift _ _) = ord_max); last exact/val_inj. by rewrite H addr0. rewrite fdist1E1 => /eqP ->. by rewrite Convn_fdist1 fdistI_perm_fdist1 Convn_fdist1 /= permKV. have d01 : d ord0 <> 1. move=> /eqP d01. move: H2. move/fdist1P : (d01) => -> //. move/fdist1P : d01 => -> //. by rewrite add0r ltxx. move=> [:Hp]. have @p : {prob R}. apply: (@Prob.mk_ _ (d (lift ord0 ord0) / (1 - d ord0))). abstract: Hp. apply/andP; split. by rewrite divr_ge0 // subr_ge0. rewrite ler_pdivrMr ?mul1r ?subr_gt0 -?fdist_lt1; last exact/eqP. rewrite lerBrDr -(FDist.f1 d) !big_ord_recl big_ord0 addr0. by rewrite addrC lerD2l addrC -lerBlDr subrr. have [|p1] := eqVneq p 1%:pr. move/(congr1 (@Prob.p _)); rewrite [in X in X -> _]/=. move/divr1_eq => H. rewrite (@convn3E _ _ 1%:pr) ?conv1; last 2 first. exact/eqP. by rewrite H divrr // unitfE subr_eq0 eq_sym; exact/eqP. have [d00|d00] := eqVneq (d ord0) 0. rewrite (_ : probfdist _ _ = 0%:pr) ?conv0; last exact: val_inj. move: H; rewrite d00 subr0 => /eqP; rewrite fdist1E1 => /eqP ->. by rewrite fdistI_perm_fdist1 Convn_fdist1 /= permKV; congr g; exact/val_inj. rewrite (@convn3E _ _ 1%:pr) ?conv1; last first. rewrite !fdistI_permE /S3.p01 /= !permE /=. rewrite (_ : Ordinal _ = lift ord0 ord0); last exact/val_inj. by rewrite H opprB addrC subrK divrr. rewrite /S3.p01 /= fdistI_permE permE /=. rewrite (_ : Ordinal _ = lift ord0 ord0); last exact/val_inj. apply: contra d00 => /eqP d001. move: H; rewrite d001 => /esym. by rewrite subR_eq addRC -subR_eq subRR => <-. rewrite /= /S3.p01 !permE /= convC. congr (g _ <| _ |> g _). apply/val_inj; rewrite /= fdistI_permE permE /=. by rewrite (_ : Ordinal _ = lift ord0 ord0) ?H //; exact/val_inj. rewrite (@convn3E _ _ p) //; last exact/eqP. rewrite convA. rewrite (convC _ (g ord0)). have ? : 1 - d ord0 != 0 by rewrite subr_eq0; exact/eqP/nesym. have H : Prob.p [p_of (Prob.p [r_of probfdist d ord0, p]).~%:pr, [s_of probfdist d ord0, p]] != Prob.p 1%:pr :> R. apply p_of_neq1. rewrite s_of_pqE /=. rewrite onemM !onemK. rewrite -addrA -opprB. rewrite -!RmultE. rewrite -[X in (_ < _ - (_ - X) < _)%mcR]mul1R. rewrite -mulrBl -mulNr opprB mulrCA mulrV // mulr1. apply/andP; split => //. rewrite lt_neqAle; apply/andP; split. apply: contra p1 => p1. apply/eqP/val_inj => /=. move: p1; rewrite eq_sym addrC -subR_eq' => /eqP <-. by rewrite RminusE divff. by rewrite -(FDist.f1 d) !big_ord_recl /= big_ord0 addr0 addrA lerDl. rewrite -convA'; last by []. have [/eqP ds01|ds01] := eqVneq (d (S3.p01 ord0)) 1. move: (ds01); rewrite /S3.p01 permE => d01'. rewrite /= in d01'. rewrite (_ : Ordinal _ = lift ord0 ord0) in d01'; last exact/val_inj. rewrite fdist1E1 in d01'. rewrite fdist1E1 in ds01. rewrite [in RHS](eqP ds01) fdistI_perm_fdist1 Convn_fdist1 /= permKV. rewrite (_ : [p_of _, _] = 1%:pr); last first. apply/val_inj => /=. rewrite p_of_rsE /= r_of_pqE /= s_of_pqE /= (eqP d01'). by rewrite fdist10// mul0r onem0 !mul1r subr0 fdist1xx onemK divr1. rewrite conv1 /S3.p01 permE /= (_ : Ordinal _ = lift ord0 ord0) //. exact/val_inj. move=> [:Hq]. have @q : {prob R}. apply: (@Prob.mk_ _ ((fdistI_perm d S3.p01) (lift ord0 ord0) / (1 - (fdistI_perm d S3.p01) ord0))). abstract: Hq. rewrite !fdistI_permE. apply/andP. split. by apply/divr_ge0 => //; rewrite subr_ge0; apply ltW; rewrite -fdist_lt1. rewrite ler_pdivrMr ?mul1r; last by rewrite subr_gt0 -fdist_lt1. rewrite lerBrDr -(FDist.f1 (fdistI_perm d S3.p01)) !big_ord_recl big_ord0. by rewrite addr0 !fdistI_permE addrCA addrA -[X in (X <= _)]addr0 lerD2l. rewrite (@convn3E _ _ q) //; last by rewrite fdistI_permE. congr (_ <| _ |> _). - apply/val_inj => /=. rewrite fdistI_permE permE /= p_of_rsE /= r_of_pqE /=. rewrite s_of_pqE /= /onem. rewrite (_ : Ordinal _ = lift ord0 ord0); last exact/val_inj. rewrite -R1E -!RminusE -!RdivE'// -!RmultE. field. split; first by rewrite subR_eq0; exact/nesym. rewrite -addR_opp oppRB -addR_opp oppRB addRC addRA subRK. by apply/eqP; rewrite gtR_eqF // addRC; apply/RltP. - by rewrite /= /S3.p01 permE /=; congr g; exact/val_inj. - congr (_ <| _ |> _). + apply val_inj => /=. rewrite q_of_rsE /= !fdistI_permE p_of_rsE /= r_of_pqE /= s_of_pqE. rewrite /= /onem !permE /=. rewrite (_ : Ordinal _ = lift ord0 ord0); last exact/val_inj. rewrite -[RHS]RdivE'. rewrite -R1E -!RminusE -!RdivE' // -!RmultE. field. split. rewrite subR_eq0. apply/nesym/eqP. apply: contra ds01. rewrite /S3.p01 permE /= (_ : Ordinal _ = lift ord0 ord0) //; exact/val_inj. split; first by rewrite subR_eq0; exact/nesym. rewrite -addR_opp oppRB -addR_opp oppRB addRC addRA subRK. by apply/eqP; rewrite gt_eqF // addRC. + by congr g; apply val_inj => /=; rewrite /S3.p01 permE. + by rewrite /= /S3.p01 permE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix fingroup perm) Reals Lra mathcomp(mathcomp_extra Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext logb fdist convex