proposition: Lemma __admitted__exp_split A f mu : \E?_[mu] f -> \E_[mu] f = \P_[mu] A * \E_[mu, A] f + \P_[mu] (predC A) * \E_[mu, predC A] f.
proof: Proof. Proof using Type. Admitted. Lemma has_esp_bounded f mu : (exists M, forall x, `|f x| < M) -> \E?_[mu] f. Proof. case=> M ltM; rewrite /has_esp; apply/summable_seqP. exists (Num.max M 0); first by rewrite le_maxr lexx orbT. move=> J uqJ; apply/(@le_trans _ _ (\sum_(j <- J) M * mu j)). apply/ler_sum=> j _; rewrite normrM [X in _*X]ger0_norm //. by apply/ler_wpM2r=> //; apply/ltW. case: (ltrP M 0) => [lt0_M|ge0_M]. rewrite ?(ltW lt0_M) // -mulr_sumr. by rewrite nmulr_rle0 //; apply/sumr_ge0. by rewrite -mulr_sumr ler_piMr // -pr_mem ?le1_pr. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum