diff --git a/theories/real_measure/lebesgue_stieltjes_measure.v b/theories/real_measure/lebesgue_stieltjes_measure.v index 0ddbb8bffd..77bc93a252 100644 --- a/theories/real_measure/lebesgue_stieltjes_measure.v +++ b/theories/real_measure/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 ssralg ssrnum ssrint algebra interval. From mathcomp Require Import interval_inference archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. @@ -463,85 +463,114 @@ Qed. End rgenopensets. End RGenOpenSets. +(* 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 MeasurableNormedModuleOpen. +Section measurableOpen. +Context {R : realType} {N : normedModType R}. +Import numFieldNormedType.Exports. -Definition measurableTypeR := g_sigma_algebraType (@open R). +Definition measurableTypeNormedModule := 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 measurableNormedModule : set_system N := N.-open.-measurable. -HB.instance Definition _ : Measurable lebesgue_display measurableTypeR := - Measurable.on measurableTypeR. +HB.instance Definition _ : Measurable borel_display measurableTypeNormedModule := + Measurable.on measurableTypeNormedModule. (* 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 measurableTypeNormedModule. -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 measurableTypeNormedModule : 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 := @measurableTypeNormedModule R R. + +Definition lebesgue_display : measure_display := @borel_display R R. + +Definition measurableR := @measurableNormedModule 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 MeasurableNormedModuleOpen. + +Module MeasurableR. +Export numFieldNormedType.Exports. +Export MeasurableNormedModuleOpen. +End MeasurableR. + Section ocitv_measure. +Import MeasurableR. Context {R : realType} (mu : measure (measurableTypeR R) R). Definition ocitv_measure : set (MeasurableRocitv.measurableTypeR R) -> \bar R := @@ -568,12 +597,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. @@ -950,13 +973,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 (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/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v index 06f4b1a94e..7eba93cbab 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 by apply: ballxx; + rewrite invr_gt0. +apply: close_eq _=>//; first exact: metric_hausdorff; rewrite ball_close=> e0; +rewrite ball_symE. apply: (le_ball _ (bn (truncn e0%:num^-1) I)). +by rewrite invf_ple ?posrE//; exact: (ltW (truncnS_gt _)). +Qed. + +End metric_archiRealFieldType. + Section prod_metric. Context {K : numDomainType} (T U : metricType K).