proposition: Lemma second_summand n k epsilon0 : let M := [finType of 'I_k.+1] in forall i, i != ord0 -> (\sum_(f : encT A M n) Wght.d P f * Pr (W ``(| f ord0)) (cal_E epsilon0 f i))%R = Pr ((P `^ n) `x `O( P , W ) `^ n) [set x | prod_rV x \in `JTS P W n epsilon0].
proof: Proof. move=> M. have M_prednK : #|M|.-1.+1 = #|M| by rewrite card_ord. move=> i i_m0. set E_F_N := @cal_E M n epsilon0. have Hcast : (i.-1 + (#|M| - i.+1).+1).+1 = #|M|. rewrite /M card_ord subSS addnS -addSn prednK; last by rewrite lt0n. by rewrite subnKC // -ltnS ltn_ord. transitivity ( \sum_(j1 in {: i.-1.-tuple ('rV[A]_n)}) \sum_(j2 in {: (#|M| - i.+1).-tuple ('rV[A]_n)}) \sum_(j0 in 'rV[A]_n) \sum_(ji in 'rV[A]_n) Wght.d P [ffun x => (tcast Hcast [tuple of j0 :: j1 ++ ji :: j2])!_x] * \sum_(y | y \in [set w | prod_rV (ji, w) \in `JTS P W n epsilon0]) (W ``(| j0)) y)%R. transitivity ( \sum_(j0 in 'rV[A]_n) \sum_(j1 in {: i.-1.-tuple ('rV[A]_n)}) \sum_(ji in 'rV[A]_n) \sum_(j2 in {: (#|M| - i.+1).-tuple ('rV[A]_n)}) Wght.d P [ffun x => (tcast Hcast [tuple of j0 :: j1 ++ ji :: j2])!_x] * \sum_( y | y \in [set w | prod_rV (ji, w) \in `JTS P W n epsilon0]) (W ``(| j0) ) y)%R. rewrite (reindex_onto (fun p => [ffun x => p!_(enum_rank x)]) (fun y => fgraph y)) /=; last first. move=> f _; apply/ffunP => m; by rewrite ffunE tnth_fgraph enum_rankK. transitivity ( \sum_(j : _) (Wght.d P [ffun x => j!_(enum_rank x)] * Pr (W ``(| [ffun x => j!_(enum_rank x)] ord0)) (E_F_N [ffun x => j!_(enum_rank x)] i)))%R. apply eq_big => //= x; apply/eqP/eq_from_tnth => j. by rewrite tnth_fgraph ffunE enum_valK. rewrite (big_tcast (card_ord k.+1)). rewrite -(big_tuple_cons_behead _ xpredT xpredT). apply eq_bigr => i0 _. have [Hq i_q] : (i.-1 + (k - i.-1) = k /\ i <= k)%nat. split. by rewrite subnKC // -(leq_add2r 1) !addn1 (leq_ltn_trans _ (ltn_ord i)) // leq_pred. by rewrite -(leq_add2r 1) !addn1 ltn_ord. rewrite (big_tcast (esym Hq)) esymK. rewrite -big_cat_tuple /=. apply eq_bigr => /= i1 _. have Hs : (k - i.-1 = (k - i).+1)%nat. by rewrite -subn1 subnBA ?lt0n // addnC -addnBA. rewrite (big_tcast Hs) -(big_tuple_cons_behead _ xpredT xpredT). apply eq_bigr => i2 _. have Ht : (#|'I_k.+1| - i.+1 = k - i)%nat by rewrite card_ord /= subSS. rewrite (big_tcast Ht) //; apply eq_bigr => /= i3 _; congr (_ * _)%R. - rewrite 2!Wght.dE /Wght.f 2!ffunE /=. rewrite (reindex_onto enum_rank enum_val); last by move=> *; rewrite enum_valK. apply eq_big => /=; first by move=> x; rewrite enum_rankK eqxx inE. move=> i4 _; congr (P `^ _ _). rewrite !ffunE; congr (_ !_ _). apply/val_inj => /=. rewrite [LHS]eq_tcast /= !eq_tcast /= [RHS]eq_tcast eq_tcast /=; congr (_ :: _ ++ _ :: _). by rewrite eq_tcast. - apply eq_big. + move=> x /=. rewrite !inE ffunE. rewrite (_ : (_ !_ _) = i2) //=. rewrite enum_rank_ord /= tcastE !cast_ord_comp (tnth_nth i0) /=. rewrite eq_tcast /=. rewrite -cat_cons nth_cat /= size_tuple prednK ?lt0n // ltnn subnn. by rewrite eq_tcast. + move=> i4 Hi4. rewrite 2!DMCE. apply eq_bigr => i5 /= _; congr (W _ _). by rewrite ffunE tcastE /= enum_rank_ord /= cast_ordK. rewrite exchange_big /=. apply eq_bigr => /= i1 _. rewrite [in RHS]exchange_big /=. apply eq_bigr => /= i2 _. rewrite [in RHS]exchange_big /=. by apply eq_bigr. transitivity ( (\sum_(j1 in {: i.-1.-tuple ('rV[A]_n)}) \sum_(j2 in {: (#|M| - i.+1).-tuple ('rV[A]_n)}) \prod_(i <- j1 ++ j2) (P `^ n) i) * (\sum_(j0 in 'rV[A]_n) \sum_(ji in 'rV[A]_n) ((P `^ n) j0) * ((P `^ n) ji) * (\sum_( y | y \in [set y0 | prod_rV (ji , y0) \in `JTS P W n epsilon0]) (W ``(| j0) ) y)))%R. rewrite !big_distrl /=. apply eq_bigr => j1 _. rewrite !big_distrl /=. apply eq_bigr => j2 _. rewrite !big_distrr /=. apply eq_bigr => j0 _. rewrite !big_distrr /=. apply eq_bigr => j3 _. rewrite !mulRA Wght.dE /Wght.f /=; congr (_ * _)%R. transitivity (\prod_( i <- j0 :: j1 ++ j3 :: j2) P `^ _ i)%R; last first. rewrite big_cons -mulRA mulRCA; congr (_ * _)%R. rewrite big_cat /= big_cons [in RHS]mulRC mulRCA; congr (_ * _)%R. by rewrite big_cat /= mulRC. rewrite [in RHS](big_nth j0) /= big_mkord. transitivity (\prod_(j < #|@predT M|) P `^ _ ([ffun x => (tcast Hcast [tuple of j0 :: j1 ++ j3 :: j2])!_(enum_rank x)] (enum_val j)))%R. rewrite ffunE; apply eq_big => ? //= _. by rewrite !ffunE enum_valK. have j_M : (size (j1 ++ j3 :: j2)).+1 = #|M|. rewrite size_cat (size_tuple j1) /= (size_tuple j2) card_ord. by rewrite -[RHS](card_ord k.+1) -Hcast card_ord. rewrite j_M. apply eq_bigr => i0 _; congr (P `^ n _). rewrite ffunE /= enum_valK tcastE /tnth /=. apply set_nth_default; by rewrite /= j_M ltn_ord. transitivity (\sum_(j0 : 'rV[A]_n) \sum_(ji : 'rV[A]_n) ((P `^ n) j0) * ((P `^ n) ji) * (\sum_( y | y \in [set y0 in 'rV[B]_n | prod_rV (ji , y0) \in `JTS P W n epsilon0]) (W ``(| j0)) y))%R. set lhs := (\sum_(_ <- _) _)%R. suff : lhs = 1%R by move=> ->; rewrite mul1R. rewrite /lhs {lhs}. rewrite (@big_cat_tuple_seq _ i.-1 (#|M| - i.+1) (fun x => \prod_(i0 <- x) (P `^ n) i0))%R. by rewrite rsum_rmul_tuple_pmf. transitivity (\sum_(ji : 'rV[A]_n) ((P `^ n) ji) * (\sum_(y | y \in [set y0 | prod_rV (ji , y0) \in `JTS P W n epsilon0]) \sum_(j0 : 'rV[A]_n) ((W ``(| j0) ) y) * ((P `^ n) j0)))%R. rewrite exchange_big /=. apply eq_bigr => ta _. transitivity (\sum_(i1 : 'rV[A]_n) P `^ _ ta * P `^ _ i1 * (\sum_(y in [set y0 | prod_rV (ta, y0) \in `JTS P W n epsilon0]) W ``(y | i1)))%R. apply eq_bigr => i1 _. by rewrite -mulRA mulRCA mulRA. rewrite exchange_big /= big_distrr /=. apply eq_bigr => ta' _. rewrite -[in X in _ = (_ * X)%R]big_distrl /= -mulRA; congr Rmult. by rewrite mulRC. transitivity (\sum_(ji : 'rV[A]_n) ((P `^ n) ji) * \sum_( y | y \in [set y0 | prod_rV (ji , y0) \in `JTS P W n epsilon0]) ((`O(P , W)) `^ n) y)%R. apply eq_bigr => ta _; congr (_ * _)%R; apply eq_bigr => /= tb _. by rewrite fdist_rV_out; apply eq_bigr => i0 _; by rewrite DMCE. transitivity (\sum_(v : 'rV[A]_n) (\sum_(y | y \in [set y0 | prod_rV (v , y0) \in `JTS P W n epsilon0]) ((P `^ n) `x ((`O(P , W)) `^ n)) (v, y)))%R. apply eq_bigr => // v _. rewrite big_distrr /=; apply eq_bigr => w _; by rewrite fdist_prodE. transitivity (\sum_( jiy | prod_rV jiy \in `JTS P W n epsilon0) ((P `^ n) `x ((`O(P , W)) `^ n)) jiy)%R. rewrite [in LHS]pair_big_dep /=. by apply eq_big => -[? ?] /=; rewrite !inE ?fdist_prodE. by apply eq_bigl => ?; rewrite !inE. 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