From ae27d0e6f0fdbcbbda554a7a404d060555fc2b93 Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 19:15:09 +0200
Subject: [PATCH 1/5] Dominated convergence for Rintegral

---
 CHANGELOG_UNRELEASED.md                       |  2 +
 .../lebesgue_Rintegral.v                      | 43 +++++++++++++++++++
 2 files changed, 45 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 9d34c3bd5e..cf31f0acc7 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -271,6 +271,8 @@
   + lemmas `dlet_dlet`, `dmargin_dlet`, `dlet_dmargin`, `dfst_dswap`,
     `dsnd_dswap`, `dsndE`, `pr_dlet` are no longer deprecated
 
+- in file `lebesgue_Rintegral.v`,
+  + new lemma `Rdominated_cvg`.
 
 ### Changed
 
diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
index 1e409c2b69..f9ff47519c 100644
--- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
+++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
@@ -251,3 +251,46 @@ End Rintegral_lebesgue_measure.
 Notation Rintegral_itv_bndo_bndc := Rintegral_itvbo_itvbc (only parsing).
 #[deprecated(since="mathcomp-analysis 1.17.0", use=Rintegral_itvob_itvcb)]
 Notation Rintegral_itv_obnd_cbnd := Rintegral_itvob_itvcb (only parsing).
+
+Section Rdominated_convergence.
+Context d (T : measurableType d) (R : realType).
+Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
+Variables (f_ : (T -> R)^nat) (f g : T -> R).
+Hypothesis mf_ : forall n, measurable_fun D (f_ n).
+Hypothesis f_f : forall x, D x -> f_ ^~ x @ \oo --> f x.
+Hypothesis ig : integrable.body mu D (EFin \o g).
+Hypothesis absfg : forall n x, D x -> `|f_ n x| <= g x.
+
+Let mf_e n : measurable_fun D (EFin \o f_ n).
+Proof. by apply/measurable_EFinP. Qed.
+
+Let f_fe (x : T) : D x -> (f_ n x)%:E @[n --> \oo] --> (f x)%:E.
+Proof.
+move=> Dx.
+apply/fine_cvgP; split; first by apply: nearW.
+by apply: f_f.
+Qed.
+
+Let egi (x : T) : (g x)%:E \is a fin_num.
+Proof. by []. Qed.
+
+Let absfge (n : nat) (x : T) : D x -> (`|(f_ n x)%:E| <= (g x)%:E)%E.
+Proof.
+move=> Dx.
+rewrite abse_EFin lee_fin.
+by apply: absfg.
+Qed.
+
+Let mf : measurable_fun D (EFin \o f).
+Proof. by apply: emeasurable_fun_cvg; first by exact: mf_e. Qed.
+
+Lemma Rdominated_cvg : \int[mu]_(x in D) f_ n x @[n \oo] --> \int[mu]_(x in D) f x.
+Proof.
+rewrite /Rintegral.
+have := dominated_convergence mD mf_e mf (aeW _ f_fe) ig (aeW _ (fun x n Dx => absfge n Dx)).
+move=> /= [i_f _ +].
+rewrite -[X in _ --> X]fineK; first by apply: integrable_fin_num.
+by move/fine_cvg.
+Qed.
+
+End Rdominated_convergence.
\ No newline at end of file

From b8070c56db49be0ea03a104f9a3811a28774cb49 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 30 Jul 2026 11:13:19 +0900
Subject: [PATCH 2/5] shorten

---
 CHANGELOG_UNRELEASED.md                       |  2 +
 .../lebesgue_Rintegral.v                      | 55 ++++++-------------
 2 files changed, 20 insertions(+), 37 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index cf31f0acc7..5d0176b2b7 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -273,6 +273,8 @@
 
 - in file `lebesgue_Rintegral.v`,
   + new lemma `Rdominated_cvg`.
+- in `lebesgue_Rintegral.v`:
+  + lemma `Rdominated_cvg`
 
 ### Changed
 
diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
index f9ff47519c..ef99c971c6 100644
--- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
+++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
@@ -253,44 +253,25 @@ Notation Rintegral_itv_bndo_bndc := Rintegral_itvbo_itvbc (only parsing).
 Notation Rintegral_itv_obnd_cbnd := Rintegral_itvob_itvcb (only parsing).
 
 Section Rdominated_convergence.
-Context d (T : measurableType d) (R : realType).
-Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
-Variables (f_ : (T -> R)^nat) (f g : T -> R).
-Hypothesis mf_ : forall n, measurable_fun D (f_ n).
-Hypothesis f_f : forall x, D x -> f_ ^~ x @ \oo --> f x.
-Hypothesis ig : integrable.body mu D (EFin \o g).
-Hypothesis absfg : forall n x, D x -> `|f_ n x| <= g x.
-
-Let mf_e n : measurable_fun D (EFin \o f_ n).
-Proof. by apply/measurable_EFinP. Qed.
-
-Let f_fe (x : T) : D x -> (f_ n x)%:E @[n --> \oo] --> (f x)%:E.
-Proof.
-move=> Dx.
-apply/fine_cvgP; split; first by apply: nearW.
-by apply: f_f.
-Qed.
-
-Let egi (x : T) : (g x)%:E \is a fin_num.
-Proof. by []. Qed.
-
-Let absfge (n : nat) (x : T) : D x -> (`|(f_ n x)%:E| <= (g x)%:E)%E.
-Proof.
-move=> Dx.
-rewrite abse_EFin lee_fin.
-by apply: absfg.
-Qed.
-
-Let mf : measurable_fun D (EFin \o f).
-Proof. by apply: emeasurable_fun_cvg; first by exact: mf_e. Qed.
-
-Lemma Rdominated_cvg : \int[mu]_(x in D) f_ n x @[n \oo] --> \int[mu]_(x in D) f x.
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D)
+  (f_ : (T -> R)^nat) (f g : T -> R).
+Hypotheses (mf_ : forall n, measurable_fun D (f_ n))
+  (f_f : forall x, D x -> f_ ^~ x @ \oo --> f x)
+  (int_g : mu.-integrable D (EFin \o g))
+  (absfg : forall n x, D x -> `|f_ n x| <= g x).
+
+Lemma Rdominated_cvg :
+  \int[mu]_(x in D) f_ n x @[n \oo] --> \int[mu]_(x in D) f x.
 Proof.
 rewrite /Rintegral.
-have := dominated_convergence mD mf_e mf (aeW _ f_fe) ig (aeW _ (fun x n Dx => absfge n Dx)).
-move=> /= [i_f _ +].
-rewrite -[X in _ --> X]fineK; first by apply: integrable_fin_num.
-by move/fine_cvg.
+have []// := @dominated_convergence _ _ _ mu _ mD (fun n t => (f_ n t)%:E)
+    (EFin \o f) (EFin \o g).
+- by move=> n; exact/measurable_EFinP.
+- exact/measurable_EFinP/measurable_fun_cvg.
+- by apply: aeW => x Dx; apply/fine_cvgP; split; [exact: nearW|exact: f_f].
+- by apply: aeW => x n Dx/=; rewrite lee_fin absfg.
+by move=> int_f _/= int_f_f; apply/fine_cvg; rewrite fineK// integrable_fin_num.
 Qed.
 
-End Rdominated_convergence.
\ No newline at end of file
+End Rdominated_convergence.

From dfadc0a9a1425bdfd568d9084535a6ee58270db9 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 30 Jul 2026 11:23:41 +0900
Subject: [PATCH 3/5] fix changelog

---
 CHANGELOG_UNRELEASED.md | 2 --
 1 file changed, 2 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 5d0176b2b7..a0e9b7e944 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -271,8 +271,6 @@
   + lemmas `dlet_dlet`, `dmargin_dlet`, `dlet_dmargin`, `dfst_dswap`,
     `dsnd_dswap`, `dsndE`, `pr_dlet` are no longer deprecated
 
-- in file `lebesgue_Rintegral.v`,
-  + new lemma `Rdominated_cvg`.
 - in `lebesgue_Rintegral.v`:
   + lemma `Rdominated_cvg`
 

From 900ebd95ccc3d24460f33919637ac5cceee9db53 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 30 Jul 2026 11:49:56 +0900
Subject: [PATCH 4/5] fix

---
 theories/lebesgue_integral_theory/lebesgue_Rintegral.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
index ef99c971c6..d31e31b9bb 100644
--- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
+++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
@@ -261,6 +261,8 @@ Hypotheses (mf_ : forall n, measurable_fun D (f_ n))
   (int_g : mu.-integrable D (EFin \o g))
   (absfg : forall n x, D x -> `|f_ n x| <= g x).
 
+Import MeasurableR.
+
 Lemma Rdominated_cvg :
   \int[mu]_(x in D) f_ n x @[n \oo] --> \int[mu]_(x in D) f x.
 Proof.

From 038310ff7735cd4bfb2f54900ee70698bab7ff1e Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 30 Jul 2026 11:59:52 +0900
Subject: [PATCH 5/5] fix

---
 theories/lebesgue_integral_theory/lebesgue_Rintegral.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
index d31e31b9bb..c6a3bd1c5e 100644
--- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
+++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
@@ -256,13 +256,12 @@ Section Rdominated_convergence.
 Context {d} {T : measurableType d} {R : realType}
   (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D)
   (f_ : (T -> R)^nat) (f g : T -> R).
+Import MeasurableR.
 Hypotheses (mf_ : forall n, measurable_fun D (f_ n))
   (f_f : forall x, D x -> f_ ^~ x @ \oo --> f x)
   (int_g : mu.-integrable D (EFin \o g))
   (absfg : forall n x, D x -> `|f_ n x| <= g x).
 
-Import MeasurableR.
-
 Lemma Rdominated_cvg :
   \int[mu]_(x in D) f_ n x @[n \oo] --> \int[mu]_(x in D) f x.
 Proof.