proposition: Lemma measure_sigma_sub_additive_tail d (R : realType) (T : semiRingOfSetsType d) (mu : {measure set T -> \bar R}) (A : set T) (F : nat -> set T) N : (forall n, measurable (F n)) -> measurable A -> A `<=` \bigcup_(n in ~` `I_N) F n -> (mu A <= \sum_(N <= n <oo) mu (F n))%E.
proof: Proof. move=> mF mA AF; rewrite eseries_cond eseries_mkcondr. rewrite (@eq_eseriesr _ _ (fun n => mu (if (N <= n)%N then F n else set0))). - apply: measure_sigma_sub_additive => //. + by move=> n; case: ifPn. + move: AF; rewrite bigcup_mkcond. by under eq_bigcupr do rewrite mem_not_I. - by move=> o _; rewrite (fun_if mu) measure0. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)