proposition: Lemma output_type_out_fdist : forall b, type.d (`tO( V )) b = `O( P , V ) b.
proof: Proof. rewrite /fdist_of_ffun /= /OutType.d /OutType.f => b /=. rewrite ffunE big_morph_natRD /Rdiv (big_morph _ (morph_mulRDl _) (mul0R _)). rewrite fdist_outE; apply eq_bigr => a _. case: (typed_tuples_not_empty P) => /= ta Hta. move: (Vctyp). rewrite in_set. move/cond_type_equiv/(_ _ Hta a) => sum_V. rewrite (JType.c_f V) /=. case: ifP => [/eqP |] Hcase. rewrite Hcase in sum_V. rewrite in_set in Hta. move/forallP/(_ a) : Hta. rewrite -sum_V div0R. move/eqP => ->; rewrite -RmultE mulR0. move/eqP in Hcase. rewrite sum_nat_eq0 in Hcase. move/forallP/(_ b) : Hcase. move/implyP/(_ Logic.eq_refl)/eqP => ->. by rewrite mul0R. - rewrite -RmultE -mulRA sum_V; congr (_ * _). move: Hta; rewrite in_set => /forallP/(_ a)/eqP ->. by rewrite mulRA -{1}(mul1R (/ n%:R)) mulVR // INR_eq0' -sum_V Hcase. 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