proposition: Lemma g_salgebra_measure_unique_trace : (forall X, (<<s D, H >>) X -> X `<=` D) -> forall X, <<s D, H >> X -> m1 X = m2 X.
proof: Proof. move=> sDHD; set E := [set A | [/\ measurable A, m1 A = m2 A & A `<=` D] ]. have HE : H `<=` E. by move=> X HX; rewrite /E /=; split; [exact: Hm|exact: m1m2|case: HX]. have setDE : setD_closed E. move=> A B BA [mA m1m2A AD] [mB m1m2B BD]; split; first exact: measurableD. - rewrite measureD//; last first. by rewrite (le_lt_trans _ m1oo)//; apply: le_measure => // /[!inE]. rewrite setIidr//= m1m2A m1m2B measureD// ?setIidr//. by rewrite (le_lt_trans _ m1oo)//= -m1m2A; apply: le_measure => // /[!inE]. - by rewrite setDE; apply: subIset; left. have ndE : ndseq_closed E. move=> A ndA EA; split; have mA n : measurable (A n) by have [] := EA n. - exact: bigcupT_measurable. - transitivity (limn (m1 \o A)). apply/esym/cvg_lim=>//. exact/(nondecreasing_cvg_mu mA _ ndA)/bigcupT_measurable. transitivity (limn (m2 \o A)). by apply/congr_lim/funext => n; have [] := EA n. apply/cvg_lim => //. exact/(nondecreasing_cvg_mu mA _ ndA)/bigcupT_measurable. - by apply: bigcup_sub => n; have [] := EA n. have sDHE : <<s D, H >> `<=` E. by apply: monotone_class_subset => //; split => //; [move=> A []|exact/HE]. by move=> X /sDHE[]. 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)