proposition: Lemma error_rate_symmetry (P : {fdist A}) (W : `Ch(A, B)) epsilon : 0 <= epsilon -> let Jtdec := jtdec P W epsilon in forall m m', \sum_(f : encT A M n) (Wght.d P f * e(W, mkCode f (Jtdec f)) m) = \sum_(f : encT A M n) (Wght.d P f * e(W, mkCode f (Jtdec f)) m').
proof: Proof. move=> Hepsilon PHI' m m'. set lhs := \sum_(_ <- _) _. have Hlhs : lhs = \sum_(f : encT A M n) (Wght.d P f * e(W, mkCode f (PHI' f)) m) by []. have -> : lhs = \sum_(f : encT A M n) (Wght.d P (o_PI m m' f) * e(W, mkCode (o_PI m m' f) (PHI' (o_PI m m' f))) m). rewrite Hlhs (reindex_onto (o_PI m m') (o_PI m m')) /=; last first. by move=> i _; apply/ffunP => m_; rewrite o_PI_2. by apply eq_bigl => x /=; apply/eqP/ffunP => y; exact: o_PI_2. apply: eq_bigr => g _; rewrite wght_o_PI; congr (_ * _). rewrite /ErrRateCond /= (_ : (o_PI m m' g) m = g m'); last by rewrite ffunE tpermL. congr Pr; apply/setP => tb /=. rewrite 2!inE. apply/negbLR. rewrite finset.in_setC negbK. apply/idP/idP. - rewrite {1}/PHI' {1}/jtdec ffunE. set p0 := fun _ => _ && _. case: (pickP _) => [m0 Hm0 | Hm0 /eqP //]. case/eqP => ?; subst m0. rewrite /p0 {p0} in Hm0. rewrite /PHI' /jtdec. rewrite inE ffunE. case: (pickP _) => [m1 Hm1 | Hm1]. + apply/eqP; f_equal. suff : (prod_rV (g m', tb) \in `JTS P W n epsilon) && [forall m'0, (m'0 != m') ==> (prod_rV (g m'0, tb) \notin `JTS P W n epsilon)]. by move/(jtdec_map Hm1). apply/andP; split. * by move: Hm0; rewrite {1}/o_PI ffunE tpermL => /andP[]. * apply/forallP => m_; apply/implyP => m__m'. case/andP : Hm0 => Hm0 /forallP Hm0'. have [m_m|m_m] := eqVneq m_ m. - subst m_. by move: (Hm0' m'); rewrite eq_sym m__m' /= /o_PI ffunE tpermR; exact. - move: (Hm0' m_) => {}Hm0'. rewrite eq_sym in m__m'. by move: Hm0'; rewrite m_m /= /o_PI ffunE tpermD // eq_sym. + exfalso. rewrite {1}/o_PI ffunE tpermL in Hm0. move/negbT: {Hm1}(Hm1 m'). rewrite negb_and; case/orP => Hm'. * by case/andP : Hm0 => Hm0 _; rewrite Hm0 in Hm'. * move/negP : Hm'; apply. apply/forallP => m_; apply/implyP => m_m'. case/andP: Hm0 => Hm0 /forallP Hm01. have [m_m|m_m] := eqVneq m_ m. - subst m_. by move: (Hm01 m'); rewrite eq_sym m_m' /= /o_PI ffunE tpermR; exact. - by move: (Hm01 m_); rewrite m_m /= /o_PI ffunE tpermD // eq_sym. - rewrite {1}/PHI' {1}/jtdec inE ffunE. case: (pickP _) => [m0 Hm0 | Hm0 /eqP //]. case/eqP => ?; subst m0. apply/eqP. rewrite /PHI' /jtdec ffunE. case: (pickP _) => [m1 Hm1 | Hm1]. + f_equal. suff : (prod_rV ((o_PI m m' g) m, tb) \in `JTS P W n epsilon) && [forall m'0, (m'0 != m) ==> (prod_rV ((o_PI m m' g) m'0, tb) \notin `JTS P W n epsilon)]. by move/(jtdec_map Hm1). apply/andP; split. - by rewrite /o_PI ffunE tpermL; case/andP: Hm0. - apply/forallP => m_; apply/implyP => m_m. have [?|m_m'] := eqVneq m_ m'. + subst m_. rewrite /o_PI ffunE tpermR. case/andP : Hm0 => _ /forallP/(_ m). by rewrite eq_sym m_m. + rewrite eq_sym in m_m; rewrite eq_sym in m_m'. rewrite /o_PI ffunE tpermD //. case/andP : Hm0 => _ /forallP/(_ m_). by rewrite eq_sym m_m'. * exfalso. move: {Hm1}(Hm1 m) => /negbT; rewrite negb_and => /orP[|]. - rewrite /o_PI ffunE tpermL. by case/andP : Hm0 => ->. - move/negP; apply. apply/forallP => m_; apply/implyP => m_m. have [?|m_m'] := eqVneq m_ m'. + subst m_. rewrite /o_PI ffunE tpermR. case/andP : Hm0 => _ /forallP/(_ m). by rewrite eq_sym m_m. + rewrite eq_sym in m_m; rewrite eq_sym in m_m'. rewrite /o_PI ffunE tpermD //. case/andP : Hm0 => _ /forallP/(_ m_). by rewrite eq_sym m_m'. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix perm) Reals Lra Classical mathcomp(Rstruct classical_sets) ssrZ ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq joint_typ_seq channel channel_code