diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1b864bc1d..0b8cd1be9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,8 +4,26 @@ ### Added +- 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`: @@ -23,10 +41,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 diff --git a/classical/classical_sets.v b/classical/classical_sets.v index a2522509f..cdc9f1883 100644 --- a/classical/classical_sets.v +++ b/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}. diff --git a/classical/filter.v b/classical/filter.v index 0cd56cf06..1f0ac7c83 100644 --- a/classical/filter.v +++ b/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) => //. diff --git a/theories/kernel.v b/theories/kernel.v index f2f9c36a0..20db39e6a 100644 --- a/theories/kernel.v +++ b/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. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v index fa7ea76a6..4850aa1e0 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v +++ b/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. diff --git a/theories/measure_theory/measurable_function.v b/theories/measure_theory/measurable_function.v index 772e6d0a8..0bcd9504a 100644 --- a/theories/measure_theory/measurable_function.v +++ b/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 = <> -> preimage_set_system D f G `<=` @measurable _ aT -> + @measurable _ rT = <> -> + 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) = - <>. - 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. diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index 529dfffb1..222366c93 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -89,8 +89,6 @@ From mathcomp Require Import ereal topology normedtype sequences. (* ## Other measure-theoretic definitions *) (* *) (* ``` *) -(* preimage_set_system D f G == set system of the preimages by f of sets *) -(* in G *) (* g_sigma_algebra_preimage f == sigma-algebra generated by the *) (* function f *) (* g_sigma_algebra_preimageType f == the measurableType corresponding to *) @@ -1233,8 +1231,11 @@ Section measurable_lemmas. Context d (T : measurableType d). Implicit Types (A B : set T) (F : (set T)^nat) (P : set nat). -Lemma sigma_algebra_measurable : sigma_algebra setT (@measurable d T). -Proof. by split=> // [A|]; [exact: measurableD|exact: bigcupT_measurable]. Qed. +Lemma sigma_algebra_measurable D : measurable D -> + sigma_algebra D (@measurable d T). +Proof. +by move=> mD; split=> // [A|]; [exact: measurableD|exact: bigcupT_measurable]. +Qed. Lemma bigcap_measurableType F P : (forall k, P k -> measurable (F k)) -> measurable (\bigcap_(i in P) F i). @@ -1304,32 +1305,6 @@ Proof. exact: sigma_algebra_id. Qed. Section measurability. -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 sigma_algebra_preimage (aT rT : Type) (G : set (set rT)) (D : set aT) (f : aT -> rT) : sigma_algebra setT G -> sigma_algebra D (preimage_set_system D f G). @@ -1552,11 +1527,35 @@ Lemma measurable_uncurry (T1 T2 : Type) d (T : semiRingOfSetsType d) measurable (G x.1 x.2) <-> measurable (uncurry G x). Proof. by case: x. Qed. +Section g_sigma_algebra_cross. + +(**md Yoneda Lemma: two elements in a poset are equal if and only if they share the same set of upper bounds *) +Let forall_subset_eq {T} (A B : set_system T) : + sigma_algebra [set: T] A -> sigma_algebra [set: T] B -> + (forall Z, sigma_algebra [set: T] Z -> A `<=` Z <-> B `<=` Z) + <-> A = B. +Proof. +move=> sA sB; split=> [AB|AB]; last by rewrite AB. +by apply/seteqP; split; exact/AB. +Qed. + +Lemma g_sigma_algebra_cross {T1 T2 : pointedType} (X : set_system T1) + (Y : set_system T2) : + <> >> = <>. +Proof. +apply/forall_subset_eq; [exact: smallest_sigma_algebra..|]. +move=> Z mZ. +rewrite smallest_sub_iff//=. +rewrite {1}/cross12/= subUset -g_sigma_preimageE//. +rewrite smallest_sub_iff//= -subUset -[_ `|` _]/(cross12 X Y)//. +by rewrite smallest_sub_iff. +Qed. + +End g_sigma_algebra_cross. + Definition g_sigma_preimageU d1 d2 - (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2) (T : Type) - (f1 : T -> T1) (f2 : T -> T2) := - <>. + (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2) (T : Type) + (f1 : T -> T1) (f2 : T -> T2) := <>. #[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `g_sigma_preimageU`")] Notation preimage_classes := g_sigma_preimageU (only parsing). @@ -1622,34 +1621,37 @@ Lemma measurableX d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2 measurable A -> measurable B -> measurable (A `*` B). Proof. move=> mA mB. -have -> : A `*` B = (A `*` setT) `&` (setT `*` B) :> set (T1 * T2). - by rewrite -{1}(setIT A) -{1}(setTI B) setXI. -rewrite setXT setTX; apply: measurableI. +rewrite -(setIT A) -(setTI B) setXI setXT setTX; apply: measurableI. - by apply: sub_sigma_algebra; left; exists A => //; rewrite setTI. - by apply: sub_sigma_algebra; right; exists B => //; rewrite setTI. Qed. +Lemma g_sigma_algebra_rectangle {T1 T2 : pointedType} (X : set_system T1) + (Y : set_system T2) : X [set: T1] -> Y [set: T2] -> + <> = <>. +Proof. +move=> sX sY; apply/seteqP; split. +- rewrite smallest_sub_iff//= => _ [A1 X1] [A2 X2] <-. + rewrite (_ : _ `*` _ = fst @^-1` A1 `&` snd @^-1` A2)//. + apply: (@measurableI _ (@g_sigma_algebraType _ (X `x` Y))). + + by apply: sub_sigma_algebra; left; exists A1 => //; rewrite setTI. + + by apply: sub_sigma_algebra; right; exists A2 => //; rewrite setTI. +- apply: sub_sigma_algebra2 => A [|]. + + rewrite /preimage_set_system/= => -[A1 XA1 <-{A}]. + by rewrite -setXT setTI; exact: rectangle_setX. + + rewrite /preimage_set_system/= => -[A1 XA1 <-{A}]. + by rewrite -setTX setTI; exact: rectangle_setX. +Qed. + Section product_salgebra_algebraOfSetsType. Context d1 d2 (T1 : algebraOfSetsType d1) (T2 : algebraOfSetsType d2). Let M1 := @measurable _ T1. Let M2 := @measurable _ T2. -Let M1xM2 := [set A `*` B | A in M1 & B in M2]. +#[deprecated(since="mathcomp-analysis 1.17.0", note="use `g_sigma_algebra_rectangle` instead")] Lemma measurable_prod_measurableType : - (d1, d2).-prod.-measurable = <>. -Proof. -rewrite eqEsubset; split. - apply: smallest_sub; first exact: smallest_sigma_algebra. - rewrite subUset; split. - - have /subset_trans : preimage_set_system setT fst M1 `<=` M1xM2. - by move=> _ [X MX <-]; exists X=> //; exists setT; rewrite /M2 // setIC//. - by apply; exact: sub_sigma_algebra. - - have /subset_trans : preimage_set_system setT snd M2 `<=` M1xM2. - by move=> _ [Y MY <-]; exists setT; rewrite /M1 //; exists Y. - by apply; exact: sub_sigma_algebra. -apply: smallest_sub; first exact: smallest_sigma_algebra. -by move=> _ [A ?] [B ?] <-; apply: measurableX => //; exact: sub_sigma_algebra. -Qed. + (d1, d2).-prod.-measurable = <>. +Proof. by rewrite g_sigma_algebra_rectangle//; exact: measurableT. Qed. End product_salgebra_algebraOfSetsType. @@ -1657,10 +1659,10 @@ Section product_salgebra_g_measurableTypeR. Context d1 (T1 : algebraOfSetsType d1) (T2 : pointedType) (C2 : set (set T2)). Hypothesis setTC2 : setT `<=` C2. -(* NB: useful? *) -Lemma measurable_prod_g_measurableTypeR : +#[deprecated(since="mathcomp-analysis 1.17.0")] +Lemma __deprecated__measurable_prod_g_measurableTypeR : @measurable _ (T1 * g_sigma_algebraType C2)%type - = <>. + = <>. Proof. rewrite measurable_prod_measurableType //; congr (<>). rewrite predeqE => X; split=> [[A mA] [B mB] <-{X}|[A C1A] [B C2B] <-{X}]. @@ -1674,11 +1676,12 @@ Section product_salgebra_g_measurableType. Variables (T1 T2 : pointedType) (C1 : set (set T1)) (C2 : set (set T2)). Hypotheses (setTC1 : setT `<=` C1) (setTC2 : setT `<=` C2). -Lemma measurable_prod_g_measurableType : +#[deprecated(since="mathcomp-analysis 1.17.0")] +Lemma __deprecated__measurable_prod_g_measurableType : @measurable _ (g_sigma_algebraType C1 * g_sigma_algebraType C2)%type = - <>. + <>. Proof. -rewrite measurable_prod_measurableType //; congr (<>). +rewrite -[LHS]g_sigma_algebra_rectangle//; congr (<>). rewrite predeqE => X; split=> [[A mA] [B mB] <-{X}|[A C1A] [B C2B] <-{X}]. by exists A; [exact: setTC1|exists B => //; exact: setTC2]. by exists A; [exact: sub_sigma_algebra|exists B => //; exact: sub_sigma_algebra]. diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v index 26f797a8c..e5bf1db35 100644 --- a/theories/measure_theory/measure_function.v +++ b/theories/measure_theory/measure_function.v @@ -1867,7 +1867,7 @@ Lemma g_sigma_algebra_measure_unique_cover : Proof. pose GT : ringOfSetsType G.-sigma:= g_sigma_algebraType G. move=> sGm1m2; pose g' k := \bigcup_(i < k) g i. -have sGm := smallest_sub (@sigma_algebra_measurable _ T) Gm. +have sGm := smallest_sub (@sigma_algebra_measurable _ T _ measurableT) Gm. have Gg' i : <> (g' i). apply: (@fin_bigcup_measurable _ GT) => //. by move=> n _; apply: sub_sigma_algebra. diff --git a/theories/topology_theory/function_spaces.v b/theories/topology_theory/function_spaces.v index 2e18cbdd1..5cc34da3a 100644 --- a/theories/topology_theory/function_spaces.v +++ b/theories/topology_theory/function_spaces.v @@ -1227,8 +1227,8 @@ have C : compact R. apply: (subclosed_compact _ C); first exact: closed_closure. have WsubR : (fW @` W) `<=` R. by move=> f [i Wi <-] x; rewrite /K; apply: subset_closure; exists i. -rewrite closureE; apply: smallest_sub (compact_closed _ C) WsubR. -exact: hausdorff_product. +rewrite closureE; apply: smallest_sub => //. +by apply: compact_closed => //=; exact: hausdorff_product. Qed. Lemma uniform_pointwise_compact (W : set (X -> Y)) : diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v index 356ce9ce3..0565b3413 100644 --- a/theories/topology_theory/subspace_topology.v +++ b/theories/topology_theory/subspace_topology.v @@ -261,10 +261,12 @@ have /closed_subspaceP := @closed_closure _ (U : set (subspace A)). move=> [V clV VAclUA] /[dup] /(@closureS (subspace _)). have /closure_id <- := closed_subspaceT => /setIidr <-; rewrite setIC. move=> UsubA; rewrite eqEsubset; split. - apply: setSI; rewrite closureE; apply: smallest_sub (@subset_closure _ U). + apply: setSI; rewrite closureE. + apply: smallest_sub (@subset_closure _ U). by apply: closed_subspaceW; exact: closed_closure. -rewrite -VAclUA; apply: setSI; rewrite closureE //=; apply: smallest_sub => //. -apply: subset_trans (@subIsetl _ V A); rewrite VAclUA subsetI; split => //. +rewrite -VAclUA; apply: setSI; rewrite closureE //=. +apply: smallest_sub => //; apply: subset_trans (@subIsetl _ V A). +rewrite VAclUA subsetI; split => //. exact: (@subset_closure _ (U : set (subspace A))). Qed. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 1c4b0db96..265198b09 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -858,14 +858,14 @@ Definition closure_subset := closureS. Lemma closureE A : closure A = smallest closed A. Proof. rewrite eqEsubset; split=> [x ? B [cB AB]|]; first exact/cB/(closureS AB). -exact: (smallest_sub (@closed_closure _ _) (@subset_closure _ _)). +by apply: smallest_sub; [exact: closed_closure|exact: subset_closure]. Qed. (* TODO: the LHS and RHS of the equality should be swapped *) Lemma closure_id E : closed E <-> E = closure E. Proof. split=> [?|->]; last exact: closed_closure. -rewrite eqEsubset; split => //; exact: subset_closure. +by rewrite eqEsubset; split => //; exact: subset_closure. Qed. End closure_lemmas.