proposition: Lemma preimC_Cal_E k n epsilon0 : let M := [finType of 'I_k.+1] in let PHI' := jtdec P W epsilon0 in let Cal_E := @cal_E M n epsilon0 in forall f : encT A M n, preimC (PHI' f) ord0 =i (~: Cal_E f ord0) :|: \bigcup_(m : M | m != ord0) Cal_E f m.
proof: Proof. move=> M PHI' Cal_E f tb. rewrite 2!inE. apply/idP/idP. - rewrite /PHI' /jtdec ffunE. case: (pickP _) => [m2 Hm2 | Hm2]. + move/eqP => m2m0. rewrite finset.in_setU finset.in_setC {1}/Cal_E {1}/cal_E inE; apply/orP; left. case/andP : Hm2 => _ /forallP/(_ ord0)/implyP; apply. by move/eqP in m2m0; apply: contra m2m0 => /eqP <-. + move=> _. rewrite finset.in_setU. move/negbT : {Hm2}(Hm2 ord0). rewrite negb_and. case/orP => Hm2. * by rewrite finset.in_setC {1}/Cal_E {1}/cal_E inE Hm2. * apply/orP; right. apply/negPn. move: Hm2; apply contra => Hm2. apply/forallP => m_; apply/implyP => m_m0. apply: contra Hm2 => Hm2. apply/bigcupP; exists m_ => //; by rewrite /Cal_E /cal_E inE. - rewrite finset.in_setU ffunE. case: (pickP _) => [m2 Hm2|//]. case/orP. + rewrite finset.in_setC /cal_E inE => Hy. apply/eqP => -[m20]. by case/andP : Hm2; rewrite m20 (negbTE Hy). + case/bigcupP => m Hm; rewrite /cal_E 2!inE => m_tb. apply/eqP => -[m20]. case/andP : Hm2 => _ /forallP /(_ m); by rewrite !inE m_tb m20 Hm implyTb. 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