Classical sets 20260331 (#1924)

* introduce rectangle

* generate from cross or rectangle is the same

Co-authored-by: shinya-katsumata

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -6,9 +6,26 @@
 
 - in `realfun.v`:
   + lemma `derivable_sqrt`
+- in `classical_sets.v`:
+  + definition `rectangle`
+  + lemmas `rectangle_setX`, `setI_closed_rectangle`
+  + definitions `cross`, `cross12`
+  + lemmas `smallest_sub_sub`, `bigcap_closed_smallest`, `smallest_sub_iff`
+  + lemma `preimage_set_systemS`
+
+- in `measurable_structure.v`:
+  + lemmas `g_sigma_algebra_cross`, `g_sigma_algebra_rectangle`
+
+- in `measurable_function.v`:
+  + lemma `preimage_measurability`
 
 ### Changed
 
+- moved from `measurable_structure.v` to `classical_sets.v`:
+  + definition `preimage_set_system`
+  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
+    `preimage_set_system_id`
+
 ### Renamed
 
 - in `tvs.v`:
@@ -26,10 +43,16 @@
 
 ### Generalized
 
+- in `measurable_structure.v`:
+  + lemma `sigma_algebra_measurable` (not specialized to `setT` anymore)
+
 ### Deprecated
 
 ### Removed
 
+- in `measurable_structure.v`:
+  + lemmas `measurable_prod_g_measurableType`, `measurable_prod_g_measurableTypeR`
+
 ### Infrastructure
 
 ### Misc

classical/classical_sets.v

@@ -100,10 +100,17 @@ From mathcomp Require Import mathcomp_extra boolp wochoice.
 (*                                                                            *)
 (* ### About sets of sets                                                     *)
 (* ```                                                                        *)
-(*       set_system T := set (set T)                                          *)
-(*      setI_closed G == the set of sets G is closed under finite             *)
-(*                       intersection                                         *)
-(*      setU_closed G == the set of sets G is closed under finite union       *)
+(*                set_system T := set (set T)                                 *)
+(*               setI_closed G == the set of sets G is closed under finite    *)
+(*                                intersection                                *)
+(*               setU_closed G == the set of sets G is closed under finite    *)
+(*                                union                                       *)
+(*               rectangle X Y := [set U `*` V | U in X & V in Y]             *)
+(*   preimage_set_system D f G == set system of the preimages by f of sets    *)
+(*                                in G                                        *)
+(*               cross f g X Y := preimage_set_system setT f X                *)
+(*                                `|` preimage_set_system setT g Y            *)
+(*                     X `x` Y := cross fst snd X Y                           *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* ```                                                                        *)
@@ -258,6 +265,7 @@ Reserved Notation "[ 'disjoint' A & B ]"
 Reserved Notation "F `#` G"
   (at level 48, left associativity, format "F  `#`  G").
 Reserved Notation "'`I_' n" (at level 8, n at level 2, format "'`I_' n").
+Reserved Notation "A `x` B"  (at level 46, left associativity).
 
 Definition set T := T -> Prop.
 (* we use fun x => instead of pred to prevent inE from working *)
@@ -1643,6 +1651,69 @@ Definition setU_closed := forall A B, G A -> G B -> G (A `|` B).
 
 End set_systems.
 
+Section rectangle.
+Context {T1 T2 : Type}.
+Implicit Types (X : set_system T1) (Y : set_system T2).
+
+Definition rectangle X Y : set_system (T1 * T2) :=
+  [set U `*` V | U in X & V in Y].
+
+Lemma rectangle_setX X Y A B : X A -> Y B -> rectangle X Y (A `*` B).
+Proof. by move=> XA YB; exists A => //; exists B. Qed.
+
+Lemma setI_closed_rectangle X Y : setI_closed X -> setI_closed Y ->
+  setI_closed (rectangle X Y).
+Proof.
+move=> IG IH _ _ [A mA [B mB] <-] [A' mA' [B' mB'] <-].
+by rewrite -setXI; apply: rectangle_setX; [exact: IG|exact: IH].
+Qed.
+
+End rectangle.
+
+Definition preimage_set_system {aT rT : Type} (D : set aT) (f : aT -> rT)
+    (G : set_system rT) : set (set aT) :=
+  [set D `&` f @^-1` B | B in G].
+
+Lemma preimage_set_system0 {aT rT : Type} (D : set aT) (f : aT -> rT) :
+  preimage_set_system D f set0 = set0.
+Proof. exact: image_set0. Qed.
+
+Lemma preimage_set_systemU {aT rT : Type} (D : set aT) (f : aT -> rT) :
+  {morph preimage_set_system D f : x y / x `|` y >-> x `|` y}.
+Proof. exact: image_setU. Qed.
+
+Lemma preimage_set_system_comp {aT bT rT : Type} (D : set aT)
+    (f : aT -> bT) (g : bT -> rT) (F : set_system rT) :
+  preimage_set_system D (g \o f) F
+    = preimage_set_system D f (preimage_set_system setT g F).
+Proof.
+apply/seteqP; split=> [_ [B FB] <-|_ [_ [C FC <-] <-]].
+  by exists (g @^-1` B) => //; exists B => //; rewrite setTI.
+by exists C => //; rewrite setTI comp_preimage.
+Qed.
+
+Lemma preimage_set_system_id {aT : Type} (D : set aT) (F : set (set aT)) :
+  preimage_set_system D idfun F = setI D @` F.
+Proof. by []. Qed.
+
+Lemma preimage_set_systemS {T1 T2} (A B : set_system T2) (f : T1 -> T2) :
+  A `<=` B ->
+  preimage_set_system [set: _] f A `<=` preimage_set_system [set: _] f B.
+Proof. by move=> AB _ [C ? <-]; exists C => //; exact: AB. Qed.
+
+Section cross.
+Context {T T1 T2 : Type}.
+Implicit Types (X : set_system T1) (Y : set_system T2).
+
+Definition cross (f : T -> T1) (g : T -> T2) X Y :=
+  preimage_set_system [set: T] f X
+  `|` preimage_set_system [set: T] g Y.
+
+End cross.
+
+Definition cross12 {T1 T2 : Type} := @cross (T1 * T2)%type T1 T2 fst snd.
+Notation "A `x` B" := (cross12 A B) : classical_set_scope.
+
 Lemma subKimage {T T'} {P : set (set T')} (f : T -> T') (g : T' -> T) :
   cancel f g -> [set A | P (f @` A)] `<=` [set g @` A | A in P].
 Proof. by move=> ? A; exists (f @` A); rewrite ?image_comp ?eq_image_id/=. Qed.
@@ -2228,34 +2299,56 @@ move=> /mem_set; rewrite (@big_morph _ _ (fun X => u \in X) false orb).
 Qed.
 
 Section smallest.
-Context {T} (C : set T -> Prop) (G : set T).
+Context {T} (C : set T -> Prop).
 
-Definition smallest := \bigcap_(A in [set M | C M /\ G `<=` M]) A.
+Definition smallest (G : set T) := \bigcap_(A in [set M | C M /\ G `<=` M]) A.
 
-Lemma sub_smallest X : X `<=` G -> X `<=` smallest.
-Proof. by move=> XG A /XG GA Y /= [PY]; apply. Qed.
+Lemma smallest_sub G X : C X -> G `<=` X -> smallest G `<=` X.
+Proof. by move=> XC GX A; apply. Qed.
 
-Lemma sub_gen_smallest : G `<=` smallest. Proof. exact: sub_smallest. Qed.
+Lemma smallest_sub_sub G X : smallest G `<=` X -> G `<=` X.
+Proof. by apply: subset_trans => t Gt B [CB]; exact. Qed.
 
-Lemma smallest_sub X : C X -> G `<=` X -> smallest `<=` X.
-Proof. by move=> XC GX A; apply. Qed.
+Lemma sub_smallest G X : X `<=` G -> X `<=` smallest G.
+Proof. by move=> XG A /XG GA Y /= [PY]; exact. Qed.
 
-Lemma smallest_id : C G -> smallest = G.
+Lemma sub_gen_smallest G : G `<=` smallest G. Proof. exact: sub_smallest. Qed.
+
+Lemma smallest_id G : C G -> smallest G = G.
 Proof.
-by move=> Cs; apply/seteqP; split; [apply: smallest_sub|apply: sub_smallest].
+by move=> Cs; apply/seteqP; split; [exact: smallest_sub|exact: sub_smallest].
 Qed.
 
 End smallest.
 #[global] Hint Resolve sub_gen_smallest : core.
 
-Lemma sub_smallest2r {T} (C : set T-> Prop) G1 G2 :
+Lemma smallest_sub_iff {T} (C : set T -> Prop) (X Y : set T) :
+  C Y -> smallest C X `<=` Y <-> X `<=` Y.
+Proof.
+by move=> CY; split; [exact: smallest_sub_sub|exact: smallest_sub].
+Qed.
+
+Definition bigcap_closed {T} (C : set T -> Prop) :=
+  forall (MM : set_system T), MM `<=` C -> C (\bigcap_(A in MM) A).
+
+Section bigcap_closed_smallest.
+Context {T} (C : set T -> Prop).
+
+Lemma bigcap_closed_smallest (G : set T) : bigcap_closed C -> C (smallest C G).
+Proof. by apply; exact: subIsetl. Qed.
+
+End bigcap_closed_smallest.
+
+Lemma sub_smallest2r {T} (C : set T -> Prop) G1 G2 :
    C (smallest C G2) -> G1 `<=` G2 -> smallest C G1 `<=` smallest C G2.
-Proof. by move=> *; apply: smallest_sub=> //; apply: sub_smallest. Qed.
+Proof.
+by move=> CCG2 G12; apply: smallest_sub => //; exact: sub_smallest.
+Qed.
 
 Lemma sub_smallest2l {T} (C1 C2 : set T -> Prop) :
    (forall G, C2 G -> C1 G) ->
    forall G, smallest C1 G `<=` smallest C2 G.
-Proof. by move=> C12 G X sX M [/C12 C1M GM]; apply: sX. Qed.
+Proof. by move=> C12 G X sX M [/C12 C1M GM]; exact: sX. Qed.
 
 Section bigop_nat_lemmas.
 Context {T : Type}.

classical/filter.v

@@ -1482,7 +1482,7 @@ Lemma filterI_iterE {T : Type} (F : set (set T)) :
   smallest Filter F = filter_from (\bigcup_n (filterI_iter F n)) id.
 Proof.
 rewrite eqEsubset; split.
-  apply: smallest_sub => //; first last.
+  apply: smallest_sub; first last.
     by move=> A FA; exists A => //; exists O => //; right.
   apply: filter_from_filter; first by exists setT; exists O => //; left.
   move=> P Q [i _ sFP] [j _ sFQ]; exists (P `&` Q) => //.

theories/kernel.v

@@ -601,12 +601,10 @@ Lemma measurable_prod_subset_xsection_kernel :
   measurable `<=` XY.
 Proof.
 move=> kD_ub; rewrite measurable_prod_measurableType.
-set C := [set A `*` B | A in measurable & B in measurable].
+set C := rectangle (@measurable _ X) (@measurable _ Y).
 have CI : setI_closed C.
-  move=> _ _ [X1 mX1 [X2 mX2 <-]] [Y1 mY1 [Y2 mY2 <-]].
-  exists (X1 `&` Y1); first exact: measurableI.
-  by exists (X2 `&` Y2); [exact: measurableI|rewrite setXI].
-have CT : C setT by exists setT => //; exists setT => //; rewrite setXTT.
+  by apply: setI_closed_rectangle => E F mE MF; exact: measurableI.
+have CT : C setT by rewrite -setXTT; exact: rectangle_setX.
 have CXY : C `<=` XY.
   move=> _ [A mA [B mB <-]]; split; first exact: measurableX.
   rewrite phiM.
@@ -1305,15 +1303,6 @@ exists (fun n => if n is O then mu else mzero) => [[]//|U mU].
 by rewrite /mseries nneseries_recl// eseries0 ?adde0// => -[|].
 Qed.
 
-Let setI_closedX (d1 d2 : measure_display) (T1 : measurableType d1)
-    (T2 : measurableType d2) : @setI_closed (T1 * T2)
-  [set A `*` B | A in d1.-measurable & B in d2.-measurable].
-Proof.
-move=> X Y [X1 mX1 [X2 mX2 <-{X}]] [Y1 mY1 [Y2 mY2 <-{Y}]].
-exists (X1 `&` Y1); first exact: measurableI.
-by exists (X2 `&` Y2); [exact: measurableI|rewrite setXI].
-Qed.
-
 Variables (d1 d2 : measure_display) (T1 : measurableType d1)
   (T2 : measurableType d2) (R : realType) (k : R.-ftker T1 ~> T2)
   (f : T1 * T2 -> \bar R).
@@ -1399,7 +1388,9 @@ move=> m.
 have DE : D = @measurable _ (T1 * T2)%type.
   apply/seteqP; split => [/= A []//|].
   rewrite measurable_prod_measurableType.
-  apply: lambda_system_subset => //= C [A mA [B mB] <-].
+  apply: lambda_system_subset => //=.
+    by apply: setI_closed_rectangle => ? ? ? ?; exact: measurableI.
+  move=> C [A mA [B mB] <-].
   split; [exact: measurableX|rewrite /K kfcompkg//].
   apply: emeasurable_funM; first exact/measurable_EFinP.
   exact: measurable_kernel.

theories/lebesgue_integral_theory/lebesgue_integral_fubini.v

@@ -117,12 +117,10 @@ Lemma measurable_prod_subset_xsection
   measurable `<=` B.
 Proof.
 rewrite measurable_prod_measurableType.
-set C := [set A1 `*` A2 | A1 in measurable & A2 in measurable].
+set C := rectangle (@measurable _ T1) (@measurable _ T2).
 have CI : setI_closed C.
-  move=> X Y [X1 mX1 [X2 mX2 <-{X}]] [Y1 mY1 [Y2 mY2 <-{Y}]].
-  exists (X1 `&` Y1); first exact: measurableI.
-  by exists (X2 `&` Y2); [exact: measurableI|rewrite setXI].
-have CT : C setT by exists setT => //; exists setT => //; rewrite setXTT.
+  by apply: setI_closed_rectangle => E F mE MF; exact: measurableI.
+have CT : C setT by rewrite -setXTT; exact: rectangle_setX.
 have CB : C `<=` B.
   move=> X [X1 mX1 [X2 mX2 <-{X}]]; split; first exact: measurableX.
   have -> : phi (X1 `*` X2) = (fun x => m2D X2 * (\1_X1 x)%:E)%E.
@@ -158,12 +156,10 @@ Lemma measurable_prod_subset_ysection
   measurable `<=` B.
 Proof.
 rewrite measurable_prod_measurableType.
-set C := [set A1 `*` A2 | A1 in measurable & A2 in measurable].
+set C := rectangle (@measurable _ T1) (@measurable _ T2).
 have CI : setI_closed C.
-  move=> X Y [X1 mX1 [X2 mX2 <-{X}]] [Y1 mY1 [Y2 mY2 <-{Y}]].
-  exists (X1 `&` Y1); first exact: measurableI.
-  by exists (X2 `&` Y2); [exact: measurableI|rewrite setXI].
-have CT : C setT by exists setT => //; exists setT => //; rewrite setXTT.
+  by apply: setI_closed_rectangle => E F mE MF; exact: measurableI.
+have CT : C setT by rewrite -setXTT; exact: rectangle_setX.
 have CB : C `<=` B.
   move=> X [X1 mX1 [X2 mX2 <-{X}]]; split; first exact: measurableX.
   have -> : psi (X1 `*` X2) = (fun x => m1D X1 * (\1_X2 x)%:E)%E.

theories/measure_theory/measurable_function.v

@@ -354,20 +354,22 @@ Lemma preimage_set_system_measurable_fun d (aT : pointedType)
     (D : set (g_sigma_algebraType (preimage_set_system D f measurable))) f.
 Proof. by move=> mD A mA; apply: sub_sigma_algebra; exists A. Qed.
 
+(** The converse hols when `D` is measurable *)
+Lemma preimage_measurability d d' (aT : measurableType d)
+    (rT : measurableType d') (D : set aT) (f : aT -> rT) :
+  preimage_set_system D f (@measurable _ rT) `<=` @measurable _ aT ->
+  measurable_fun D f.
+Proof. by move=> + mD Y mY; apply; exists Y. Qed.
+
 Lemma measurability d d' (aT : measurableType d) (rT : measurableType d')
     (D : set aT) (f : aT -> rT) (G : set (set rT)) :
-  @measurable _ rT = <<s G >> -> preimage_set_system D f G `<=` @measurable _ aT ->
+  @measurable _ rT = <<s G >> ->
+  preimage_set_system D f G `<=` @measurable _ aT ->
   measurable_fun D f.
 Proof.
-move=> sG_rT fG_aT mD.
-suff h : preimage_set_system D f (@measurable _ rT) `<=` @measurable _ aT.
-  by move=> A mA; apply: h; exists A.
-have -> : preimage_set_system D f (@measurable _ rT) =
-         <<s D, preimage_set_system D f G >>.
-  by rewrite [in LHS]sG_rT [in RHS]g_sigma_preimageE.
-apply: smallest_sub => //; split => //.
-- by move=> A mA; exact: measurableD.
-- by move=> F h; exact: bigcupT_measurable.
+move=> sG_rT fG_aT /[dup] mD; apply: preimage_measurability.
+rewrite sG_rT -g_sigma_preimageE smallest_sub_iff//.
+exact: sigma_algebra_measurable.
 Qed.
 
 End measurability.