proposition: Lemma ring_sigma_sub_additive : sigma_sub_additive mu -> sigma_sub_additive Rmu.
proof: Proof. move=> muS; move=> /= D A Am Dm Dsub. rewrite /Rmu -(eq_eseriesr (fun _ _ => esum_fset _ _))//; last first. by move=> *; exact: decomp_finite_set. rewrite nneseries_esum ?esum_esum//=; last by move=> *; rewrite esum_ge0. set K := _ `*`` _. have /ppcard_eqP[f] : (K #= [set: nat])%card. apply: cardMR_eq_nat => [|i]. by rewrite (_ : [set _ | true] = setT)//; exact/predeqP. split; first by apply/finite_set_countable; exact: decomp_finite_set. exact/set0P/decompN0. have {Dsub} : D `<=` \bigcup_(k in K) k.2. apply: (subset_trans Dsub); apply: bigcup_sub => i _. rewrite -[A i]cover_decomp; apply: bigcup_sub => X/= XAi. by move=> x Xx; exists (i, X). rewrite -(image_eq [bij of f^-1%FUN])/=. rewrite (esum_set_image _ f^-1)//= bigcup_image => Dsub. have DXsub X : X \in decomp D -> X `<=` \bigcup_i ((f^-1%FUN i).2 `&` X). move=> XD; rewrite -setI_bigcupl -[Y in Y `<=` _](setIidr (decomp_sub XD)). by apply: setSI. have mf i : measurable ((f^-1)%function i).2. have [_ /mem_set/decomp_measurable] := 'invS_f (I : setT i). by apply; exact: Am. have mfD i X : X \in decomp D -> measurable (((f^-1)%FUN i).2 `&` X : set T). by move=> XD; apply: measurableI; [exact: mf|exact: (decomp_measurable _ XD)]. apply: (@le_trans _ _ (\sum_(i <oo) \sum_(X <- fset_set (decomp D)) mu ((f^-1%FUN i).2 `&` X))). rewrite nneseries_sum// fsbig_finite/=; last exact: decomp_finite_set. rewrite [leLHS]big_seq [leRHS]big_seq. rewrite lee_sum// => X /[!in_fset_set]; last exact: decomp_finite_set. move=> XD; have Xm := decomp_measurable Dm XD. by apply: muS => // [i|]; [exact: mfD|exact: DXsub]. apply: lee_lim => /=; do ?apply: is_cvg_nneseries=> //. by move=> n _; exact: sume_ge0. near=> n; rewrite [n in _ <= n]big_mkcond; apply: lee_sum => i _. rewrite ifT ?inE//. under eq_big_seq. move=> x; rewrite in_fset_set=> [xD|]; last exact: decomp_finite_set. rewrite -RmuE//; last exact: mfD. over. rewrite -fsbig_finite/=; last exact: decomp_finite_set. rewrite -measure_fin_bigcup//=. - rewrite -setI_bigcupr (cover_decomp D) -[leRHS]RmuE// ?le_measure ?inE//. by apply: measurableI => //; apply: sub_gen_smallest; apply: mf. by apply: sub_gen_smallest; apply: mf. - exact: decomp_finite_set. - by apply: trivIset_setIl; apply: decomp_triv. - by move=> X /= XD; apply: sub_gen_smallest; apply: mfD; rewrite inE. Unshelve. all: by end_near. 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)