Dominated convergence for Rintegral

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 `lebesgue_Rintegral.v`:
+  + lemma `Rdominated_cvg`
 
 ### Changed
 

theories/lebesgue_integral_theory/lebesgue_Rintegral.v

@@ -251,3 +251,28 @@ 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}
+  (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).
+
+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 _ _ _ 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.