diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 43da589cbf..3daded7623 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -36,6 +36,27 @@ + lemma `esumE` + lemmas `esummable_esumZ`, `esummable_esumD`, `esummableB` +- in `lebesgue_stieltjes_measure.v`: + + module `MeasurableRocitv` + + definition `open_type` + + notations `.-open`, `.-open.-measurable` + + module `MeasurableOpen` + * definition `measurableTypeO` + + definition `borel_display` + * definition `measurableO` + * definition `measurableTypeR` + + definition `lebesgue_display` + * definition `measurableR` + + lemmas `measurable_set1`, `measurable_itv` (also declared as hints) + + lemma `measurable_ball_norm` + + definition `ocitv_measure`, lemma `ocitv_measure_ext` + + module `MeasurableR` + + module `RGenOpenSets` + * lemma `measurableE` + +- in `real_interval.v`: + + lemma `set1_bigcap_oo` + ### Changed - in `derive.v`: @@ -44,6 +65,18 @@ - moved from `metric_structure.v` to `num_topology.v`: + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`. +- moved from `measurable_realfun.v` to `lebesgue_stieltjes_measure.v` + + module `RGenOInfty` + + module `RGenInftyO` + + module `RGenCInfty` + + module `RGenOpens` + +- moved inside module `MeasurableRocitv` (`lebesgue_stieltjes_measure.v`): + + lemmas `measurable_set1`, `measurable_itv` + +- in `lebesgue_stieltjes_measure.v`: + + lemma `lebesgue_stieltjes_measure_unique` is now about the sigma-algebra generated by open sets + ### Renamed - in `esum.v`: diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index 1652724365..42f93ddd05 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -1,6 +1,6 @@ (* 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 algebra interval. From mathcomp Require Import archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. @@ -465,85 +465,129 @@ Qed. End rgenopensets. End RGenOpenSets. +(* Could be moved elsewhere and generalized to metric spaces *) +Section normed_lemmas. +Context {R : realType} {N : normedModType R}. + +Lemma set1_bigcap_ball (x : N) : [set x] = \bigcap_n ball x n.+1%:R^-1. +Proof. +rewrite eqEsubset/bigcap; split=> [y -> n _ | y /= bn]/=. + by apply: ballxx; rewrite invr_gt0. +apply: close_eq _=>//; rewrite ball_close=> e0; rewrite ball_symE. +apply: (le_ball _ (bn (truncn e0%:num^-1) I)). rewrite invf_ple ?posrE//. +exact: (ltW (truncnS_gt _)). +Qed. + +End normed_lemmas. + +(* Should be moved to a more general file *) Section open. -Context {R : realType}. +Context {R : realType} {N : normedModType R}. -Definition open_type : Type := R. +Definition open_type : Type := N. HB.instance Definition _ := Pointed.on open_type. -Let measurable : set_system R := @measurable _ (g_sigma_algebraType (@open R)). +Let measurable : set_system N := @measurable _ (g_sigma_algebraType (@open N)). 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)) -> +Let measurable_bigcup (F : (set N)^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)) + @isMeasurable.Build (sigma_display (@open N)) open_type measurable measurable0 measurableC measurable_bigcup. End open. -Notation "R .-open" := (sigma_display (@open R)) : measure_display_scope. -Notation "R .-open.-measurable" := (measurable : set_system (@open_type R)) : +Notation "N .-open" := (sigma_display (@open N)) : measure_display_scope. +Notation "N .-open.-measurable" := (measurable : set_system (@open_type _ N)) : classical_set_scope. -Module MeasurableRopen. -Section measurableRopen. -Context {R : realType}. +Module MeasurableOpen. +Section measurableOpen. +Context {R : realType} {N : normedModType R}. -Definition measurableTypeR := g_sigma_algebraType (@open R). +Definition measurableTypeO := g_sigma_algebraType (@open N). -Definition lebesgue_display : measure_display := R.-open. +Definition borel_display : measure_display := N.-open. -Definition measurableR : set_system R := R.-open.-measurable. +Definition measurableO : set_system N := N.-open.-measurable. -HB.instance Definition _ : Measurable lebesgue_display measurableTypeR := - Measurable.on measurableTypeR. +HB.instance Definition _ : Measurable borel_display measurableTypeO := + Measurable.on measurableTypeO. (* 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. +HB.instance Definition _ := Measurable.copy N measurableTypeO. -Lemma measurable_set1 (r : R) : measurable [set r]. +Lemma measurable_set1 (x : N) : measurable [set x]. Proof. -rewrite set1_bigcap_oo; apply: bigcap_measurable => // k _. -exact: sub_sigma_algebra. +rewrite set1_bigcap_ball; apply: bigcap_measurable => // k _. +apply: sub_sigma_algebra; exact: ball_open. Qed. #[local] Hint Resolve measurable_set1 : core. -Lemma measurable_itv (i : interval R) : measurable [set` i]. -Proof. -have := MeasurableRocitv.measurable_itv i. -rewrite /MeasurableRocitv.lebesgue_display. -by rewrite RGenOpenSets.measurableE. -Qed. +Lemma measurable_ball_norm (x : N) e : measurable (ball x e). +Proof. by apply: (sub_sigma_algebra (ball_open _ _)). Qed. -End measurableRopen. -Arguments measurableTypeR : clear implicits. +End measurableOpen. +Arguments measurableTypeO : 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]). + {nT : normedModType rT} (f : {mfun aT >-> nT}) D (z : nT) : + measurable D -> measurable (D `&` f @^-1` [set z]). 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. +Section measurableReal. +Context {R : realType}. +Import numFieldNormedType.Exports. + +Definition measurableTypeR := @measurableTypeO R R. + +Definition lebesgue_display : measure_display := @borel_display R R. + +Definition measurableR := @measurableO R R. + +(* Shouldn't be needing ideally... *) +HB.instance Definition _ := Measurable.copy R measurableTypeR. + +Lemma measurable_itv (i : interval R) : measurable [set` i]. +Proof. +have := MeasurableRocitv.measurable_itv i. +rewrite /MeasurableRocitv.lebesgue_display. +by rewrite RGenOpenSets.measurableE. +Qed. + +End measurableReal. +Arguments measurableTypeR : clear implicits. +#[global] +Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. + +End MeasurableOpen. + +Module MeasurableR. +Export numFieldNormedType.Exports. +Export MeasurableOpen. +End MeasurableR. + Section ocitv_measure. +Import MeasurableR. Context {R : realType} (mu : measure (measurableTypeR R) R). Definition ocitv_measure : set (MeasurableRocitv.measurableTypeR R) -> \bar R := @@ -570,12 +614,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. @@ -958,7 +996,7 @@ apply: measure_extension_unique => //=. Qed. Lemma lebesgue_stieltjes_measure_unique - (mu : {measure set (MeasurableRopen.measurableTypeR R) -> \bar R}) : + (mu : {measure set (measurableTypeR 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/probability_theory/bernoulli_distribution.v b/theories/probability_theory/bernoulli_distribution.v index 245a5777ec..cde09a8648 100644 --- a/theories/probability_theory/bernoulli_distribution.v +++ b/theories/probability_theory/bernoulli_distribution.v @@ -54,7 +54,6 @@ End bernoulli_pmf. Section bernoulli_pmf. Context {R : realType}. - Import MeasurableR. Lemma measurable_bernoulli_pmf D n : diff --git a/theories/probability_theory/normal_distribution.v b/theories/probability_theory/normal_distribution.v index 9b6d4f12aa..9d2ab1a0ea 100644 --- a/theories/probability_theory/normal_distribution.v +++ b/theories/probability_theory/normal_distribution.v @@ -209,7 +209,6 @@ Qed. End normal_density. Section normal_prob_def. - Import MeasurableR. Context {R : realType}. diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index 9d975b517c..15bf706a11 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -103,7 +103,6 @@ Lemma notin_range_measure d d' (T : measurableType d) (T' : measurableType d') Proof. by rewrite notin_setE => hr; rewrite preimage10. Qed. Section probability_range. - Import MeasurableR. Lemma probability_range d d' (T : measurableType d) (T' : measurableType d')