Generalize quotient of Lspaces to all measurable functions

Author: CohenCyril

CHANGELOG_UNRELEASED.md

@@ -201,6 +201,15 @@
 - in `measure.v`:
   + fourth argument of `probability_setT` is now explicit
 
+- in `hoelder.v`:
+  + generalized the quotient of Lspaces to all measurable functions rather than just Lp functions.
+  + consequently, 
+    * updated notation for measurable functions from `LfunType` to `{mfun_ mu , U >-> V }`
+    * renamed definitions and lemmas from `Lequiv`, `Lequiv_refl`, `Lequiv_sym`, `Lequiv_trans`,
+      `LspaceType` to `ae_eq_op`, `ae_eq_op_refl`, `ae_eq_op_sym`, `ae_eq_op_trans`, `aeEqMfun`
+   * renamed lemma `LequivP` to `ae_eqP`
+
+
 ### Renamed
 
 - in `measure.v`

theories/hoelder.v

@@ -817,45 +817,61 @@ HB.instance Definition _ := gen_choiceMixin (LfunType mu p1).
 
 End LfunType_canonical.
 
-Section Lequiv.
-Context d (T : measurableType d) (R : realType).
-Variables (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E).
+Section AeEqEquiv.
+Context d1 d2 (R : realType) (T1 : measurableType d1) (T2 : measurableType d2).
+Variables (mu : {measure set T1 -> \bar R}).
 
-Definition Lequiv (f g : LfunType mu p1) := `[< f = g %[ae mu] >].
+Definition ae_eq_op (f g : {mfun T1 >-> T2}) := `[< f = g %[ae mu] >].
 
-Let Lequiv_refl : reflexive Lequiv.
+Let ae_eq_op_refl : reflexive ae_eq_op.
 Proof.
 by move=> f; exact/asboolP/(filterS _ (ae_eq_refl mu setT (EFin \o f))).
 Qed.
 
-Let Lequiv_sym : symmetric Lequiv.
+Let ae_eq_op_sym : symmetric ae_eq_op.
 Proof.
 by move=> f g; apply/idP/idP => /asboolP h; apply/asboolP/ae_eq_sym.
 Qed.
 
-Let Lequiv_trans : transitive Lequiv.
+Let ae_eq_op_trans : transitive ae_eq_op.
 Proof.
 by move=> f g h /asboolP gf /asboolP fh; apply/asboolP/(ae_eq_trans gf fh).
 Qed.
 
-Canonical Lequiv_canonical :=
-  EquivRel Lequiv Lequiv_refl Lequiv_sym Lequiv_trans.
+Canonical ae_eq_op_canonical :=
+  EquivRel ae_eq_op ae_eq_op_refl ae_eq_op_sym ae_eq_op_trans.
 
 Local Open Scope quotient_scope.
 
-Definition LspaceType := {eq_quot Lequiv}.
-HB.instance Definition _ := Choice.on LspaceType.
-HB.instance Definition _ := EqQuotient.on LspaceType.
+Definition aeEqMfun : Type := {eq_quot ae_eq_op}.
+HB.instance Definition _ := Choice.on aeEqMfun.
+HB.instance Definition _ := EqQuotient.on aeEqMfun.
+Definition aqEqMfun_to_fun (f : aeEqMfun) : T1 -> T2 := repr f.
+Coercion aqEqMfun_to_fun : aeEqMfun >-> Funclass.
 
-Lemma LequivP (f g : LfunType mu p1) :
-  reflect (f = g %[ae mu]) (f == g %[mod LspaceType]).
+Lemma ae_eqP (f g : aeEqMfun) : reflect (f = g %[ae mu]) (f == g %[mod aeEqMfun]).
 Proof. by apply/(iffP idP); rewrite eqmodE// => /asboolP. Qed.
 
-Record LType := MemLType { Lfun_class : LspaceType }.
-Coercion LfunType_of_LType (f : LType) : LfunType mu p1 :=
-  repr (Lfun_class f).
+End AeEqEquiv.
+
+Reserved Notation "{ 'mfun_' mu , U >-> V }"
+  (at level 0, U at level 69, format "{ 'mfun_'  mu ,  U  >->  V }").
+
+Notation "{ 'mfun_' mu , aT >-> T }" := (@aeEqMfun _ _ _ aT T mu)
+   : form_scope.
 
-End Lequiv.
+Import numFieldNormedType.Exports HBNNSimple.
+
+HB.mixin Record isFinLebesgue d (T : measurableType d) (R : realType)
+    (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E)
+    (f : {mfun_ mu, T >-> measurableTypeR R}) := {
+  Lebesgue_finite : finite_norm mu p f
+}.
+
+#[short(type=LType)]
+HB.structure Definition LebesgueSpace d (T : measurableType d) (R : realType)
+    (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E) :=
+  {f of isFinLebesgue d T R mu p p1 f}.
 
 Section mfun_extra.
 Context d (T : measurableType d) (R : realType).