proposition: Lemma jtype_not_empty : 0 < #|A| -> 0 < #|B| -> 0 < #|P_ n (A , B)|.
proof: Proof. move=> Anot0 Bnot0. move: (Anot0); case/card_gt0P => a _. move: (Bnot0); case/card_gt0P => b _. apply/card_gt0P. have [tmp Htmp] : [finType of {f : {ffun A -> {ffun B -> 'I_n.+1}} | \sum_(a1 in A) \sum_(b1 in B) f a1 b1 == n}]. exists [ffun a1 => [ffun b1 => if (a1, b1) == (a, b) then Ordinal (ltnSn n) else Ordinal (ltn0Sn n)]]. rewrite pair_big /=. rewrite (bigD1 (a, b)) //= big1 ; first by rewrite 2!ffunE eqxx addn0. move=> p /negbTE Hp ; by rewrite 2!ffunE -surjective_pairing Hp. have Htmp' : (forall a b, (chan_of_jtype Anot0 Bnot0 tmp) a b = (let ln := \sum_(b0 in B) (tmp a) b0 in if ln == 0 then / #|B|%:R else (((tmp a) b)%:R / ln%:R)%R)). by move=> a0 b0; rewrite ffunE. exists (@JType.mk _ _ _ (chan_of_jtype Anot0 Bnot0 tmp) tmp Htmp Htmp'). by rewrite inE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup perm) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist entropy num_occ channel types