proposition: Lemma measure_sigma_sub_additive : sigma_sub_additive mu.
proof: Proof. move=> X A Am Xm XA; pose B i := A i `&` X. have XE : X = \bigcup_i B i by rewrite -setI_bigcupl setIidr. have Bm i : measurable (B i) by rewrite /B; apply: measurableI. have subBA i : B i `<=` A i by rewrite /B. have subDUB i : seqDU B i `<=` A i by move=> x [/subBA]. have DUBm i : measurable (seqDU B i : set (SetRing.type T)). by apply: measurableD => //; do 1?apply: bigsetU_measurable => *; apply: sub_gen_smallest. rewrite XE; move: (XE); rewrite seqDU_bigcup_eq. under eq_bigcupr do rewrite -[seqDU B _]cover_decomp//. rewrite -bigcup_setM_dep; set K := _ `*`` _. have /ppcard_eqP[f] : (K #= [set: nat])%card. apply: cardMR_eq_nat=> // i; split; last by apply/set0P; rewrite decompN0. exact/finite_set_countable/decomp_finite_set. pose f' := f^-1%FUN; rewrite -(image_eq [bij of f'])/= bigcup_image/=. pose g n := (f' n).2; have fVtriv : trivIset [set: nat] g. move=> i j _ _; rewrite /g. have [/= _ f'iB] : K (f' i) by apply: funS. have [/= _ f'jB] : K (f' j) by apply: funS. have [f'ij|f'ij] := eqVneq (f' i).1 (f' j).1. move=> /(decomp_triv f'iB)/=; rewrite f'ij => /(_ f'jB) f'ij2. apply: 'inj_f'; rewrite ?inE//= -!/(f' _); move: f'ij f'ij2. by case: (f' i) (f' j) => [? ?] [? ?]//= -> ->. move=> [x [f'ix f'jx]]; have Bij := @trivIset_seqDU _ B (f' i).1 (f' j).1 I I. rewrite Bij ?eqxx// in f'ij; exists x; split. - by move/mem_set : f'iB => /decomp_sub; apply. - by move/mem_set : f'jB => /decomp_sub; apply. have g_inj : set_inj [set i | g i != set0] g. by apply: trivIset_inj=> [i /set0P//|]; apply: sub_trivIset fVtriv. move=> XEbig; rewrite measure_semi_bigcup//= -?XEbig//; last first. move=> i; have [/= _ /mem_set] : K (f' i) by apply: funS. exact: decomp_measurable. rewrite [leLHS](_ : _ = \sum_(i <oo | g i != set0) mu (g i)); last first. rewrite !nneseries_esum// esum_mkcond [RHS]esum_mkcond; apply: eq_esum. move=> i _; rewrite ifT ?inE//=; case: ifPn => //. by rewrite notin_set /= -/(g _) => /negP/negPn/eqP ->. rewrite -(esum_pred_image mu g)//. rewrite [leLHS](_ : _ = \esum_(X in range g) mu X); last first. rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum. move=> Y _; case: ifPn; rewrite ?(inE, notin_set)/=. by move=> [i giN0 giY]; rewrite ifT// ?inE//=; exists i. move=> Ngx; case: ifPn; rewrite ?(inE, notin_set)//=. move=> [i _ giY]; apply: contra_not_eq Ngx; rewrite -giY => mugi. by exists i => //; apply: contra_neq mugi => ->; rewrite measure0. have -> : range g = \bigcup_i (decomp (seqDU B i)). apply/predeqP => /= Y; split => [[n _ gnY]|[n _ /= YBn]]. have [/= _ f'nB] : K (f' n) by apply: funS. by exists (f' n).1 => //=; rewrite -gnY. by exists (f (n, Y)) => //; rewrite /g /f' funK//= inE. rewrite esum_bigcup//; last first. move=> i j /=. have [->|/set0P DUBiN0] := eqVneq (seqDU B i) set0. rewrite decomp_set0 ?set_fset1 => /negP[]. apply/eqP/predeqP=> x; split=> [[Y/=->]|->]//; first by rewrite measure0. by exists set0. have [->|/set0P DUBjN0] := eqVneq (seqDU B j) set0. rewrite decomp_set0 ?set_fset1 => _ /negP[]. apply/eqP/predeqP=> x; split=> [[Y/=->]|->]//=; first by rewrite measure0. by exists set0. move=> _ _ [Y /= [/[dup] +]]. move=> /mem_set /decomp_sub YBi /mem_set + /mem_set /decomp_sub YBj. move=> /(decomp_neq0 DUBiN0) [y Yy]. apply: (@trivIset_seqDU _ B) => //; exists y. by split => //; [exact: YBi|exact: YBj]. rewrite nneseries_esum// set_true le_esum// => i _. rewrite [leLHS](_ : _ = \sum_(j \in decomp (seqDU B i)) mu j); last first. by rewrite esum_fset//; exact: decomp_finite_set. rewrite -SetRing.Rmu_fin_bigcup//=; last 3 first. exact: decomp_finite_set. exact: decomp_triv. by move=> ?; exact: decomp_measurable. rewrite -[leRHS]SetRing.RmuE// le_measure//; last by rewrite cover_decomp. - rewrite inE; apply: fin_bigcup_measurable; first exact: decomp_finite_set. move=> j /mem_set jdec; apply: sub_gen_smallest. exact: decomp_measurable jdec. - by rewrite inE; apply: sub_gen_smallest; exact: Am. 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)