proposition: Lemma ring_measurableE : d.-ring.-measurable = measurable_fin_trivIset.
proof: Proof. apply/seteqP; split; last first. move=> _ [B [-> Bm Bfin Btriv]]; apply: fin_bigcup_measurable => //. by move=> i Di; apply: sub_gen_smallest; apply: Bm. have mdW A : measurable A -> measurable_fin_trivIset A. move=> Am; exists [set A]; split; do ?by [rewrite bigcup_set1|move=> ? ->|]. by move=> ? ? -> ->. have mdI : setI_closed measurable_fin_trivIset. move=> _ _ [A [-> Am Afin Atriv]] [B [-> Bm Bfin Btriv]]. rewrite setI_bigcupl; under eq_bigcupr do rewrite setI_bigcupr. rewrite -bigcup_setM -(bigcup_image _ _ id). eexists; split; [reflexivity | | exact/finite_image/finite_setM |]. by move=> _ [X [? ?] <-]; apply: measurableI; [apply: Am|apply: Bm]. apply: trivIset_sets => -[a b] [a' b']/= [Xa Xb] [Xa' Xb']; rewrite setIACA. by move=> [x [Ax Bx]]; rewrite (Atriv a a') 1?(Btriv b b')//; exists x. have mdisj_bigcap : finN0_bigcap_closed measurable_fin_trivIset. exact/finN0_bigcap_closedP/mdI. have mDbigcup I (D : set I) (A : set T) (B : I -> set T) : finite_set D -> measurable A -> (forall i, D i -> measurable (B i)) -> measurable_fin_trivIset (A `\` \bigcup_(i in D) B i). have [->|/set0P D0] := eqVneq D set0. by rewrite bigcup0// setD0 => *; apply: mdW. move=> Dfin Am Bm; rewrite -bigcupDr//; apply: mdisj_bigcap=> // i Di. by have [F [Ffin Fm -> ?]] := semi_measurableD A (B i) Am (Bm _ Di); exists F. have mdU : fin_trivIset_closed measurable_fin_trivIset. elim/Pchoice=> I D F Dfin Ftriv Fm. have /(_ _ (set_mem _))/cid-/(all_sig_cond_dep (fun=> set0)) [G /(_ _ (mem_set _))GP] := Fm _ _. under eq_bigcupr => i Di do case: (GP i Di) => ->. rewrite -bigcup_setM_dep -(bigcup_image _ _ id); eexists; split=> //. - by move=> _ [i [Di Gi] <-]; have [_ + _ _] := GP i.1 Di; apply. - by apply: finite_image; apply: finite_setMR=> // i Di; have [] := GP i Di. apply: trivIset_sets => -[i X] [j Y] /= [Di Gi] [Dj Gj] XYN0. suff eqij : i = j. by rewrite {i}eqij in Di Gi *; have [_ _ _ /(_ _ _ _ _ XYN0)->] := GP j Dj. apply: Ftriv => //; have [-> _ _ _] := GP j Dj; have [-> _ _ _] := GP i Di. by case: XYN0 => [x [Xx Yx]]; exists x; split; [exists X|exists Y]. have mdDI : setDI_closed measurable_fin_trivIset. move=> A B mA mB; have [F [-> Fm Ffin Ftriv]] := mA. have [F' [-> F'm F'fin F'triv]] := mB. have [->|/set0P F'N0] := eqVneq F' set0. by rewrite bigcup_set0 setD0; exists F. rewrite setD_bigcupl; apply: mdU => //; first by apply: trivIset_setIr. move=> X DX; rewrite -bigcupDr//; apply: mdisj_bigcap => //. move=> Y DY; case: (semi_measurableD X Y); [exact: Fm|exact: F'm|]. by move=> G [Gfin Gm -> Gtriv]; exists G. apply: smallest_sub => //; split=> //; first by apply: mdW. move=> A B mA mB; rewrite -(setUIDK B A) setUA [X in X `|` _]setUidl//. rewrite -bigcup2inE; apply: mdU => //; last by move=> [|[]]// _; apply: mdDI. by move=> [|[]]// [|[]]//= _ _ []; rewrite setDE ?setIA => X [] []//. 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)