From ef176a0cc8c2a46090e9048d69e8f17d41d5e381 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 5 Jun 2026 14:53:11 +0900 Subject: [PATCH 1/2] wip --- theories/lebesgue_measure.v | 4 +-- theories/lebesgue_stieltjes_measure.v | 38 +++++++++++++++++---------- 2 files changed, 26 insertions(+), 16 deletions(-) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 327961a2ff..52acd297f5 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -336,9 +336,9 @@ End hlength_extension. End LebesgueMeasure. -Definition lebesgue_measure {R : realType} : - set (measurableTypeR R) -> \bar R := +Definition lebesgue_measure {R : realType} : set R -> \bar R := lebesgue_stieltjes_measure idfun. +Check fun R : realType => lebesgue_stieltjes_measure idfun : Measure.type _ _. HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R). HB.instance Definition _ (R : realType) := SigmaFiniteMeasure.on (@lebesgue_measure R). diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index cd14543440..d8b5f4ff41 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -513,14 +513,34 @@ Definition measurableTypeR (R : realType) := Section lebesgue_stieltjes_measure. Context {R : realType}. -Variable f : cumulative R R. + +Definition lebesgue_display : measure_display := + (R.-ocitv.-measurable).-sigma. +Definition measurableR : set (set R) := + (R.-ocitv.-measurable).-sigma.-measurable. + +HB.instance Definition _ := Pointed.on R. +HB.instance Definition _ := Choice.on (measurableTypeR R). +HB.instance Definition _ := + @isMeasurable.Build lebesgue_display (measurableTypeR R) measurableR + measurable0 (@measurableC _ _) (@bigcupT_measurable _ _). +HB.instance Definition _ := Measurable.copy R (measurableTypeR R). +(*HB.instance (Real.sort R) R_isMeasurable.*) + +Lemma measurableTypeRE : R = g_sigma_algebraType (R.-ocitv.-measurable) + :> measurableType lebesgue_display. +Proof. Admitted. Lemma lebesgue_stieltjes_measure_unique - (mu : {measure set (measurableTypeR R) -> \bar R}) : + (f : cumulative R R) (mu : {measure set R -> \bar R}) : (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) -> - forall A, measurable A -> lebesgue_stieltjes_measure f A = mu A. + forall A : set R, measurable A -> lebesgue_stieltjes_measure f A = mu A. Proof. -move=> muE A mA; apply: measure_extension_unique => //=. +move=> muE A mA. +have @mu' : {measure set (g_sigma_algebraType R.-ocitv.-measurable) -> \bar R}. + rewrite {muE A mA f} -measurableTypeRE. +have := @measure_extension_unique _ _ _ _ _ mu. + apply: measure_extension_unique => //=. exact: wlength_sigma_finite. by move=> X mX; rewrite -muE// -measurable_mu_extE. Qed. @@ -551,16 +571,6 @@ Arguments completed_lebesgue_stieltjes_measure {R}. Section salgebra_R_ssets. Variable R : realType. -Definition measurableR : set (set R) := - (R.-ocitv.-measurable).-sigma.-measurable. - -HB.instance Definition _ := Pointed.on R. -HB.instance Definition R_isMeasurable : - isMeasurable default_measure_display R := - @isMeasurable.Build _ (measurableTypeR R) measurableR - measurable0 (@measurableC _ _) (@bigcupT_measurable _ _). -(*HB.instance (Real.sort R) R_isMeasurable.*) - Lemma measurable_set1 (r : R) : measurable [set r]. Proof. rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _. From 7a7a1c57e8b5e32b5c1c8224d09528936a290d72 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 5 Jun 2026 17:53:21 +0900 Subject: [PATCH 2/2] Keeping definitionally identical display on R --- theories/ftc.v | 6 ++---- .../lebesgue_integral_differentiation.v | 10 ++++----- theories/lebesgue_measure.v | 4 ++-- theories/lebesgue_stieltjes_measure.v | 21 ++++++------------- theories/measurable_realfun.v | 2 +- 5 files changed, 16 insertions(+), 27 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 59fdcaa715..f71ec3f11f 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -281,8 +281,7 @@ Corollary FTC1 f a : {ae mu, forall x, a < BRight x -> derivable F x 1 /\ F^`() x = f x}. Proof. move=> intf locf F; move: (locf) => /lebesgue_differentiation. -apply: filterS; first exact: (ae_filter_ringOfSetsType mu). -move=> i fi ai. +apply: filterS => i fi ai. by apply: (@FTC1_lebesgue_pt _ _ _ (i + 1)%R) => //; rewrite ltrDl. Qed. @@ -292,8 +291,7 @@ Corollary FTC1Ny f : let F x := (\int[mu]_(t in [set` `]-oo, x]]) (f t))%R in {ae mu, forall x, derivable F x 1 /\ F^`() x = f x}. Proof. -move=> intf locf F; have := FTC1 intf locf. -apply: filterS; first exact: (ae_filter_ringOfSetsType mu). +move=> intf locf F; have := FTC1 intf locf; apply: filterS. by move=> r /=; apply; rewrite ltNyr. Qed. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v index 4536324d23..233538111b 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v @@ -1016,14 +1016,14 @@ have incl n : Ee `<=` B k `&` (HLf_g_Be n `|` f_g_Be n) by move=> ?; apply. near \oo => n. rewrite (@le_trans _ _ (mu (B k `&` (HLf_g_Be n `|` f_g_Be n))))//. rewrite le_measure// inE//; apply: measurableI; first exact: measurable_ball. - by apply: measurableU => //; [exact: mEHL|exact: mfge]. + by apply: measurableU => //; exact: mfge. rewrite (@le_trans _ _ ((4 / (e / 2))%:E * n.+1%:R^-1%:E))//. rewrite (@le_trans _ _ (mu (HLf_g_Be n `|` f_g_Be n)))//. rewrite le_measure// inE//. apply: measurableI => //. - by apply: measurableU => //; [exact: mEHL|exact: mfge]. - by apply: measurableU => //; [exact: mEHL|exact: mfge]. - rewrite (le_trans (measureU2 _ _ _))//=; [exact: mEHL|exact: mfge|]. + by apply: measurableU => //; exact: mfge. + by apply: measurableU => //; exact: mfge. + rewrite (le_trans (measureU2 _ _ _))//=. apply: le_trans; first by apply: leeD; [exact: HL_null|exact: fgn_null]. rewrite -muleDl// lee_pmul2r// -EFinD lee_fin -{2}(mul1r (_^-1)%R). by rewrite -mulrDl natr1. @@ -1109,7 +1109,7 @@ Lemma lebesgue_density (A : set R) : measurable A -> @[r --> 0^'+] --> (\1_A x)%:E}. Proof. move=> mA; have := lebesgue_differentiation (locally_integrable_indic openT mA). -apply: filter_app; first exact: (ae_filter_ringOfSetsType mu). +apply: filter_app. apply: aeW => /= x Ax. apply: (sube_cvg0 _ _).1 => //. move: Ax; rewrite /lebesgue_pt /davg /= -/mu => Ax. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 52acd297f5..92c0fe2910 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -989,7 +989,7 @@ have : mu \o Dn @ \oo --> mu (\bigcup_n Dn n). rewrite -setI_bigcupr; rewrite bigcup_itvT setIT. have finDn n : mu (Dn n) \is a fin_num. rewrite ge0_fin_numE// (le_lt_trans _ Dfin)//. - by rewrite le_measure// ?inE//=; [exact: mDn|exact: subIsetl]. + by rewrite le_measure// ?inE//=; exact: subIsetl. have finD : mu D \is a fin_num by rewrite fin_num_abs gee0_abs. rewrite -[mu D]fineK// => /fine_cvg/(_ (interior (ball (fine (mu D)) eps)))[]. exact/nbhs_interior/nbhsx_ballx. @@ -1001,7 +1001,7 @@ have finDDn : mu D - mu (Dn n) \is a fin_num by rewrite ?fin_numB ?finD /= ?(finDn n). rewrite -fine_abse // gee0_abs ?sube_ge0 ?finD ?(finDn _) //; last first. by rewrite -[_ - _]fineK // lte_fin fine. -by rewrite le_measure// ?inE//; [exact: measurableI |exact: subIsetl]. +by rewrite le_measure// ?inE//; exact: subIsetl. Qed. Lemma lebesgue_regularity_inner (D : set R) (eps : R) : diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index d8b5f4ff41..be715f4337 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -519,28 +519,19 @@ Definition lebesgue_display : measure_display := Definition measurableR : set (set R) := (R.-ocitv.-measurable).-sigma.-measurable. -HB.instance Definition _ := Pointed.on R. -HB.instance Definition _ := Choice.on (measurableTypeR R). -HB.instance Definition _ := - @isMeasurable.Build lebesgue_display (measurableTypeR R) measurableR - measurable0 (@measurableC _ _) (@bigcupT_measurable _ _). +HB.instance Definition _ : Measurable lebesgue_display (measurableTypeR R) := + Measurable.on (measurableTypeR R). +(* 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 R). -(*HB.instance (Real.sort R) R_isMeasurable.*) - -Lemma measurableTypeRE : R = g_sigma_algebraType (R.-ocitv.-measurable) - :> measurableType lebesgue_display. -Proof. Admitted. Lemma lebesgue_stieltjes_measure_unique (f : cumulative R 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. -move=> muE A mA. -have @mu' : {measure set (g_sigma_algebraType R.-ocitv.-measurable) -> \bar R}. - rewrite {muE A mA f} -measurableTypeRE. -have := @measure_extension_unique _ _ _ _ _ mu. - apply: measure_extension_unique => //=. +move=> muE A mA; apply: measure_extension_unique => //=. exact: wlength_sigma_finite. by move=> X mX; rewrite -muE// -measurable_mu_extE. Qed. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 75565ec051..28095e43ed 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -1088,7 +1088,7 @@ split=> [|f g|f g]; rewrite !inE/=. - exact: measurable_funM. Qed. HB.instance Definition _ := GRing.isSubringClosed.Build _ - (@mfun d default_measure_display aT rT) mfun_subring_closed. + (@mfun d lebesgue_display aT rT) mfun_subring_closed. HB.instance Definition _ := [SubChoice_isSubComPzRing of {mfun aT >-> rT} by <:].