proposition: Lemma Convn_permI3_p02 (d : {fdist 'I_3}) (g : 'I_3 -> A) : <|>_d g = <|>_(fdistI_perm d S3.p02) (g \o S3.p02).
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 le_eqVlt => /orP -[|H]; first by move/eqP; auto. rewrite le_eqVlt => /orP -[|H']; first by move/eqP; 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; 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 d1 : d ord0 = 1. rewrite -(FDist.f1 d) !big_ord_recl big_ord0 addr0 addrC. apply/eqP. rewrite -subr_eq subrr. rewrite (_ : lift ord0 (lift _ _) = ord_max) ?H //; exact/val_inj. rewrite fdist1E1 in d1. by rewrite (eqP d1) Convn_fdist1 fdistI_perm_fdist1 Convn_fdist1 /= permKV. have d01 : d ord0 <> 1%coqR. 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; first by apply/divr_ge0/ltW => //; rewrite subr_gt0 -fdist_lt1; exact/eqP. rewrite ler_pdivrMr; last by rewrite subr_gt0 -fdist_lt1; exact/eqP. rewrite mul1r. rewrite lerBrDr -(FDist.f1 d) !big_ord_recl big_ord0 addr0. by rewrite addrC lerD2l addrC -lerBlDr subrr. rewrite (@convn3E _ _ p) //; last exact/eqP. rewrite convC. rewrite (convC _ _ (g (Ordinal (erefl (2 < 3)%nat)))). have [/eqP dmax1|dmax1] := eqVneq (d ord_max) 1%coqR. move/fdist1P in dmax1. by move: H1; rewrite dmax1 // dmax1 // addr0 ltxx. have [d00|d00] := eqVneq (d ord0) 0. rewrite (_ : (Prob.p (probfdist d ord0)).~%:pr = 1%:pr) ?conv1; last first. by apply/val_inj; rewrite /= d00 onem0. rewrite (@convn3E _ _ 1%:pr); last 2 first. rewrite fdistI_permE /= !permE /=. rewrite (_ : Ordinal _ = ord_max) //; exact/val_inj. rewrite !fdistI_permE /S3.p02 !permE /=. rewrite (_ : Ordinal _ = ord_max) //; last exact/val_inj. rewrite -[in LHS](FDist.f1 d) !big_ord_recl big_ord0 addr0 d00 add0r. rewrite (_ : lift _ (lift _ _) = ord_max); last exact/val_inj. rewrite addrK divrr //. apply/eqP => d10. by move: H1; rewrite d00 d10 addr0 ltxx. rewrite /= /S3.p02 !permE /= conv1. congr (g _ <| _ |> _). apply/val_inj => /=. rewrite fdistI_permE permE /=. rewrite (_ : Ordinal _ = ord_max) //; last exact/val_inj. rewrite d00 subr0 divr1 /onem -(FDist.f1 d) /= !big_ord_recl big_ord0 addr0. rewrite d00 add0r [X in X - _]addrC addrK; congr (d _); exact/val_inj. have H : [p_of (Prob.p p).~%:pr, (Prob.p (probfdist d ord0)).~%:pr] != 1%:pr. apply: p_of_neq1 => /=; apply/andP; split. by apply/onem_gt0; rewrite -fdist_lt1; exact/eqP. by rewrite ltrBlDr ltrDl -fdist_gt0. rewrite -convA'; last by []. move=> [:Hq]. have @q : {prob R}. apply: (@Prob.mk_ _ ((fdistI_perm d S3.p02) (lift ord0 ord0) / (1 - (fdistI_perm d S3.p02) ord0))). abstract: Hq. rewrite !fdistI_permE !permE /= (_ : Ordinal _ = ord_max); last exact/val_inj. apply/andP. split. apply/divr_ge0 => //; first by apply/ltW; rewrite subr_gt0 -fdist_lt1. rewrite ler_pdivrMr ?mul1r; last by rewrite subr_gt0 -fdist_lt1 //. rewrite lerBrDr -(FDist.f1 d) !big_ord_recl big_ord0 addr0. by rewrite (_ : lift _ (lift _ _) = ord_max) ?lerDr //; exact/val_inj. rewrite (@convn3E _ _ q) //; last first. rewrite fdistI_permE permE /= (_ : Ordinal _ = ord_max) //; exact/val_inj. rewrite /= !permE /=. have ? : 1 - d ord0 != 0; first by rewrite subr_eq0 eq_sym; exact/eqP. congr (g _ <| _ |> (_ <| _ |> _)). apply val_inj => /=. rewrite !fdistI_permE p_of_rsE /= permE /=. rewrite (_ : Ordinal _ = ord_max); last exact/val_inj. rewrite {1}/onem. rewrite mulrBl mul1r -mulrA mulVr ?mulr1//. rewrite /onem -addrA -opprB opprK; apply/eqP; rewrite subr_eq; apply/eqP. rewrite -(FDist.f1 d) !big_ord_recl big_ord0 addr0. rewrite (_ : lift _ (lift _ _) = ord_max); last exact/val_inj. by rewrite addrA addrC addrA addrAC addrA. apply val_inj => /=. rewrite !fdistI_permE !permE /= q_of_rsE /= p_of_rsE /=. rewrite (_ : Ordinal _ = ord_max); last exact/val_inj. rewrite onemK. rewrite -!RdivE' //. rewrite -!RminusE. rewrite {1 2}/Rdiv. rewrite -2!mulRA. rewrite [in RHS]/Rdiv. congr (_ * _)%coqR. rewrite mulRA mulVR; last first. rewrite subR_eq0' eq_sym; exact/eqP. rewrite mul1R. congr Rinv. rewrite onemM !onemK. rewrite -RminusE -!RplusE -!RmultE. rewrite addRC. rewrite -{1}(mulR1 (d (lift ord0 ord0) / _))%coqR. rewrite -subRBA. rewrite -mulRBr. rewrite -addR_opp. rewrite -mulRN. rewrite oppRB. rewrite /Rdiv. rewrite -mulRA. rewrite mulVR ?mulR1; last first. rewrite subR_eq0' eq_sym; exact/eqP. apply/esym; rewrite subR_eq -(FDist.f1 d) !big_ord_recl big_ord0 addr0. rewrite (_ : lift _ (lift _ _) = ord_max); last exact/val_inj. by rewrite addrA. 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