From 58670644af24a4bcfc80491a9e41f900377696e5 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 5 Jul 2024 20:38:18 +0900
Subject: [PATCH] gen section mfun

---
 CHANGELOG_UNRELEASED.md      |  6 ++++++
 theories/lebesgue_integral.v | 20 +++++++++++++-------
 2 files changed, 19 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c52d4873e7..096254f1dd 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -54,6 +54,12 @@
 
 ### Generalized
 
+- in `lebesgue_integral.v`:
+  + generalized from `realType` to `sigmaRingType`
+    * mixin `isMeasurableFun`
+    * structure `MeasurableFun`
+	* definition `mfun`
+
 ### Deprecated
 
 ### Removed
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index a012dab54b..7807da6f3b 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -251,16 +251,17 @@ HB.builders Context T R f of @FiniteDecomp T R f.
 HB.end.
 
 Section mfun_pred.
-Context {d} {aT : sigmaRingType d} {rT : realType}.
+Context {d d'} {aT : sigmaRingType d} {rT : sigmaRingType d'}.
 Definition mfun : {pred aT -> rT} := mem [set f | measurable_fun setT f].
 Definition mfun_key : pred_key mfun. Proof. exact. Qed.
 Canonical mfun_keyed := KeyedPred mfun_key.
 End mfun_pred.
 
-Section mfun.
-Context {d} {aT : measurableType d} {rT : realType}.
+Section mfun_realType.
+Context {d} {aT : sigmaRingType d} {rT : realType}.
 Notation T := {mfun aT >-> rT}.
-Notation mfun := (@mfun _ aT rT).
+Notation mfun := (@mfun _ _ aT rT).
+
 Section Sub.
 Context (f : aT -> rT) (fP : f \in mfun).
 Definition mfun_Sub_subproof := @isMeasurableFun.Build d _ aT rT f (set_mem fP).
@@ -292,6 +293,11 @@ Definition cst_mfun x := [the {mfun aT >-> rT} of cst x].
 
 Lemma mfun_cst x : @cst_mfun x =1 cst x. Proof. by []. Qed.
 
+End mfun_realType.
+
+Section mfun.
+Context {d} {aT : measurableType d} {rT : realType}.
+
 HB.instance Definition _ := @isMeasurableFun.Build _ _ _ rT
   (@normr rT rT) (@measurable_normr rT setT).
 
@@ -310,14 +316,14 @@ End mfun.
 Section ring.
 Context d (aT : measurableType d) (rT : realType).
 
-Lemma mfun_subring_closed : subring_closed (@mfun _ aT rT).
+Lemma mfun_subring_closed : subring_closed (@mfun _ _ aT rT).
 Proof.
 split=> [|f g|f g]; rewrite !inE/=.
 - exact: measurable_cst.
 - exact: measurable_funB.
 - exact: measurable_funM.
 Qed.
-HB.instance Definition _ := GRing.isSubringClosed.Build _ mfun
+HB.instance Definition _ := GRing.isSubringClosed.Build _ (@mfun d default_measure_display aT rT)
   mfun_subring_closed.
 HB.instance Definition _ := [SubChoice_isSubComRing of {mfun aT >-> rT} by <:].
 
@@ -388,7 +394,7 @@ Notation measurable_fun_indic := measurable_indic (only parsing).
 
 Section sfun_pred.
 Context {d} {aT : sigmaRingType d} {rT : realType}.
-Definition sfun : {pred _ -> _} := [predI @mfun _ aT rT & fimfun].
+Definition sfun : {pred _ -> _} := [predI @mfun _ _ aT rT & fimfun].
 Definition sfun_key : pred_key sfun. Proof. exact. Qed.
 Canonical sfun_keyed := KeyedPred sfun_key.
 Lemma sub_sfun_mfun : {subset sfun <= mfun}. Proof. by move=> x /andP[]. Qed.