Trying to fix the R sigma-algebra issue (#1986)

* Keeping definitionally identical display on R

---------

Co-authored-by: Cyril Cohen <cyril.cohen@inria.fr>

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -128,6 +128,9 @@
     * lemmas `zornS_ex`, `domain_extend`, `hahn_banach_witness`
   + theorems `hahn_banach_extension`, `hahn_banach_extension_normed`
 
+- in `lebesgue_stieltjes_measure.v`:
+  + definition `lebesgue_display`
+
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:

theories/ftc.v

@@ -263,8 +263,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.
 
@@ -274,8 +273,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.
 

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.

theories/lebesgue_measure.v

@@ -336,8 +336,7 @@ 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.
 HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R).
 HB.instance Definition _ (R : realType) :=
@@ -989,7 +988,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 +1000,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) :

theories/lebesgue_stieltjes_measure.v

@@ -33,6 +33,10 @@ From mathcomp Require Import realfun.
 (*         R.-ocitv.-measurable == semiring of sets of open-closed intervals  *)
 (*                  wlength f A := f b - f a with the hull of the set of real *)
 (*                                 numbers A being delimited by a and b       *)
+(*           @measurableTypeR R == measurableType generated by R.-ocitv       *)
+(*          @lebesgue_display R == (measure_)display for the sigma-algebra    *)
+(*                                 generated by R.-ocitv                      *)
+(*               @measurableR R == measurable sets generated by R.-ocitv      *)
 (* lebesgue_stieltjes_measure f == Lebesgue-Stieltjes measure for f           *)
 (*                                 f is a cumulative function.                *)
 (* completed_lebesgue_stieltjes_measure f == the completed Lebesgue-Stieltjes *)
@@ -513,12 +517,23 @@ 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 _ : 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).
 
 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 => //=.
   exact: wlength_sigma_finite.
@@ -551,16 +566,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 _.

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 <:].