proposition: Lemma setI_closed_gdynkin_salgebra G : setI_closed G -> <<d G >> = <<s G >>.
proof: Proof. move=> GI; rewrite eqEsubset; split. by apply: sub_smallest2l; apply: sigma_algebra_dynkin. pose delta (D : set T) := [set E | <<d G >> (E `&` D)]. have ddelta (D : set T) : <<d G >> D -> dynkin (delta D). move=> dGD; split; first by rewrite /delta /= setTI. - move=> E DE; rewrite /delta /=. have -> : (~` E) `&` D = ~` ((E `&` D) `|` (~` D)). by rewrite -[LHS]setU0 -(setICl D) -setIUl -setCI -{2}(setCK D) -setCU. have : <<d G >> ((E `&` D) `|` ~` D). rewrite -bigcup2E => S [dS GS]; apply: (dynkinU dS). move=> [|[|i]] [|[|j]] => // _ _; rewrite /bigcup2 /=. + by rewrite -setIA setICr setI0 => /set0P; rewrite eqxx. + by rewrite setI0 => /set0P; rewrite eqxx. + by rewrite setICA setICl setI0 => /set0P; rewrite eqxx. + by rewrite setI0 => /set0P; rewrite eqxx. + by rewrite set0I => /set0P; rewrite eqxx. + by rewrite set0I => /set0P; rewrite eqxx. + by rewrite set0I => /set0P; rewrite eqxx. move=> [|[|n]] //; rewrite /bigcup2 /=; [exact: DE| |]. + suff: <<d G >> (~` D) by exact. by move=> F [dF GF]; apply: (dynkinC dF) => //; exact: dGD. + by rewrite -setCT; apply/(dynkinC dS)/(dynkinT dS). by move=> dGEDD S /= [+ GS] => dS; apply/(dynkinC dS); exact: dGEDD. - move=> F tF deltaDF; rewrite /delta /= => S /= [dS GS]. rewrite setI_bigcupl; apply: (dynkinU dS) => //. by under eq_fun do rewrite setIC; exact: trivIset_setIl. by move=> n; exact: deltaDF. have GdG : G `<=` <<d G >> by move=> ? ? ? [_]; apply. have Gdelta A : G A -> G `<=` delta A. by move=> ? ? ?; rewrite /delta /= => ? [?]; apply; exact/GI. have GdGdelta A : G A -> <<d G >> `<=` delta A. move=> ?; apply: smallest_sub => //; last exact: Gdelta. by apply/ddelta; exact: GdG. have dGGI A B : <<d G >> A -> G B -> <<d G >> (A `&` B). by move=> ? ?; apply: GdGdelta. have dGGdelta A : <<d G >> A -> G `<=` delta A. by move=> ? ? ?; rewrite /delta /= setIC; exact: dGGI. have dGdGdelta A : <<d G >> A -> <<d G >> `<=` delta A. by move=> ?; exact: smallest_sub (ddelta _ _) (dGGdelta _ _). have dGdGdG A B : <<d G >> A -> <<d G >> B -> <<d G >> (A `&` B). by move=> ? ?; exact: dGdGdelta. apply: smallest_sub => //; apply: dynkin_setI_sigma_algebra => //. exact: dynkin_g_dynkin. 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)