proposition: Lemma nondecreasing_cvg_mu d (T : ringOfSetsType d) (R : realFieldType) (mu : {measure set T -> \bar R}) (F : (set T) ^nat) : (forall i, measurable (F i)) -> measurable (\bigcup_n F n) -> nondecreasing_seq F -> mu \o F @ \oo --> mu (\bigcup_n F n).
proof: Proof. move=> mF mbigcupF ndF. have Binter : trivIset setT (seqD F) := trivIset_seqD ndF. have FBE : forall n, F n.+1 = F n `|` seqD F n.+1 := setU_seqD ndF. have FE n : F n = \big[setU/set0]_(i < n.+1) (seqD F) i := eq_bigsetU_seqD n ndF. rewrite eq_bigcup_seqD. have mB i : measurable (seqD F i) by elim: i => * //=; apply: measurableD. apply: cvg_trans (measure_semi_sigma_additive _ mB Binter _); last first. by rewrite -eq_bigcup_seqD. apply: (@cvg_trans _ ((fun n => \sum_(i < n.+1) mu (seqD F i)) @ \oo)). rewrite [X in _ --> X @ \oo](_ : _ = mu \o F) // funeqE => n. by rewrite -measure_semi_additive // -?FE// => -[|k]. move=> S [n _] nS; exists n => // m nm. under eq_fun do rewrite -(big_mkord predT (mu \o seqD F)). exact/(nS m.+1)/(leq_trans nm). 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)