diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d7f0405803..ab374cb110 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,26 +10,53 @@ `pownMexpr_cvgn0` + instance `is_derive1_powRl` -### Changed +- in `function_spaces.v`: + + lemma `within_continuous_big` + +- in `nat_topology.v`: + + lemma `near_infty_after` + +- in `num_topology.v`: + + lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, + `at_left_shift`, `at_right_shift` -- in `lebesgue_integral_nonneg.v`, generalized and deprecated: - + lemma `ge0_integralZl_EFin` (no condition on `k`) -- in file `function_spaces.v`, - + new lemma `within_continuous_big`. -- in file `nat_topology.v`, - + new lemma `near_infty_after`. -- in file `num_topology.v`, - + new lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, - `at_left_shift`, and `at_right_shift`. - in `realfun.v`: + lemmas `derivable_oo_LRcontinuousZ`, `derivable_oo_LRcontinuousD`, `derivable_oo_LRcontinuousN`, `derivable_oo_LRcontinuous_shift`, `derivable_oo_LRcontinuousS` +- in `metric_structure.v`: + + lemma `set1_bigcap_ball` + +- file `normedtype_measurable.v` + + definition `borel_type` + + definition `borel_display` + + module `MeasurableNormedModuleOpen` + * lemma `measurable_set1` + * lemma `measurable_ball_norm` + * lemma ` measurable_funP1` + ### Changed +- in `lebesgue_integral_nonneg.v`, generalized and deprecated: + + lemma `ge0_integralZl_EFin` (no condition on `k`) + +- from `lebesgue_stieltjes_measure.v` to (new) `normedtyped_measurable.v`: + + move definition `open_type` + + move notations `.-open`, `.-open.-measurable` + +- in `lebesgue_stieltjes_measure.v`: + + sigma-algebra for `\bar R` now uses open sets instead of octiv + ### Renamed +- in `lebesgue_stieltjes_measure.v`: + + `RGenOpens` -> `RGenItvoo` + + `MeasurableRocitv.measurable_set1` -> `MeasurableRocitv.ocitv_measurable_set1` + + `MeasurableRocitv.measurable_itv` -> `MeasurableRocitv.ocitv_measurable_itv` + +- in `lebesgue_stieltjes_measure.v`: + ### Generalized - in `lebesgue_integral_nonneg.v`: @@ -39,6 +66,10 @@ ### Removed +- in `lebesgue_stieltjes_measure.v`: + + definition `MeasurableRocitv.lebesgue_display` + + definition `MeasurableRocitv.measurableR` + ### Infrastructure ### Misc diff --git a/_CoqProject b/_CoqProject index 0dcbd12ffa..20e376835e 100644 --- a/_CoqProject +++ b/_CoqProject @@ -116,6 +116,7 @@ theories/measure_theory/measurable_function.v theories/measure_theory/signed_measure.v theories/measure_theory/measure.v +theories/real_measure/normedtype_measurable.v theories/real_measure/lebesgue_stieltjes_measure.v theories/real_measure/lebesgue_measure.v theories/real_measure/measurable_realfun.v diff --git a/theories/Make b/theories/Make index 15781fc7db..b228cf3b83 100644 --- a/theories/Make +++ b/theories/Make @@ -83,6 +83,7 @@ measure_theory/measurable_function.v measure_theory/signed_measure.v measure_theory/measure.v +real_measure/normedtype_measurable.v real_measure/lebesgue_stieltjes_measure.v real_measure/lebesgue_measure.v real_measure/measurable_realfun.v diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v index 41a86b07f3..ab9855cd3d 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v @@ -58,7 +58,7 @@ Section continuous_compact_integrable. Context {rT : realType}. Let mu : measure _ _ := @lebesgue_measure rT. Import MeasurableR. -Let R : measurableType _ := measurableTypeR rT. +Let R : measurableType _ := (*measurableTypeR*) rT. Local Open Scope ereal_scope. Lemma continuous_compact_integrable (f : R -> R^o) (A : set R^o) : @@ -78,7 +78,7 @@ Section continuous_density_L1. Context (rT : realType). Let mu : measure _ _ := @lebesgue_measure rT. Import MeasurableR. -Let R : measurableType _ := measurableTypeR rT. +Let R : measurableType _ := (*measurableTypeR*) rT. Local Open Scope ereal_scope. Import HBSimple. @@ -180,7 +180,7 @@ Section lebesgue_differentiation_continuous. Context {rT : realType}. Let mu : measure _ _ := @lebesgue_measure rT. Import MeasurableR. -Let R : measurableType _ := measurableTypeR rT. +Let R : measurableType _ := (*measurableTypeR*) rT. Let ballE (x : R) (r : {posnum rT}) : ball x r%:num = `](x - r%:num), (x + r%:num)[%classic :> set rT. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index a4af3f425b..c142c7979c 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -557,7 +557,7 @@ Local Notation mu := lebesgue_measure. Import MeasurableR. Lemma lebesgue_measureN (A : set R) : measurable A -> - pushforward mu (-%R : _ -> measurableTypeR R) A = mu A. + pushforward mu (-%R : _ -> (*measurableTypeR*) R) A = mu A. Proof. move=> mA; apply/esym/lebesgue_measure_unique => //= _ [[a b]] _ <-. rewrite /pushforward opp_preimage_itvbndbnd/= !lebesgue_measure_itv/=. @@ -569,7 +569,7 @@ Lemma ge0_integration_by_substitution0 (f : R -> \bar R) : \int[mu]_(r in `[0%R, +oo[) f r = \int[mu]_(r in `]-oo, 0%R]) f (- r)%R. Proof. move=> mf f0; rewrite (_ : `]-oo, 0%R]%classic = - (-%R : _ -> measurableTypeR R) @^-1` `[0%R, +oo[). + (-%R : _ -> (*measurableTypeR*) R) @^-1` `[0%R, +oo[). by rewrite opp_preimage_itvbndy oppr0. rewrite -ge0_integral_pushforward//=; first exact: measurable_funS mf. by apply: eq_measure_integral => //= A mA AS; exact/esym/lebesgue_measureN. @@ -1068,7 +1068,7 @@ End integral_patch. Section ge0_cvgn_integral. Local Open Scope ereal_scope. Import MeasurableR. -Context {R : realType} (mu : {measure set (@measurableTypeR R) -> \bar R}) +Context {R : realType} (mu : {measure set ((*@measurableTypeR*) R) -> \bar R}) (f : R -> R). Hypothesis f0 : (forall x, 0 <= f x)%R. diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v index cc5f2ab413..8794f07ef1 100644 --- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v +++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v @@ -703,7 +703,7 @@ Hint Extern 0 (hausdorff_space _) => (exact: Rhausdorff) : core. Local Open Scope ereal_scope. Context (rT : realType) (A : set rT). Let mu : measure _ _ := @lebesgue_measure rT. -Let R : measurableType _ := measurableTypeR rT. +Let R : measurableType _ := rT(*measurableTypeR rT*). Hypothesis mA : measurable A. Hypothesis finA : mu A < +oo. diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index efebbbfa82..bcd8f48fef 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -381,7 +381,7 @@ Context {R : realType} (f : cumulativeBounded (0:R) (1:R)). Local Open Scope measure_display_scope. Import MeasurableR. -Let idTR : measurableTypeR R -> R := idfun. +Let idTR : (*measurableTypeR*) R -> R := idfun. #[local] HB.instance Definition _ := @isMeasurableFun.Build _ _ _ _ idTR (@measurable_id _ _ setT). @@ -410,10 +410,10 @@ End cdf_of_lebesgue_stieltjes_measure. Section lebesgue_stieltjes_measure_of_cdf. Import MeasurableR. -Context {R : realType} (P : probability (measurableTypeR R) R). +Context {R : realType} (P : probability ((*measurableTypeR*) R) R). Local Open Scope measure_display_scope. -Let idTR : measurableTypeR R -> R := idfun. +Let idTR : (*measurableTypeR*) R -> R := idfun. #[local] HB.instance Definition _ := @isMeasurableFun.Build _ _ _ _ idTR (@measurable_id _ _ setT). @@ -626,7 +626,7 @@ Let mu : {measure set _ -> \bar R} := @lebesgue_measure R. Lemma ge0_expectation_ccdf (X : {RV P >-> R}) : (forall x, 0 <= X x)%R -> 'E_P[X] = \int[mu]_(r in `[0%R, +oo[) ccdf X r. Proof. -pose GR := measurableTypeR R. +pose GR := (*measurableTypeR*) R. pose distrX := distribution P X. pose D : set R := `[0%R, +oo[%classic. move=> X_ge0. diff --git a/theories/real_measure/lebesgue_measure.v b/theories/real_measure/lebesgue_measure.v index 246eff542f..110626a7af 100644 --- a/theories/real_measure/lebesgue_measure.v +++ b/theories/real_measure/lebesgue_measure.v @@ -8,7 +8,8 @@ From mathcomp Require Import boolp classical_sets functions cardinality fsbigop reals. From mathcomp Require Import topology ereal numfun normedtype sequences esum measure. -From mathcomp Require Export lebesgue_stieltjes_measure measurable_realfun. +From mathcomp Require Export normedtype_measurable lebesgue_stieltjes_measure + measurable_realfun. (**md**************************************************************************) (* # Lebesgue Measure *) @@ -572,9 +573,7 @@ apply: (@measure_semi_sigma_additive _ _ _ (@lebesgue_measure R) move=> [X mX [X' mX']] XX'Fn. apply: measurable_image_fine. rewrite -XX'Fn. - apply: measurableU. - apply: measurable_image_EFin. - by rewrite RGenOpenSets.measurableE/= in mX. + apply: measurableU; first exact: measurable_image_EFin. by case: mX' => //; exact: measurableU. - move=> i j _ _ [x [[a [Fia aoo ax] [b [Fjb boo] bx]]]]. move: tF => /(_ i j Logic.I Logic.I); apply. @@ -591,17 +590,16 @@ apply: (@measure_semi_sigma_additive _ _ _ (@lebesgue_measure R) + by rewrite not_orP => -[]/(_ erefl). + by rewrite not_orP => -[]/(_ erefl). - move: mUF. - rewrite {1}/measurable /emeasurable /= => -[X mX [Y []]] {Y}; - have moX : measurable X by rewrite -RGenOpenSets.measurableE. + rewrite {1}/measurable /emeasurable /= => -[X mX [Y []]] {Y}. + rewrite setU0 => h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. + rewrite [X in measurable X](_ : _ = X)// predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-{r}]]]. have : (\bigcup_n F n) x by exists n. by rewrite -h => -[x' Xx' <-]. have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; exists r. by exists n => //; exists r%:E => //; split => // -[]. + move=> h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. + rewrite [X in measurable X](_ : _ = X)// predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-]]]. have : (\bigcup_n F n) x by exists n. by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[]. @@ -609,14 +607,14 @@ apply: (@measure_semi_sigma_additive _ _ _ (@lebesgue_measure R) by exists n => //; exists r%:E => //; split => // -[]. + (* NB: almost the same as the previous one, factorize?*) move=> h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. + rewrite [X in measurable X](_ : _ = X)// predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-]]]. have : (\bigcup_n F n) x by exists n. by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[]. have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. by exists n => //; exists r%:E => //; split => // -[]. + move=> h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. + rewrite [X in measurable X](_ : _ = X)// predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-]]]. have : (\bigcup_n F n) x by exists n. by rewrite -h => -[[x' Xx' <-//]|]. diff --git a/theories/real_measure/lebesgue_stieltjes_measure.v b/theories/real_measure/lebesgue_stieltjes_measure.v index 0ddbb8bffd..2baa90cfc8 100644 --- a/theories/real_measure/lebesgue_stieltjes_measure.v +++ b/theories/real_measure/lebesgue_stieltjes_measure.v @@ -1,12 +1,12 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import boot order finmap ssralg ssrnum ssrint interval. +From mathcomp Require Import boot order finmap ssralg ssrnum ssrint algebra interval. From mathcomp Require Import interval_inference archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets fsbigop cardinality. From mathcomp Require Import reals ereal topology normedtype sequences esum - measure realfun. + measure realfun normedtype_measurable. (**md**************************************************************************) (* # Lebesgue Stieltjes Measure *) @@ -30,7 +30,7 @@ From mathcomp Require Import reals ereal topology normedtype sequences esum (* The HB class is CumulativeBounded. *) (* ``` *) (* *) -(* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens, ROpenSets *) +(* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenItvoo, ROpenSets *) (* provide proofs of equivalence between the sigma-algebra generated by *) (* open-closed intervals and the sigma-algebras generated by open rays, *) (* closed rays, open intervals, and open sets. *) @@ -43,7 +43,6 @@ From mathcomp Require Import reals ereal topology normedtype sequences esum (* x and y are real numbers *) (* R.-ocitv == display for ocitv_type R *) (* R.-ocitv.-measurable == semiring of sets of open-closed intervals *) -(* open_type R == alias for R : realType *) (* R.-open := sigma_display (@open R) *) (* R.-open.-measurable == sigma-algebra generated by open sets *) (* ``` *) @@ -54,9 +53,7 @@ From mathcomp Require Import reals ereal topology normedtype sequences esum (* measurableTypeR R == measurableType generated by *) (* R.-ocitv or R.-open *) (* @lebesgue_display R == (measure_)display for the sigma-algebra *) -(* generated by R.-ocitv or R.-open *) -(* @measurableR R == measurable sets generated by *) -(* R.-ocitv or R.-open *) +(* generated by R.-open *) (* ``` *) (* The module `MeasurableR` contains the default sigma-algebra, which is *) (* `MeasurableRopen`. The latter contains in addition: *) @@ -97,9 +94,6 @@ Local Open Scope ring_scope. Reserved Notation "R .-ocitv" (at level 1, format "R .-ocitv"). Reserved Notation "R .-ocitv.-measurable" (at level 2, format "R .-ocitv.-measurable"). -Reserved Notation "R .-open" (at level 1, format "R .-open"). -Reserved Notation "R .-open.-measurable" - (at level 2, format "R .-open.-measurable"). Notation right_continuous f := (forall x, f%function @ at_right x --> f%function x). @@ -167,11 +161,11 @@ Definition ocitv := [set `]x.1, x.2]%classic | x in [set: R * R]]. Lemma is_ocitv a b : ocitv `]a, b]%classic. Proof. by exists (a, b); split => //=; rewrite in_itv/= andbT. Qed. -Hint Extern 0 (ocitv _) => solve [apply: is_ocitv] : core. +#[local] Hint Extern 0 (ocitv _) => solve [apply: is_ocitv] : core. Lemma ocitv0 : ocitv set0. Proof. by exists (1, 0); rewrite //= set_itv_ge ?bnd_simp//= ltr10. Qed. -Hint Resolve ocitv0 : core. +#[local] Hint Resolve ocitv0 : core. Lemma ocitvP X : ocitv X <-> X = set0 \/ exists2 x, x.1 < x.2 & X = `]x.1, x.2]%classic. Proof. @@ -234,41 +228,40 @@ Context {R : realType}. Definition measurableTypeR := g_sigma_algebraType (@ocitv R). -Definition lebesgue_display : measure_display := (@ocitv R).-sigma. +Let ocitv_lebesgue_display : measure_display := (@ocitv R).-sigma. -Definition measurableR : set_system R := (@ocitv R).-sigma.-measurable. +Let measurableR : set_system R := (@ocitv R).-sigma.-measurable. -HB.instance Definition _ : Measurable lebesgue_display measurableTypeR := +HB.instance Definition _ : Measurable ocitv_lebesgue_display measurableTypeR := Measurable.on measurableTypeR. (* Presumably it is safe to use NFI here because morally R is unique and nothing else can be used here *) #[non_forgetful_inheritance] HB.instance Definition _ := Measurable.copy R measurableTypeR. -Lemma measurable_set1 (r : R) : measurable [set r]. +Lemma ocitv_measurable_set1 (r : R) : measurable [set r]. Proof. rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _. by apply: sub_sigma_algebra; exact/is_ocitv. Qed. -#[local] Hint Resolve measurable_set1 : core. +#[local] Hint Resolve ocitv_measurable_set1 : core. -Lemma measurable_itv (i : interval R) : measurable [set` i]. +Lemma ocitv_measurable_itv (i : interval R) : measurable [set` i]. Proof. have moc (a b : R) : measurable `]a, b]. - by apply: sub_sigma_algebra; apply: is_ocitv. + by apply: sub_sigma_algebra; exact: is_ocitv. have mopoo (x : R) : measurable `]x, +oo[. by rewrite itv_bndy_bigcup_BRight; exact: bigcup_measurable. have mnooc (x : R) : measurable `]-oo, x]. by rewrite -setCitvr; exact/measurableC. -have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b. - by rewrite setDitv1r. +have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b by rewrite setDitv1r. have moo (a b : R) : measurable `]a, b[ by rewrite ooE; exact: measurableD. have mcc (a b : R) : measurable `[a, b]. case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge. - by rewrite -setU_1itvob//; apply/measurableU. + by rewrite -setU_1itvob//; exact/measurableU. have mco (a b : R) : measurable `[a, b[. case: (boolP (a < b)) => ab; last by rewrite set_itv_ge. - by rewrite -setU_1itvob//; apply/measurableU. + by rewrite -setU_1itvob//; exact/measurableU. have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b. by rewrite setDitv1r. case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge. @@ -279,13 +272,6 @@ Qed. End measurableRocitv. Arguments measurableTypeR : clear implicits. -#[global] -Hint Extern 0 (measurable (_ @^-1` [set _])) => - solve [apply: measurable_funPTI; exact: measurable_set1] : core. -#[global] -Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. -#[global] -Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. End MeasurableRocitv. Module RGenOInfty. @@ -317,7 +303,8 @@ Proof. rewrite eqEsubset; split => A. apply: smallest_sub; first exact: smallest_sigma_algebra. by move=> I [x _ <-]; exact: measurable_itv_bounded. -by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. +apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. +exact: MeasurableRocitv.ocitv_measurable_itv. Qed. End rgenoinfty. @@ -353,7 +340,8 @@ Proof. rewrite eqEsubset; split => A. apply: smallest_sub; first exact: smallest_sigma_algebra. by move=> I [x _ <-]; exact: measurable_itv_bounded. -by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. +apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. +exact: MeasurableRocitv.ocitv_measurable_itv. Qed. End rgeninftyo. @@ -388,13 +376,14 @@ Proof. rewrite eqEsubset; split => A. apply: smallest_sub; first exact: smallest_sigma_algebra. by move=> I [x _ <-]; exact: measurable_itv_bounded. -by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. +apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. +exact: MeasurableRocitv.ocitv_measurable_itv. Qed. End rgencinfty. End RGenCInfty. -Module RGenOpens. +Module RGenItvoo. Section rgenopens. Context (R : realType). Implicit Types x y z : R. @@ -437,11 +426,12 @@ Proof. rewrite eqEsubset; split => A. apply: smallest_sub; first exact: smallest_sigma_algebra. by move=> I [x _ <-]; exact: measurable_itv_bounded. -by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x [y ->]]]. +apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x [y ->]]]. +exact: MeasurableRocitv.ocitv_measurable_itv. Qed. End rgenopens. -End RGenOpens. +End RGenItvoo. Module RGenOpenSets. Section rgenopensets. @@ -451,98 +441,49 @@ Import MeasurableRocitv. Lemma measurableE : (@ocitv R).-sigma.-measurable = open.-sigma.-measurable. Proof. -rewrite eqEsubset; split; [rewrite RGenOpens.measurableE|]; +rewrite eqEsubset; split; [rewrite RGenItvoo.measurableE|]; apply: sigma_algebra_subl=> U. -- by rewrite /RGenOpens.G/= => -[a [b ->]]; exact: sub_sigma_algebra. +- by rewrite /RGenItvoo.G/= => -[a [b ->]]; exact: sub_sigma_algebra. - move=> oU; rewrite (open_disjoint_itv_bigcup oU). apply: sigma_algebra_bigcup => k. have /is_intervalP -> := @open_disjoint_itv_is_interval _ U oU k. - exact: measurable_itv. + exact: ocitv_measurable_itv. Qed. End rgenopensets. End RGenOpenSets. -Section open. +Module MeasurableROpen. +Section measurableReal. Context {R : realType}. +Import numFieldNormedType.Exports. -Definition open_type : Type := R. - -HB.instance Definition _ := Pointed.on open_type. - -Let measurable : set_system R := @measurable _ (g_sigma_algebraType (@open R)). - -Let measurable0 : measurable set0. Proof. exact: measurable0. Qed. - -Let measurableC A : measurable A -> measurable (~` A). -Proof. by move=> /measurableC. Qed. - -Let measurable_bigcup (F : (set R)^nat) : (forall i, measurable (F i)) -> - measurable (\bigcup_i (F i)). -Proof. move=> mF; exact: bigcupT_measurable. Qed. - -HB.instance Definition _ := - @isMeasurable.Build (sigma_display (@open R)) - open_type measurable measurable0 measurableC measurable_bigcup. +Import MeasurableNormedModule. -End open. +Definition lebesgue_display : measure_display := @borel_display R R. -Notation "R .-open" := (sigma_display (@open R)) : measure_display_scope. -Notation "R .-open.-measurable" := (measurable : set_system (@open_type R)) : - classical_set_scope. - -Module MeasurableRopen. -Section measurableRopen. -Context {R : realType}. - -Definition measurableTypeR := g_sigma_algebraType (@open R). - -Definition lebesgue_display : measure_display := R.-open. - -Definition measurableR : set_system R := R.-open.-measurable. - -HB.instance Definition _ : Measurable lebesgue_display measurableTypeR := - Measurable.on measurableTypeR. -(* Presumably it is safe to use NFI here because morally R is unique - and nothing else can be used here *) #[non_forgetful_inheritance] -HB.instance Definition _ := Measurable.copy R measurableTypeR. - -Lemma measurable_set1 (r : R) : measurable [set r]. -Proof. -rewrite set1_bigcap_oo; apply: bigcap_measurable => // k _. -exact: sub_sigma_algebra. -Qed. -#[local] Hint Resolve measurable_set1 : core. +HB.instance Definition _ := Measurable.copy R (g_sigma_algebraType (@open R)). Lemma measurable_itv (i : interval R) : measurable [set` i]. Proof. -have := MeasurableRocitv.measurable_itv i. -rewrite /MeasurableRocitv.lebesgue_display. -by rewrite RGenOpenSets.measurableE. +by rewrite -RGenOpenSets.measurableE; exact: MeasurableRocitv.ocitv_measurable_itv. Qed. -End measurableRopen. -Arguments measurableTypeR : clear implicits. -#[global] -Hint Extern 0 (measurable (_ @^-1` [set _])) => - solve [apply: measurable_funPTI; exact: measurable_set1] : core. -#[global] -Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. -#[global] -Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. - -Lemma measurable_funP1 {d} {aT : measurableType d} {rT : realType} - (f : {mfun aT >-> rT}) D (y : rT) : - measurable D -> measurable (D `&` f @^-1` [set y]). -Proof. by move=> /(measurable_funP f); exact. Qed. -#[deprecated(since="mathcomp-analysis 1.13.0", use=measurable_funP1)] -Notation measurable_sfun_inP := measurable_funP1 (only parsing). -#[global] Hint Extern 0 (measurable (_ `&` _ @^-1` [set _])) => - solve [apply: measurable_funP1; assumption] : core. +End measurableReal. +#[global] Hint Extern 0 (measurable [set` _]) => exact: measurable_itv : core. + +End MeasurableROpen. + +Module MeasurableR. +Export numFieldNormedType.Exports. +Export MeasurableNormedModule. +Export MeasurableROpen. +End MeasurableR. Section ocitv_measure. -Context {R : realType} (mu : measure (measurableTypeR R) R). +Import MeasurableR. +Context {R : realType} (mu : {measure set R -> \bar R}). Definition ocitv_measure : set (MeasurableRocitv.measurableTypeR R) -> \bar R := mu. @@ -568,12 +509,6 @@ Lemma ocitv_measure_ext A : ocitv_measure A = mu A. Proof. by []. Qed. End ocitv_measure. -End MeasurableRopen. - -Module MeasurableR. -Export MeasurableRopen. -End MeasurableR. - (** The construction of the Lebesgue-Stieltjes measure actually starts here. *) Section wlength. @@ -784,8 +719,6 @@ HB.instance Definition _ (f : cumulative R R) := (wlength_ge0 f) (wlength_semi_additive f). -Hint Extern 0 (measurable _) => solve [apply: is_ocitv] : core. - Lemma cumulative_content_sub_fsum (f : cumulative R R) (D : {fset nat}) a0 b0 (a b : nat -> R) : (forall i, i \in D -> a i <= b i) -> `]a0, b0] `<=` \big[setU/set0]_(i <- D) `]a i, b i]%classic -> @@ -796,7 +729,8 @@ move=> Dab h; have [ab|ab] := leP a0 b0; last first. by rewrite subr_le0 cumulative_is_nondecreasing// ltW. rewrite big_seq sumr_ge0// => i iD. by rewrite subr_ge0 cumulative_is_nondecreasing// Dab. -have mab k : [set` D] k -> R.-ocitv.-measurable `]a k, b k]%classic by []. +have mab k : [set` D] k -> R.-ocitv.-measurable `]a k, b k]%classic. + by move=> ?; exact: is_ocitv. move: h; rewrite -bigcup_fset. move/(content_sub_fsum (wlength f) (finite_fset D) mab (is_ocitv a0 b0)) => /=. rewrite wlength_itv_bnd// -lee_fin => /le_trans; apply. @@ -884,8 +818,8 @@ Proof. exists (fun k => `](- k%:R), k%:R]%classic). apply/esym; rewrite -subTset => /= x _ /=. by exists (Num.bound x); rewrite //= in_itv/= ltrNl ltrNbound ltW// ltr_bound. -move=> k; split => //; rewrite wlength_itv /= -EFinB. -by case: ifP; rewrite ltey. +move=> k; split; first exact: is_ocitv. +by rewrite wlength_itv /= -EFinB; case: ifP; rewrite ltey. Qed. Definition ocitv_lebesgue_stieltjes_measure (f : cumulative R R) := @@ -950,13 +884,13 @@ Let ocitv_lebesgue_stieltjes_measure_unique Proof. move=> muE A mA. apply: measure_extension_unique => //=. -- exact: wlength_sigma_finite. -- by move=> X mX; rewrite -muE// -measurable_mu_extE. -- by rewrite RGenOpenSets.measurableE. + exact: wlength_sigma_finite. +by move=> X mX; rewrite -muE// -measurable_mu_extE. +by rewrite RGenOpenSets.measurableE. Qed. Lemma lebesgue_stieltjes_measure_unique - (mu : {measure set (MeasurableRopen.measurableTypeR R) -> \bar R}) : + (mu : {measure set R -> \bar R}) : (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) -> forall A : set R, measurable A -> lebesgue_stieltjes_measure f A = mu A. Proof. diff --git a/theories/real_measure/measurable_realfun.v b/theories/real_measure/measurable_realfun.v index 90857b09cf..6534efc8f7 100644 --- a/theories/real_measure/measurable_realfun.v +++ b/theories/real_measure/measurable_realfun.v @@ -7,7 +7,7 @@ From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import reals ereal topology numfun normedtype sequences measure realfun exp. -From mathcomp Require Import lebesgue_stieltjes_measure. +From mathcomp Require Import lebesgue_stieltjes_measure normedtype_measurable. (**md**************************************************************************) (* # Measurable Functions over $\mathbb{R}$ and $\overline{\mathbb{R}}$ *) @@ -45,7 +45,6 @@ From mathcomp Require Import lebesgue_stieltjes_measure. (* ``` *) (******************************************************************************) -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -186,7 +185,7 @@ End puncture_ereal_itv. Section salgebra_R_ssets. Context {R : realType}. -HB.instance Definition _ := (ereal_isMeasurable (R.-ocitv.-measurable)). +HB.instance Definition _ := ereal_isMeasurable (@open R). (* NB: Until we dropped support for Coq 8.12, we were using HB.instance (\bar (Real.sort R)) (ereal_isMeasurable (@measurable (@itvs_semiRingOfSets R))). @@ -205,7 +204,7 @@ Import MeasurableR. Lemma measurable_image_EFin (A : set R) : measurable A -> measurable (EFin @` A). Proof. -move=> mA; exists A; first by rewrite RGenOpenSets.measurableE. +move=> mA; exists A => //. by exists set0; [constructor|rewrite setU0]. Qed. @@ -224,7 +223,7 @@ Let emeasurable_itv_bndy b (y : \bar R) : measurable [set` Interval (BSide b y) +oo%O]. Proof. move: y => [y| |]. -- exists [set` Interval (BSide b y) +oo%O]; first by []. +- exists [set` Interval (BSide b y) +oo%O] => //. by exists [set +oo%E]; [constructor|rewrite -punct_eitv_bndy]. - by case: b; rewrite ?itv_oyy ?itv_cyy. - case: b; first by rewrite itv_cNyy. @@ -249,24 +248,24 @@ Lemma measurable_image_fine (X : set \bar R) : measurable X -> Proof. case => Y mY [X' [ | <-{X} | <-{X} | <-{X} ]]. - rewrite setU0 => <-{X}. - rewrite [X in measurable X](_ : _ = Y) -?RGenOpenSets.measurableE// predeqE => r; split. + rewrite [X in measurable X](_ : _ = Y)// predeqE => r; split. by move=> [x [[x' Yx' <-{x}/= _ <-//]]]. by move=> Yr; exists r%:E; split => [|[]//]; exists r. -- rewrite [X in measurable X](_ : _ = Y) -?RGenOpenSets.measurableE// predeqE => r; split. +- rewrite [X in measurable X](_ : _ = Y)// predeqE => r; split. move=> [x [[[x' Yx' <- _ <-//]|]]]. by move=> <-; rewrite not_orP => -[]/(_ erefl). by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. -- rewrite [X in measurable X](_ : _ = Y) -?RGenOpenSets.measurableE// predeqE => r; split. +- rewrite [X in measurable X](_ : _ = Y)// predeqE => r; split. move=> [x [[[x' Yx' <-{x} _ <-//]|]]]. by move=> ->; rewrite not_orP => -[_]/(_ erefl). by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. -- rewrite [X in measurable X](_ : _ = Y) -?RGenOpenSets.measurableE// predeqE => r; split. +- rewrite [X in measurable X](_ : _ = Y)// predeqE => r; split. by rewrite setDUl setDv setU0 => -[_ [[x' Yx' <-]] _ <-]. by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. Qed. Lemma measurable_ball (x : R) e : measurable (ball x e). -Proof. by rewrite ball_itv -?RGenOpenSets.measurableE//. Qed. +Proof. by rewrite ball_itv. Qed. Lemma measurable_closed_ball (x : R) r : measurable (closed_ball x r). Proof. @@ -444,9 +443,9 @@ rewrite eset1y; apply: bigcapT_measurable => i. by apply: sub_sigma_algebra; exists i%:R. Qed. -Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. +Lemma measurableE : emeasurable (@open R) = G.-sigma.-measurable. Proof. -apply/seteqP; split; last first. +rewrite /emeasurable -RGenOpenSets.measurableE; apply/seteqP; split; last first. apply: smallest_sub. split; first exact: emeasurable0. by move=> *; rewrite setTD; exact: emeasurableC. @@ -497,9 +496,9 @@ apply: bigcap_measurable => // j _; rewrite -setCitvr; apply: measurableC. by apply: sub_sigma_algebra; exists (i%:R + j.+1%:R^-1)%R. Qed. -Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. +Lemma measurableE : emeasurable (@open R) = G.-sigma.-measurable. Proof. -apply/seteqP; split; last first. +rewrite /emeasurable -RGenOpenSets.measurableE; apply/seteqP; split; last first. apply: smallest_sub. split; first exact: emeasurable0. by move=> *; rewrite setTD; exact: emeasurableC. @@ -533,7 +532,7 @@ Context (R : realType). Definition G := [set A : set \bar R | exists r, A = `]-oo, r%:E[%classic]. -Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. +Lemma measurableE : emeasurable (@open R) = G.-sigma.-measurable. Proof. rewrite ErealGenCInfty.measurableE eqEsubset; split => A. apply: smallest_sub; first exact: smallest_sigma_algebra. @@ -551,7 +550,7 @@ End ErealGenInftyO. Lemma is_interval_measurable (R : realType) (I : set R) : is_interval I -> measurable I. -Proof. by move/is_intervalP => ->; rewrite -?RGenOpenSets.measurableE//. Qed. +Proof. by move/is_intervalP => ->. Qed. Section coutinuous_measurable. Context {R : realType}. @@ -582,8 +581,8 @@ Lemma subspace_continuous_measurable_fun (D : set R) (f : subspace D -> R) : measurable D -> continuous f -> measurable_fun D f. Proof. move=> mD /continuousP cf. -rewrite /measurable_fun -?RGenOpenSets.measurableE. -apply: (measurability _ (RGenOpens.measurableE R)). +rewrite /measurable_fun -!RGenOpenSets.measurableE. +apply: (measurability _ (RGenItvoo.measurableE R)). move=> _ [_ [a [b ->] <-]]. rewrite RGenOpenSets.measurableE. apply: open_measurable_subspace => //. @@ -635,7 +634,7 @@ have [x0|x0] := leP 0 x; last first. rewrite [X in measurable X](_ : _ = setT)// predeqE => r. by split => // _; rewrite /= in_itv /= andbT (lt_le_trans x0). rewrite [X in measurable X](_ : _ = `]-oo, (- x)[ `|` `]x, +oo[); last first. - exact: measurableU. + by apply: measurableU => //; exact: MeasurableRocitv.ocitv_measurable_itv. rewrite predeqE => r; split => [|[|]]; rewrite preimage_itv ?in_itv ?andbT/=. - (have [r0|r0] := leP 0 r; [rewrite ger0_norm|rewrite ltr0_norm]) => // xr; rewrite 2!in_itv/=. @@ -1238,7 +1237,7 @@ Lemma EFin_measurable (D : set R) : measurable_fun D EFin. Proof. move=> mD; apply: (measurability _ (ErealGenOInfty.measurableE R)) => //. move=> /= _ [_ [x ->]] <-; apply: measurableI => //. -by rewrite -RGenOpenSets.measurableE preimage_itvoy EFin_itv. +by rewrite preimage_itvoy EFin_itv. Qed. Lemma abse_measurable (D : set (\bar R)) : measurable_fun D abse. @@ -1249,14 +1248,12 @@ rewrite [X in _ @^-1` X](punct_eitv_bndy _ x) preimage_setU setIUr. apply: measurableU; last first. by rewrite preimage_abse_pinfty; apply: measurableI => //; exact: measurableU. apply: measurableI => //; exists (normr @^-1` `]x, +oo[%classic). - rewrite -[X in measurable X]setTI. - rewrite RGenOpenSets.measurableE. - exact: normr_measurable. + by rewrite -[X in measurable X]setTI; exact: normr_measurable. exists set0; first by constructor. rewrite setU0 predeqE => -[y| |]; split => /= => -[r]; rewrite ?/= /= ?in_itv /= ?andbT => xr//. + by move=> [ry]; exists `|y| => //=; rewrite in_itv/= andbT -ry. - + by move=> [ry]; exists y => //=; rewrite /= in_itv/= andbT -ry. + + by move=> [ry]; exists y => //=; rewrite in_itv/= andbT -ry. Qed. Lemma oppe_measurable (D : set (\bar R)) : @@ -1284,7 +1281,6 @@ Proof. split=> [mf mD A mA|]; last by move=> mg; exact: measurableT_comp. rewrite [X in measurable X](_ : _ = D `&` (EFin \o g) @^-1` (EFin @` A)); last first. apply: mf => //; exists A => //. - by rewrite RGenOpenSets.measurableE//. by exists set0; [constructor|rewrite setU0]. congr (_ `&` _);rewrite eqEsubset; split=> [|? []/= _ /[swap] -[->//]]. by move=> ? ?; exact: preimage_image. diff --git a/theories/real_measure/normedtype_measurable.v b/theories/real_measure/normedtype_measurable.v new file mode 100644 index 0000000000..ed642432b8 --- /dev/null +++ b/theories/real_measure/normedtype_measurable.v @@ -0,0 +1,106 @@ +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import boot order algebra. +From mathcomp Require Import boolp classical_sets. +From mathcomp Require Import topology normedtype measure. + +(**md**************************************************************************) +(* # Sigma-algebra for normed modules *) +(* *) +(* `borel_type N` *) +(* : alias for `N : normedModType R` *) +(* *) +(* `borel_display N` *) +(* : display for `borel_type N` *) +(* *) +(* `N .-open.-measurable` *) +(* : the set of measurable sets *) +(* *) +(* `MeasurableNormedModule` *) +(* : module that contains the definition of a sigma-algebra for normed *) +(* : modules *) +(* *) +(******************************************************************************) + +Reserved Notation "R .-open" (at level 1, format "R .-open"). +Reserved Notation "R .-open.-measurable" + (at level 2, format "R .-open.-measurable"). + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Section open. +Context {R : numFieldType} {N : normedModType R}. + +Definition borel_type : Type := N. + +Definition borel_display : measure_display := sigma_display (@open N). + +(*HB.instance Definition _ := Pointed.on borel_type.*) + +HB.instance Definition _ := + Measurable.copy borel_type (g_sigma_algebraType (@open N)). + +End open. +Arguments borel_type {R} N. +Arguments borel_display {R} N. + +Notation "N .-open" := (borel_display N) : measure_display_scope. +Notation "N .-open.-measurable" := (measurable : set_system (@borel_type _ N)) : + classical_set_scope. + +Module MeasurableNormedModuleOpen. +Section measurableOpen. +Context {R : archiRealFieldType} {N : normedModType R}. + +Let measurableTypeNormedModule := g_sigma_algebraType (@open N). + +HB.instance Definition _ : Measurable (borel_display N) measurableTypeNormedModule := + Measurable.on measurableTypeNormedModule. + +(* Presumably it is safe to use NFI here because the sigma-algebra of opens + for N is unique and nothing else can be used here *) +#[non_forgetful_inheritance] +HB.instance Definition _ := Measurable.copy N measurableTypeNormedModule. + +Lemma measurable_set1 (x : N) : measurable [set x]. +Proof. +rewrite set1_bigcap_ball; apply: bigcap_measurable => // k _. +by apply: sub_sigma_algebra; exact: ball_open. +Qed. +#[local] Hint Resolve measurable_set1 : core. + +Lemma measurable_ball_norm (x : N) e : measurable (ball x e). +Proof. exact: (sub_sigma_algebra (ball_open _ _)). Qed. + +End measurableOpen. + +Lemma measurable_funP1 {d} {aT : measurableType d} {rT : archiRealFieldType} + {nT : normedModType rT} (f : {mfun aT >-> nT}) D (z : nT) : + measurable D -> measurable (D `&` f @^-1` [set z]). +Proof. +by move=> /(measurable_funP f); apply => //; exact: measurable_set1. +Qed. + +(* NB: really used, e.g., in simple_functions.v *) +#[global] Hint Extern 0 (measurable (_ @^-1` [set _])) => + solve [apply: measurable_funPTI; exact: measurable_set1] : core. + +(* NB: really used, e.g., in radon_nikodym.v *) +#[global] Hint Extern 0 (measurable (_ `&` _ @^-1` [set _])) => + solve [apply: measurable_funP1; assumption] : core. + +(* NB: really used, e.g., in realfun.v *) +#[global] Hint Extern 0 (measurable [set _]) => + solve [apply: measurable_set1] : core. + +End MeasurableNormedModuleOpen. + +Module MeasurableNormedModule. +Export numFieldNormedType.Exports. +Export MeasurableNormedModuleOpen. +End MeasurableNormedModule. diff --git a/theories/real_measure/real_measure.v b/theories/real_measure/real_measure.v index 44582f4c6a..480fac9700 100644 --- a/theories/real_measure/real_measure.v +++ b/theories/real_measure/real_measure.v @@ -1,4 +1,5 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Export normedtype_measurable. From mathcomp Require Export lebesgue_stieltjes_measure. From mathcomp Require Export lebesgue_measure. From mathcomp Require Export measurable_realfun. diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v index 06f4b1a94e..4abf633194 100644 --- a/theories/topology_theory/metric_structure.v +++ b/theories/topology_theory/metric_structure.v @@ -109,6 +109,20 @@ Qed. End metric_numFieldType. +Section metric_archiRealFieldType. +Context {R : archiRealFieldType} {N : metricType R}. + +Lemma set1_bigcap_ball (x : N) : [set x] = \bigcap_n ball x n.+1%:R^-1. +Proof. +rewrite eqEsubset; split=> [y -> n _ | y /= bn]/=; first exact: ballxx. +apply: close_eq _ => //; first exact: metric_hausdorff. +rewrite ball_close => e0. +apply/ball_sym/(le_ball _ (bn (truncn e0%:num^-1) Logic.I)). +by rewrite invf_ple ?posrE//; exact: (ltW (truncnS_gt _)). +Qed. + +End metric_archiRealFieldType. + Section prod_metric. Context {K : numDomainType} (T U : metricType K).