proposition: Lemma bigcup_negative_set nu (F : (set T)^nat) : (forall i, nu.-negative_set (F i)) -> nu.-negative_set (\bigcup_i F i).
proof: Proof. move=> hF; have mUF : measurable (\bigcup_k F k). by apply: bigcup_measurable => n _; have [] := hF n. split=> [//|S mS SUF]. pose SF n := (S `&` F n) `\` \bigcup_(k < n) F k. have SSF : S = \bigcup_i SF i. transitivity (\bigcup_k seqDU (fun n => S `&` F n) k); last first. by apply: eq_bigcup => // n _; rewrite seqDUIE. by rewrite -seqDU_bigcup_eq -setI_bigcupr setIidl. have mSF n : measurable (SF n). apply: measurableD; first by apply: measurableI => //; have [] := hF n. by apply: bigcup_measurable => // k _; have [] := hF k. have SFS : (\sum_(0 <= i < n) nu (SF i)) @[n --> \oo] --> nu S. by rewrite SSF; apply: charge_semi_sigma_additive => //; [by rewrite /SF -seqDUIE; exact: trivIset_seqDU|exact: bigcup_measurable]. have nuS_ n : nu (SF n) <= 0 by have [_] := hF n; apply => // x -[[]]. move/cvg_lim : (SFS) => <-//; apply: lime_le. by apply/cvg_ex => /=; first eexists; exact: SFS. by apply: nearW => n; exact: sume_le0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets cardinality) mathcomp(functions fsbigop set_interval) HB(structures) reals ereal signed topology numfun normedtype sequences esum measure realfun lebesgue_measure lebesgue_integral