proposition: Lemma first_summand k n epsilon0 : let M := [finType of 'I_k.+1] in (\sum_(f : encT A M n) Wght.d P f * Pr (W ``(| f ord0)) (~: cal_E epsilon0 f ord0)) = Pr ((P `X W) `^ n) (~: `JTS P W n epsilon0).
proof: Proof. move=> M. have M_prednK : #|M|.-1.+1 = #|M| by rewrite card_ord. pose E_F_N := @cal_E M n epsilon0. rewrite {1}/cal_E. case/card_gt0P : (fdist_card_neq0 P) => a _. pose zero := @enum_rank M ord0. have : 0%N = zero :> nat by rewrite /zero enum_rank_ord. move/(@sum_rV_ffun _ _ _ _ _ (Wght.d P) (fun r v => r * Pr (W ``(| v )) (~: [set w | prod_rV (v, w) \in `JTS P W n epsilon0])) ord0 zero). rewrite (_ : nth ord0 (enum M) 0 = ord0); last by rewrite enum_ordSl. move=> <- /=. transitivity (\sum_(v : 'rV['rV[A]_n]_#|M|) ( (\prod_(m : M) P `^ n ([ffun x => v ``_ x] (enum_rank m))) * \sum_(w | w \in ~: cal_E epsilon0 [ffun x => v ``_ x] zero) (W ``(| [ffun x => v ``_ x] zero)) w)). apply eq_bigr => v _; congr (_ * _). rewrite Wght.dE ffunE. by apply eq_bigr => m _; rewrite 2!ffunE. apply eq_big. - move=> /= ?; by rewrite !inE ffunE. - move=> ? _; by rewrite ffunE. rewrite /cal_E. transitivity (\sum_(v : 'rV[A]_n) (\sum_(y in ~: [set w | prod_rV (v, w) \in `JTS P W n epsilon0]) (W ``(| v)) y) * \sum_(j in {: #|M|.-1.-tuple ('rV[A]_n)}) (\prod_(m : M) P `^ _ ((tcast M_prednK [tuple of v :: j]) !_ (enum_rank m)))). rewrite (reindex_onto (fun y : {ffun _ -> 'rV__} => \row_(i < _) y (enum_val i)) (fun p : 'rV_ _ => [ffun x => p ``_ (enum_rank x)])) //=; last first. move=> v _; by apply/rowP => i; rewrite mxE ffunE enum_valK. apply trans_eq with (\sum_(f : {ffun M -> 'rV__}) ((\prod_(m < k.+1) P `^ n (f m)) * \sum_(y in ~: [set y0 | prod_rV (f ord0, y0) \in `JTS P W n epsilon0]) W ``(y | f ord0))). apply eq_big => //= f. - apply/eqP/ffunP => m; by rewrite ffunE mxE enum_rankK. - move/eqP => Hf; congr (_ * _). apply eq_bigr => i _; by rewrite -[in RHS]Hf 2!ffunE. apply eq_big => /=. move=> ?; by rewrite !inE -[in RHS]Hf !ffunE mxE. move=> ? _; by rewrite -[in RHS]Hf !ffunE mxE. rewrite (_ : ord0 = nth ord0 (enum M) 0); last by rewrite enum_ordSl. rewrite -(big_tuple_ffun _ (fun f => \prod_(m : M) P `^ n (f m)) (fun r yn => r * (\sum_(y in ~: [set y0 | prod_rV (yn, y0) \in `JTS P W n epsilon0]) W ``(y | yn))) (\row_(i < n) a) ord0)%R. transitivity (\sum_(j : _) (\prod_(m : M) P `^ n ((tcast M_prednK j) !_ (enum_rank m))) * (\sum_(y in ~: [set y0 | prod_rV (nth (\row_(i < n) a) j 0, y0) \in `JTS P W n epsilon0]) W ``(y | nth (\row_(i < n) a) j 0))). rewrite (big_tcast (esym M_prednK)) esymK. apply eq_bigr => i _; congr (_ * _). apply eq_bigr => m _; by rewrite ffunE. have H : nth (\row_(i < n) a) (tcast M_prednK i) 0 = nth (\row_(i < n) a) i 0. move: M_prednK i; rewrite card_ord => M_prednK i. rewrite -(tnth_nth _ i ord0) -(tnth_nth _ (tcast M_prednK i) ord0). by rewrite tcastE /= cast_ord_id. apply eq_big => m; by rewrite !inE H. rewrite -(@big_tuple_cons_behead _ #|M|.-1 (fun j => ((\prod_(m : M) P `^ n ((tcast M_prednK j) !_ (enum_rank m))) * (\sum_(y in ~: [set y0 | prod_rV (nth (\row_(i < n) a) j 0, y0) \in `JTS P W n epsilon0]) W ``(y | nth (\row_(i < n) a) j 0)))) xpredT xpredT). apply eq_bigr => ta _ /=; by rewrite -big_distrl /= mulRC. transitivity ((\sum_(ta in 'rV[A]_n) P `^ _ ta * (\sum_(y in ~: [set y0 | prod_rV (ta, y0) \in `JTS P W n epsilon0]) (W ``(| ta ) ) y)) * \sum_(j in {:k.-tuple ('rV[A]_n)}) \prod_(m < k) (P `^ _ (j !_ m)))%R. rewrite big_distrl /=. apply eq_bigr => ta _. rewrite -mulRA mulRCA; congr Rmult. transitivity (\sum_(j in {: #|'I_k|.-tuple ('rV[A]_n) }) P `^ _ ta * \prod_(m < k) P `^ _ (j !_ (enum_rank m)))%R. have k_prednK : #|'I_k.+1|.-1 = #|'I_k| by rewrite !card_ord. rewrite (big_tcast (esym k_prednK)) esymK. apply eq_bigr => i0 Hi0. rewrite big_ord_recl /=. congr (P `^ _ _ * _)%R; first by rewrite tcastE // enum_rank_ord. apply eq_bigr => i1 _; congr (P `^ _ _). rewrite !tcastE {1}/tnth /=. rewrite (_ : enum_rank _ = (enum_rank i1).+1 :> nat) /=; last by rewrite !enum_rank_ord. apply set_nth_default; by rewrite size_tuple /= enum_rank_ord /= card_ord. rewrite -big_distrr /=; congr (_ * _)%R. rewrite (big_tcast (esym (card_ord k))) esymK. apply eq_bigr => /= i0 _. apply eq_bigr => /= i1 _. by rewrite tcastE -enum_rank_ord. rewrite rsum_rmul_tuple_pmf_tnth mulR1. transitivity (\sum_(v in 'rV[A]_n) \sum_(y in ~: [set w | prod_rV (v, w) \in `JTS P W n epsilon0]) ((P `X W) `^ n (prod_rV (v, y))))%R. apply eq_bigr => /= v _. rewrite big_distrr /=. apply eq_bigr => // w _. rewrite DMCE 2!fdist_rVE -big_split /=. apply eq_bigr => /= i _. rewrite fdist_prodE -fst_tnth_prod_rV -snd_tnth_prod_rV /= mulRC. by rewrite RmultE GRing.mulrC. rewrite /Pr big_rV_prod pair_big_dep /=. by apply eq_bigl; case=> /= ? ?; 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