proposition: Lemma isd_mlim T (f : nat -> distr T) : isdistr (mlim f).
proof: Proof. split=> [x|J]; rewrite /mlim. case: nlimP=> // l cvSl; apply/fine_ge0/(ncvg_geC _ cvSl). by move=> n; apply/ge0_mu. move=> uqJ; pose F j := if `[< iscvg (fun n => f n j) >] then fun n => f n j else 0%:S. apply/(@le_trans _ _ (\sum_(j <- J) (fine (nlim (F j) )))). apply/ler_sum=> j _; rewrite /F; case/boolP: `[< _ >] => //. move/asboolPn=> h; rewrite nlimC; case: nlimP=> //. by case=> // l cf; case: h; exists l. rewrite -lee_fin -nlim_sumR => [i _|]. rewrite /F; case/boolP: `[< _ >] => [/asboolP //|]. by move=> _; apply/iscvgC. rewrite leNgt; apply/negP; pose s n := \sum_(j <- J) F j n. move/ncvg_gt=> -/(_ s (nlim_ncvg _)) []. suff: iscvg s by case=> l cs; exists l%:E. apply/iscvg_sum=> j _; rewrite /F; case/boolP: `[< _ >]. by move/asboolP. by move=> _; apply/iscvgC. move=> K /(_ _ (leqnn K)) /=; apply/negP; rewrite -leNgt. apply/(@le_trans _ _ (\sum_(j <- J) f K j)); last first. have /(gerfinseq_psum uqJ) := summable_mu (f K). move/le_trans=> -/(_ _ (le1_mu (f K)))=> h. by apply/(le_trans _ h)/ler_sum=> i _; apply/ler_norm. by apply/ler_sum=> j _; rewrite /F; case/boolP: `[< _ >]. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum