proposition: Lemma g_salgebra_measure_unique_cover : (forall n A, <<s G >> A -> m1 (g n `&` A) = m2 (g n `&` A)) -> forall A, <<s G >> A -> m1 A = m2 A.
proof: Proof. pose GT := [the ringOfSetsType _ of salgebraType G]. move=> sGm1m2; pose g' k := \bigcup_(i < k) g i. have sGm := smallest_sub (@sigma_algebra_measurable _ T) Gm. have Gg' i : <<s G >> (g' i). apply: (@fin_bigcup_measurable _ GT) => //. by move=> n _; apply: sub_sigma_algebra. have sG'm1m2 n A : <<s G >> A -> m1 (g' n `&` A) = m2 (g' n `&` A). move=> sGA; rewrite setI_bigcupl bigcup_mkord. elim: n => [|n IHn] in A sGA *; rewrite (big_ord0, big_ord_recr) ?measure0//=. have sGgA i : <<s G >> (g i `&` A). by apply: (@measurableI _ GT) => //; exact: sub_sigma_algebra. apply: eq_measureU; rewrite ?sGm1m2 ?IHn//; last first. - by rewrite -big_distrl -setIA big_distrl/= IHn// setICA setIid. - exact/sGm. - by apply: bigsetU_measurable => i _; apply/sGm. have g'_cover : \bigcup_k (g' k) = setT. by rewrite -subTset -g_cover => x [k _ gx]; exists k.+1 => //; exists k => /=. have nd_g' : nondecreasing_seq g'. move=> m n lemn; rewrite subsetEset => x [k km gx]; exists k => //=. exact: leq_trans lemn. move=> A gA. have -> : A = \bigcup_n (g' n `&` A) by rewrite -setI_bigcupl g'_cover setTI. transitivity (lim (m1 (g' n `&` A) @[n --> \oo])). apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. - by move=> n; apply: measurableI; exact/sGm. - by apply: bigcupT_measurable => k; apply: measurableI; exact/sGm. - by move=> ? ? ?; apply/subsetPset; apply: setSI; exact/subsetPset/nd_g'. transitivity (lim (m2 (g' n `&` A) @[n --> \oo])). by apply/congr_lim/funext => x; apply: sG'm1m2 => //; exact/sGm. apply/cvg_lim => //; apply: nondecreasing_cvg_mu. - by move=> k; apply: measurableI => //; exact/sGm. - by apply: bigcupT_measurable => k; apply: measurableI; exact/sGm. - by move=> a b ab; apply/subsetPset; apply: setSI; exact/subsetPset/nd_g'. 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)