diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 39c539337..a14df7346 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,8 +4,6 @@ ### Added -### Changed - - in `mathcomp_extra.v`: + lemmas `prodr_ile1`, `nat_int` @@ -27,7 +25,10 @@ + lemma `pi_irrationnal` - in `numfun.v` - + lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp` + + lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp` + +- in `classical_sets.v`: + + lemmas `xsectionE`, `ysectionE` ### Changed @@ -38,10 +39,23 @@ + put the notation ``` ^`() ``` and ``` ^`( _ ) ``` in scope `classical_set_scope` - in `numfun.v` - + lock `funepos`, `funeneg` - + + lock `funepos`, `funeneg` + +- moved from `lebesgue_integral.v` to `measure.v` and generalized + + lemmas `measurable_xsection`, `measurable_ysection` + ### Renamed +- in `measure.v` + + `preimage_class` -> `preimage_set_system` + + `image_class` -> `image_set_system` + + `preimage_classes` -> `g_sigma_preimageU` + + `preimage_class_measurable_fun` -> `preimage_set_system_measurable_fun` + + `sigma_algebra_preimage_class` -> `sigma_algebra_preimage` + + `sigma_algebra_image_class` -> `sigma_algebra_image` + + `sigma_algebra_preimage_classE` -> `g_sigma_preimageE` + + `preimage_classes_comp` -> `g_sigma_preimageU_comp` + ### Generalized ### Deprecated diff --git a/classical/classical_sets.v b/classical/classical_sets.v index e5e7579d2..86b9b0ebe 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -3263,11 +3263,17 @@ Proof. by apply/idP/idP => [|]; [rewrite inE|rewrite /ysection !inE /= inE]. Qed Lemma ysectionP x y A : ysection A y x <-> A (x, y). Proof. by rewrite /ysection/= inE. Qed. +Lemma xsectionE A x : xsection A x = (fun y => (x, y)) @^-1` A. +Proof. by apply/seteqP; split => [y|y] /xsectionP. Qed. + +Lemma ysectionE A y : ysection A y = (fun x => (x, y)) @^-1` A. +Proof. by apply/seteqP; split => [x|x] /ysectionP. Qed. + Lemma xsection0 x : xsection set0 x = set0. -Proof. by rewrite predeqE /xsection => y; split => //=; rewrite inE. Qed. +Proof. by rewrite xsectionE preimage_set0. Qed. Lemma ysection0 y : ysection set0 y = set0. -Proof. by rewrite predeqE /ysection => x; split => //=; rewrite inE. Qed. +Proof. by rewrite ysectionE preimage_set0. Qed. Lemma in_xsectionX X1 X2 x : x \in X1 -> xsection (X1 `*` X2) x = X2. Proof. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 187ee9f08..284f18536 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -4799,24 +4799,6 @@ End integral_ae_eq. (** Product measure *) -Section measurable_section. -Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). -Implicit Types (A : set (T1 * T2)). - -Lemma measurable_xsection A x : measurable A -> measurable (xsection A x). -Proof. -move=> mA; rewrite (xsection_indic R) -(setTI (_ @^-1` _)). -exact: measurableT_comp. -Qed. - -Lemma measurable_ysection A y : measurable A -> measurable (ysection A y). -Proof. -move=> mA; rewrite (ysection_indic R) -(setTI (_ @^-1` _)). -exact: measurableT_comp. -Qed. - -End measurable_section. - Section ndseq_closed_B. Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Implicit Types A : set (T1 * T2). diff --git a/theories/measure.v b/theories/measure.v index 96e695153..cc1637134 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -68,7 +68,7 @@ From HB Require Import structures. (* mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets *) (* ``` *) (* *) -(* ## Structures for functions on classes of sets *) +(* ## Structures for functions on set systems *) (* *) (* Hierarchy of contents, measures, s-finite/sigma-finite/finite measures, *) (* etc. Also contains a number of details about its implementation. *) @@ -197,8 +197,8 @@ From HB Require Import structures. (* lambda_system D G == G is a lambda_system of subsets of D *) (* <> == lambda-system generated by G on D *) (* <> := <> *) -(* monotone G == G is a monotone class *) -(* <> == monotone class generated by G *) +(* monotone G == G is a monotone set system *) +(* <> == monotone set system generated by G *) (* := smallest monotone G *) (* dynkin G == G is a set of sets that form a Dynkin *) (* system (or a d-system) *) @@ -209,17 +209,19 @@ From HB Require Import structures. (* ## Other measure-theoretic definitions *) (* *) (* ``` *) -(* measurable_fun D f == the function f with domain D is measurable *) -(* preimage_class D f G == class of the preimages by f of sets in G *) -(* image_class D f G == class of the sets with a preimage by f in G *) -(* sigma_subadditive mu == predicate defining sigma-subadditivity *) +(* measurable_fun D f == the function f with domain D is measurable *) +(* preimage_set_system D f G == set system of the preimages by f of sets in G *) +(* image_set_system D f G == set system of the sets with a preimage by f *) +(* in G *) +(* sigma_subadditive mu == predicate defining sigma-subadditivity *) (* subset_sigma_subadditive mu == alternative predicate defining *) -(* sigma-subadditivity *) -(* mu.-negligible A == A is mu negligible *) -(* measure_is_complete mu == the measure mu is complete *) -(* {ae mu, forall x, P x} == P holds almost everywhere for the measure mu, *) -(* declared as an instance of the type of filters *) -(* ae_eq D f g == f is equal to g almost everywhere *) +(* sigma-subadditivity *) +(* mu.-negligible A == A is mu negligible *) +(* measure_is_complete mu == the measure mu is complete *) +(* {ae mu, forall x, P x} == P holds almost everywhere for the measure mu, *) +(* declared as an instance of the type of *) +(* filters *) +(* ae_eq D f g == f is equal to g almost everywhere *) (* ``` *) (* *) (* ## Measure extension theorem *) @@ -257,7 +259,7 @@ From HB Require Import structures. (* *) (* ## Product of measurable spaces *) (* ``` *) -(* preimage_classes f1 f2 == sigma-algebra generated by the union of *) +(* g_sigma_preimageU f1 f2 == sigma-algebra generated by the union of *) (* the preimages by f1 and the preimages by *) (* f2 with f1 : T -> T1 and f : T -> T2, T1 *) (* and T2 being semiRingOfSetsType's *) @@ -345,7 +347,7 @@ Bind Scope measure_display_scope with measure_display. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -Section classes. +Section set_systems. Context {T} (C : set (set T) -> Prop) (D : set T) (G : set (set T)). Definition setC_closed := forall A, G A -> G (~` A). @@ -411,7 +413,7 @@ Definition lambda_system := Definition monotone := ndseq_closed /\ niseq_closed. -End classes. +End set_systems. #[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `lambda_system`")] Notation monotone_class := lambda_system (only parsing). #[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `setSD_closed`")] @@ -1695,26 +1697,27 @@ Notation measurable_funT_comp := measurableT_comp (only parsing). Section measurability. -Definition preimage_class (aT rT : Type) (D : set aT) (f : aT -> rT) +Definition preimage_set_system (aT rT : Type) (D : set aT) (f : aT -> rT) (G : set (set rT)) : set (set aT) := [set D `&` f @^-1` B | B in G]. (* f is measurable on the sigma-algebra generated by itself *) -Lemma preimage_class_measurable_fun d (aT : pointedType) (rT : measurableType d) - (D : set aT) (f : aT -> rT) : - measurable_fun (D : set (g_sigma_algebraType (preimage_class D f measurable))) f. +Lemma preimage_set_system_measurable_fun d (aT : pointedType) + (rT : measurableType d) (D : set aT) (f : aT -> rT) : + measurable_fun + (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. -Lemma sigma_algebra_preimage_class (aT rT : Type) (G : set (set rT)) +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_class D f G). + sigma_algebra setT G -> sigma_algebra D (preimage_set_system D f G). Proof. case=> h0 hC hU; split; first by exists set0 => //; rewrite preimage_set0 setI0. -- move=> A; rewrite /preimage_class /= => -[B mB <-{A}]. +- move=> A; rewrite /preimage_set_system /= => -[B mB <-{A}]. exists (~` B); first by rewrite -setTD; exact: hC. rewrite predeqE => x; split=> [[Dx Bfx]|[Dx]]; first by split => // -[] _ /Bfx. by move=> /not_andP[]. -- move=> F; rewrite /preimage_class /= => mF. +- move=> F; rewrite /preimage_set_system /= => mF. have {}mF n : exists x, G x /\ D `&` f @^-1` x = F n. by have := mF n => -[B mB <-]; exists B. have [F' mF'] := @choice _ _ (fun x y => G y /\ D `&` f @^-1` y = F x) mF. @@ -1723,15 +1726,15 @@ case=> h0 hC hU; split; first by exists set0 => //; rewrite preimage_set0 setI0. exact: (mF' i).2. Qed. -Definition image_class (aT rT : Type) (D : set aT) (f : aT -> rT) +Definition image_set_system (aT rT : Type) (D : set aT) (f : aT -> rT) (G : set (set aT)) : set (set rT) := [set B : set rT | G (D `&` f @^-1` B)]. -Lemma sigma_algebra_image_class (aT rT : Type) (D : set aT) (f : aT -> rT) +Lemma sigma_algebra_image (aT rT : Type) (D : set aT) (f : aT -> rT) (G : set (set aT)) : - sigma_algebra D G -> sigma_algebra setT (image_class D f G). + sigma_algebra D G -> sigma_algebra setT (image_set_system D f G). Proof. -move=> [G0 GC GU]; split; rewrite /image_class. +move=> [G0 GC GU]; split; rewrite /image_set_system. - by rewrite /= preimage_set0 setI0. - move=> A /= GfAD; rewrite setTD -preimage_setC -setDE. rewrite (_ : _ `\` _ = D `\` (D `&` f @^-1` A)); first exact: GC. @@ -1741,47 +1744,60 @@ move=> [G0 GC GU]; split; rewrite /image_class. - by move=> F /= mF; rewrite preimage_bigcup setI_bigcupr; exact: GU. Qed. -Lemma sigma_algebra_preimage_classE aT (rT : pointedType) (D : set aT) +Lemma g_sigma_preimageE aT (rT : pointedType) (D : set aT) (f : aT -> rT) (G' : set (set rT)) : - <> = - preimage_class D f (G'.-sigma.-measurable). + <> = + preimage_set_system D f (G'.-sigma.-measurable). Proof. rewrite eqEsubset; split. have mG : sigma_algebra D - (preimage_class D f (G'.-sigma.-measurable)). - exact/sigma_algebra_preimage_class/sigma_algebra_measurable. - have subset_preimage : preimage_class D f G' `<=` - preimage_class D f (G'.-sigma.-measurable). - by move=> A [B CCB <-{A}]; exists B => //; apply: sub_sigma_algebra. + (preimage_set_system D f (G'.-sigma.-measurable)). + exact/sigma_algebra_preimage/sigma_algebra_measurable. + have subset_preimage : preimage_set_system D f G' `<=` + preimage_set_system D f (G'.-sigma.-measurable). + by move=> A [B CCB <-{A}]; exists B => //; exact: sub_sigma_algebra. exact: smallest_sub. -have G'pre A' : G' A' -> (preimage_class D f G') (D `&` f @^-1` A'). +have G'pre A' : G' A' -> (preimage_set_system D f G') (D `&` f @^-1` A'). by move=> ?; exists A'. -pose I : set (set aT) := <>. -have G'sfun : G' `<=` image_class D f I. +pose I : set (set aT) := <>. +have G'sfun : G' `<=` image_set_system D f I. by move=> A' /G'pre[B G'B h]; apply: sub_sigma_algebra; exists B. -have sG'sfun : <> `<=` image_class D f I. - apply: smallest_sub => //; apply: sigma_algebra_image_class. +have sG'sfun : <> `<=` image_set_system D f I. + apply: smallest_sub => //; apply: sigma_algebra_image. exact: smallest_sigma_algebra. by move=> _ [B mB <-]; exact: sG'sfun. Qed. Lemma measurability d d' (aT : measurableType d) (rT : measurableType d') (D : set aT) (f : aT -> rT) (G : set (set rT)) : - @measurable _ rT = <> -> preimage_class 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_class D f (@measurable _ rT) `<=` @measurable _ aT. +suff h : preimage_set_system D f (@measurable _ rT) `<=` @measurable _ aT. by move=> A mA; apply: h; exists A. -have -> : preimage_class D f (@measurable _ rT) = - <>. - by rewrite [in LHS]sG_rT [in RHS]sigma_algebra_preimage_classE. +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. Qed. End measurability. +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `preimage_set_system`")] +Notation preimage_class := preimage_set_system (only parsing). +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `image_set_system`")] +Notation image_class := image_set_system (only parsing). +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `preimage_set_system_measurable_fun`")] +Notation preimage_class_measurable_fun := preimage_set_system_measurable_fun (only parsing). +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `sigma_algebra_preimage`")] +Notation sigma_algebra_preimage_class := sigma_algebra_preimage (only parsing). +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `sigma_algebra_image`")] +Notation sigma_algebra_image_class := sigma_algebra_image (only parsing). + +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `g_sigma_preimageE`")] +Notation sigma_algebra_preimage_classE := g_sigma_preimageE (only parsing). Local Open Scope ereal_scope. @@ -4755,11 +4771,11 @@ have G_E n : G_ n = [set g n `&` C | C in G]. by move=> X [GX Xgn] /=; exists X => //; rewrite setIidr. by rewrite /G_ => X [Y GY <-{X}]; split; [exact: setIG|apply: subIset; left]. have gIsGE n : [set g n `&` A | A in <>] = - <>. - rewrite sigma_algebra_preimage_classE eqEsubset; split. + <>. + rewrite g_sigma_preimageE eqEsubset; split. by move=> _ /= [Y sGY <-]; exists Y => //; rewrite preimage_id setIC. by move=> _ [Y mY <-] /=; exists Y => //; rewrite preimage_id setIC. -have preimg_gGE n : preimage_class (g n) id G = G_ n. +have preimg_gGE n : preimage_set_system (g n) id G = G_ n. rewrite eqEsubset; split => [_ [Y GY <-]|]. by rewrite preimage_id G_E /=; exists Y => //; rewrite setIC. by move=> X [GX Xgn]; exists X => //; rewrite preimage_id setIidr. @@ -5009,21 +5025,24 @@ Qed. End completed_measure_extension. -Definition preimage_classes d1 d2 +Definition g_sigma_preimageU d1 d2 (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). Section product_lemma. Context d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2). Variables (T : pointedType) (f1 : T -> T1) (f2 : T -> T2). Variables (T3 : Type) (g : T3 -> T). -Lemma preimage_classes_comp : preimage_classes (f1 \o g) (f2 \o g) = - preimage_class setT g (preimage_classes f1 f2). +Lemma g_sigma_preimageU_comp : g_sigma_preimageU (f1 \o g) (f2 \o g) = + preimage_set_system setT g (g_sigma_preimageU f1 f2). Proof. -rewrite {1}/preimage_classes -sigma_algebra_preimage_classE; congr (<>). +rewrite {1}/g_sigma_preimageU -g_sigma_preimageE; congr (<>). rewrite predeqE => C; split. - move=> [[A mA <-{C}]|[A mA <-{C}]]. + by exists (f1 @^-1` A) => //; left; exists A => //; rewrite setTI. @@ -5034,6 +5053,9 @@ rewrite predeqE => C; split. Qed. End product_lemma. +#[deprecated(since="mathcomp-analysis 1.9.0", + note="renamed to `g_sigma_preimageU_comp`")] +Notation preimage_classes_comp := g_sigma_preimageU_comp (only parsing). Definition measure_prod_display : (measure_display * measure_display) -> measure_display. @@ -5044,21 +5066,22 @@ Context d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2). Let f1 := @fst T1 T2. Let f2 := @snd T1 T2. -Let prod_salgebra_set0 : preimage_classes f1 f2 (set0 : set (T1 * T2)). +Let prod_salgebra_set0 : g_sigma_preimageU f1 f2 (set0 : set (T1 * T2)). Proof. exact: sigma_algebra0. Qed. -Let prod_salgebra_setC A : preimage_classes f1 f2 A -> - preimage_classes f1 f2 (~` A). +Let prod_salgebra_setC A : g_sigma_preimageU f1 f2 A -> + g_sigma_preimageU f1 f2 (~` A). Proof. exact: sigma_algebraC. Qed. -Let prod_salgebra_bigcup (F : _^nat) : (forall i, preimage_classes f1 f2 (F i)) -> - preimage_classes f1 f2 (\bigcup_i (F i)). +Let prod_salgebra_bigcup (F : _^nat) : + (forall i, g_sigma_preimageU f1 f2 (F i)) -> + g_sigma_preimageU f1 f2 (\bigcup_i (F i)). Proof. exact: sigma_algebra_bigcup. Qed. HB.instance Definition _ := Pointed.on (T1 * T2)%type. HB.instance Definition prod_salgebra_mixin := @isMeasurable.Build (measure_prod_display (d1, d2)) - (T1 * T2)%type (preimage_classes f1 f2) + (T1 * T2)%type (g_sigma_preimageU f1 f2) (prod_salgebra_set0) (prod_salgebra_setC) (prod_salgebra_bigcup). End product_salgebra_instance. @@ -5093,14 +5116,14 @@ Proof. rewrite eqEsubset; split. apply: smallest_sub; first exact: smallest_sigma_algebra. rewrite subUset; split. - - have /subset_trans : preimage_class setT fst M1 `<=` M1xM2. + - 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_class setT snd M2 `<=` M1xM2. + - 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 MA] [B MB] <-; apply: measurableX => //; exact: sub_sigma_algebra. +by move=> _ [A ?] [B ?] <-; apply: measurableX => //; exact: sub_sigma_algebra. Qed. End product_salgebra_algebraOfSetsType. @@ -5145,8 +5168,8 @@ Context d d1 d2 (T : measurableType d) (T1 : measurableType d1) Lemma prod_measurable_funP (h : T -> T1 * T2) : measurable_fun setT h <-> measurable_fun setT (fst \o h) /\ measurable_fun setT (snd \o h). Proof. -apply: (@iff_trans _ (preimage_classes (fst \o h) (snd \o h) `<=` measurable)). -- rewrite preimage_classes_comp; split=> [mf A [C HC <-]|f12]; first exact: mf. +apply: (@iff_trans _ (g_sigma_preimageU (fst \o h) (snd \o h) `<=` measurable)). +- rewrite g_sigma_preimageU_comp; split=> [mf A [C HC <-]|f12]; first exact: mf. by move=> _ A mA; apply: f12; exists A. - split => [h12|[mf1 mf2]]. split => _ A mA; apply: h12; apply: sub_sigma_algebra; @@ -5229,6 +5252,27 @@ End partial_measurable_fun. #[global] Hint Extern 0 (measurable_fun _ (pair^~ _)) => solve [apply: measurable_pair2] : core. +Section measurable_section. +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). + +Lemma measurable_xsection (A : set (T1 * T2)) (x : T1) : + measurable A -> measurable (xsection A x). +Proof. +move=> mA; pose i (y : T2) := (x, y). +have mi : measurable_fun setT i by exact: measurable_pair1. +by rewrite xsectionE -[X in measurable X]setTI; exact: mi. +Qed. + +Lemma measurable_ysection (A : set (T1 * T2)) (y : T2) : + measurable A -> measurable (ysection A y). +Proof. +move=> mA; pose i (x : T1) := (x, y). +have mi : measurable_fun setT i by exact: measurable_pair2. +by rewrite ysectionE -[X in measurable X]setTI; exact: mi. +Qed. + +End measurable_section. + Section absolute_continuity. Context d (T : semiRingOfSetsType d) (R : realType). Implicit Types m : set T -> \bar R. diff --git a/theories/numfun.v b/theories/numfun.v index 4a81ae2aa..acb61398b 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -381,7 +381,7 @@ Lemma xsection_indic (R : ringType) T1 T2 (A : set (T1 * T2)) x : xsection A x = (fun y => (\1_A (x, y) : R)) @^-1` [set 1]. Proof. apply/seteqP; split => [y/mem_set/=|y/=]; rewrite indicE. -by rewrite mem_xsection => ->. + by rewrite mem_xsection => ->. by rewrite /xsection/=; case: (_ \in _) => //= /esym/eqP /[!oner_eq0]. Qed. @@ -389,7 +389,7 @@ Lemma ysection_indic (R : ringType) T1 T2 (A : set (T1 * T2)) y : ysection A y = (fun x => (\1_A (x, y) : R)) @^-1` [set 1]. Proof. apply/seteqP; split => [x/mem_set/=|x/=]; rewrite indicE. -by rewrite mem_ysection => ->. + by rewrite mem_ysection => ->. by rewrite /ysection/=; case: (_ \in _) => //= /esym/eqP /[!oner_eq0]. Qed.