Files

Module mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrnum ssrint interval.
From mathcomp Require Import interval_inference archimedean finmap.
From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.
From mathcomp Require Import reals real_interval topology ereal.
From mathcomp Require Import normedtype sequences esum measure.
From mathcomp Require Import real_measure numfun realfun.
From mathcomp Require Import simple_functions measurable_fun_approximation.
From mathcomp Require Import lebesgue_integral_definition.
From mathcomp Require Import lebesgue_integral_monotone_convergence.
From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable.
From mathcomp Require Import lebesgue_integral_dominated_convergence.

# The Lebesgue Integral for real-valued functions This file recasts lemmas about `integral` to `Rintegral`. It also establishes that continuous functions are dense in $L^1$. `Rintegral mu D f` : Definition for `fine (\int[mu]_(x in D) f x)` `measure_of_density mf f0` : measure induced by `f : T -> R` : `f` is called the density of the induced measure : `mf` is a proof that `f` is measurable and `f0`, a proof that it is : non-negative

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Theory.
Import numFieldNormedType.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Section Rintegral.
Local Open Scope ereal_scope.
Context dSource code (TSource code : measurableType d) (RSource code : realType)
        (muSource code : {measure set T -> \bar R}).

Definition Rintegral

Rintegral : forall [d : measure_display] [T : measurableType d] [R : realType], {measure set T -> \bar R}%R -> set T -> (T -> R) -> R Rintegral is not universe polymorphic Arguments Rintegral [d]%_measure_display_scope [T R] mu D%_classical_set_scope f%_function_scope Rintegral is transparent Expands to: Constant mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral.Rintegral Declared in library mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral, line 46, characters 11-20

Used by
  • mathcomp.analysis.probability_theory.beta_distribution
  • mathcomp.analysis.ftc
  • mathcomp.analysis.pi_irrational
  • mathcomp.analysis.gauss_integral
  • mathcomp.analysis.elementary_functions.trigonometry_integral
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under
  • mathcomp.analysis.lebesgue_integral_theory.radon_nikodym
Source code (DSource code : set T) (fSource code : T -> R) :=
  fine (\int[mu]_(xSource code in D) (f x)%:E).

End Rintegral.

Notation "\int [ mu ]_ ( x 'in' D ) f"Source code :=
  (Rintegral mu D (fun xSource code => f)%R) : ring_scope.
Notation "\int [ mu ]_ x f"Source code :=
  (Rintegral mu setT (fun xSource code => f)%R) : ring_scope.

Section Rintegral.
Context dSource code {TSource code : measurableType d} {RSource code : realType}
  (muSource code : {measure set T -> \bar R}).
Implicit Types (D A B : set T) (f : T -> R).

Lemma EFin_normr_RintegralSource code ASource code fSource code : measurable A ->
  mu.-integrable A (EFin \o f) ->
  `| \int[mu]_(xSource code in A) f x |%:E = `| \int[mu]_(xSource code in A) (f x)%:E |%E.
Proof.
move=> mA /integrableP[mf intfoo]; rewrite -[RHS]fineK.
- rewrite abse_fin_num fin_num_abs.
  exact: (le_lt_trans (le_abse_integral _ _ _)).
- rewrite /= fine_abse// fin_num_abs.
  exact: (le_lt_trans (le_abse_integral _ _ _)).
Qed.

Lemma eq_RintegralUsed by
  • mathcomp.analysis.probability_theory.beta_distribution
  • mathcomp.analysis.ftc
  • mathcomp.analysis.gauss_integral
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under
Source code DSource code gSource code fSource code : {in D, f =1 g} ->
  \int[mu]_(xSource code in D) f x = \int[mu]_(xSource code in D) g x.
Proof.
by move=> fg; congr fine; apply: eq_integral => /= x xD; rewrite fg. Qed.

Lemma Rintegral_mkcondUsed by
  • mathcomp.analysis.probability_theory.beta_distribution
Source code DSource code fSource code : \int[mu]_(xSource code in D) f x = \int[mu]_xSource code (f \_ D) x.
Proof.
rewrite {1}/Rintegral integral_mkcond/=.
by under eq_integral do rewrite restrict_EFin.
Qed.

Lemma Rintegral_mkcondrUsed by
  • mathcomp.analysis.ftc
Source code DSource code PSource code fSource code :
  \int[mu]_(xSource code in D `&` P) f x = \int[mu]_(xSource code in D) (f \_ P) x.
Proof.
rewrite {1}/Rintegral integral_mkcondr.
by under eq_integral do rewrite restrict_EFin.
Qed.

Lemma Rintegral_mkcondlSource code DSource code PSource code fSource code :
  \int[mu]_(xSource code in P `&` D) f x = \int[mu]_(xSource code in D) (f \_ P) x.
Proof.
by rewrite setIC Rintegral_mkcondr. Qed.

Lemma RintegralZlUsed by
  • mathcomp.analysis.probability_theory.beta_distribution
  • mathcomp.analysis.gauss_integral
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under
Source code DSource code fSource code rSource code : measurable D -> mu.-integrable D (EFin \o f) ->
  \int[mu]_(xSource code in D) (r * f x) = r * \int[mu]_(xSource code in D) f x.
Proof.
move=> mD intf; rewrite (_ : r = fine r%:E)// -fineM//.
  exact: integrable_fin_num.
by congr fine; under eq_integral do rewrite EFinM; exact: integralZl.
Qed.

Lemma RintegralZrSource code DSource code fSource code rSource code : measurable D -> mu.-integrable D (EFin \o f) ->
  \int[mu]_(xSource code in D) f x * r = (\int[mu]_(xSource code in D) f x) * r.
Proof.
move=> mD intf; rewrite mulrC -RintegralZl//.
by under eq_Rintegral do rewrite mulrC.
Qed.

Lemma Rintegral_ge0Used by
  • mathcomp.analysis.gauss_integral
Source code DSource code fSource code : (forall xSource code, D x -> 0 <= f x) ->
  0 <= \int[mu]_(xSource code in D) f x.
Proof.
by move=> f0; rewrite fine_ge0// integral_ge0. Qed.

Import MeasurableR.

Lemma le_normr_RintegralUsed by
  • mathcomp.analysis.ftc
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under
Source code DSource code fSource code : measurable D -> mu.-integrable D (EFin \o f) ->
  `|\int[mu]_(tSource code in D) f t| <= \int[mu]_(tSource code in D) `|f t|.
Proof.
move=> mA /integrableP[mf ifoo].
rewrite -lee_fin; apply: le_trans.
  apply: (le_trans _ (le_abse_integral mu mA mf)).
  rewrite /abse.
  have [/fineK <-//|] := boolP (\int[mu]_(xSource code in D) (EFin \o f) x \is a fin_num)%E.
  by rewrite fin_numEn => /orP[|] /eqP ->; rewrite leey.
rewrite /Rintegral.
move: ifoo.
rewrite -ge0_fin_numE; first exact: integral_ge0.
move/fineK ->.
by apply: ge0_le_integral => //=; do 2 apply: measurableT_comp => //;
  exact/measurable_EFinP.
Qed.

Lemma Rintegral_setUUsed by
  • mathcomp.analysis.ftc
Source code (ASource code BSource code : set T) (fSource code : T -> R) :
    d.-measurable A -> d.-measurable B ->
    mu.-integrable (A `|` B) (EFin \o f) -> [disjoint A & B] ->
  \int[mu]_(xSource code in (A `|` B)) f x = \int[mu]_(xSource code in A) f x + \int[mu]_(xSource code in B) f x.
Proof.
move=> mA mB mf AB; rewrite /Rintegral integral_setU//.
  exact/(measurable_int mu).
have mAf :  mu.-integrable A (EFin \o f).
  by  apply: integrableS mf => //; exact: measurableU.
have mBf :  mu.-integrable B (EFin \o f).
  by apply: integrableS mf => //; exact: measurableU.
move/integrableP : mAf => [mAf itAfoo].
move/integrableP : mBf => [mBf itBfoo].
rewrite fineD//.
- by rewrite fin_num_abs (le_lt_trans _ itAfoo)//; exact: le_abse_integral.
- by rewrite fin_num_abs (le_lt_trans _ itBfoo)//; exact: le_abse_integral.
Qed.

Lemma Rintegral_set0Used by
  • mathcomp.analysis.ftc
Source code fSource code : \int[mu]_(xSource code in set0) f x = 0.
Proof.
by rewrite /Rintegral integral_set0. Qed.

Lemma Rintegral_cstUsed by
  • mathcomp.analysis.probability_theory.beta_distribution
  • mathcomp.analysis.pi_irrational
  • mathcomp.analysis.gauss_integral
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
Source code DSource code : d.-measurable D ->
  forall rSource code, \int[mu]_(_ in D) r = r * fine (mu D).
Proof.
move=> mD r; rewrite /Rintegral/= integral_cst//.
have := leey (mu D); rewrite le_eqVlt => /predU1P[->/=|muy]; last first.
  by rewrite fineM// ge0_fin_numE.
rewrite mulr0 mulr_infty/=; have [_|r0|r0] := sgrP r.
- by rewrite mul0e.
- by rewrite mul1e.
- by rewrite mulN1e.
Qed.

Lemma le_RintegralUsed by
  • mathcomp.analysis.pi_irrational
Source code DSource code f1Source code f2Source code : measurable D ->
  mu.-integrable D (EFin \o f1) ->
  mu.-integrable D (EFin \o f2) ->
  (forall xSource code, D x -> f1 x <= f2 x) ->
  \int[mu]_(xSource code in D) f1 x <= \int[mu]_(xSource code in D) f2 x.
Proof.
move=> mD mf1 mf2 f12; rewrite /Rintegral fine_le//.
- rewrite -integral_fin_num_abs//; last by case/integrableP : mf1.
  by apply/measurable_EFinP; case/integrableP : mf1.
- rewrite -integral_fin_num_abs//; last by case/integrableP : mf2.
  by apply/measurable_EFinP; case/integrableP : mf2.
- by apply/le_integral => // x xD; rewrite lee_fin f12//; exact/set_mem.
Qed.

Lemma RintegralDSource code DSource code f1Source code f2Source code : measurable D ->
  mu.-integrable D (EFin \o f1) -> mu.-integrable D (EFin \o f2) ->
  \int[mu]_(xSource code in D) (f1 x + f2 x) =
  \int[mu]_(xSource code in D) f1 x + \int[mu]_(xSource code in D) f2 x.
Proof.
move=> mD if1 if2.
by rewrite /Rintegral integralD_EFin// fineD//; exact: integrable_fin_num.
Qed.

Lemma RintegralBUsed by
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under
Source code DSource code f1Source code f2Source code : measurable D ->
  mu.-integrable D (EFin \o f1) -> mu.-integrable D (EFin \o f2) ->
  \int[mu]_(xSource code in D) (f1 x - f2 x) =
  \int[mu]_(xSource code in D) f1 x - \int[mu]_(xSource code in D) f2 x.
Proof.
move=> mD if1 if2.
by rewrite /Rintegral integralB_EFin// fineB//; exact: integrable_fin_num.
Qed.

End Rintegral.

Section semi_sigma_additive_measure_of_density.
Context dSource code (TSource code : measurableType d) {RSource code : realType} (muSource code : {measure set T -> \bar R}).
Local Open Scope ereal_scope.

Lemma semi_sigma_additive_measure_of_densityUsed by
  • mathcomp.analysis.lebesgue_integral_theory.radon_nikodym
Source code (fSource code : T -> \bar R) :
  measurable_fun setT f -> (forall xSource code, 0 <= f x) ->
  semi_sigma_additive (fun ASource code => \int[mu]_(tSource code in A) f t).
Proof.
move=> mf f0 /= F mF tF mUF; rewrite ge0_integral_bigcup//=.
  exact: measurable_funTS.
by apply: is_cvg_ereal_nneg_natsum_cond => // n _ _; exact: integral_ge0.
Qed.

End semi_sigma_additive_measure_of_density.
#[deprecated(since="mathcomp-analysis 1.19.0", use=semi_sigma_additive_measure_of_density)]
Notation semi_sigma_additive_nng_inducedSource code := semi_sigma_additive_measure_of_density (only parsing).

Section measure_of_density_def.
Import MeasurableR.
Context {dSource code} {TSource code : measurableType d} {RSource code : realType}
  (muSource code : {measure set T -> \bar R}).

Definition measure_of_density

measure_of_density : forall {d : measure_display} {T : measurableType d} {R : realType}, {measure set T -> \bar R}%R -> forall [f : T -> R], measurable_fun (T:=T) (U:=Real_sort__canonical__measurable_structure_SigmaRing) [set: T] f -> (forall x : T, (0 <= f x)%R) -> set T -> GRing.BaseAddMagma.sort \bar R measure_of_density is not universe polymorphic Arguments measure_of_density {d}%_measure_display_scope {T R} mu [f]%_function_scope mf f0%_function_scope A%_classical_set_scope measure_of_density is transparent Expands to: Constant mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral.measure_of_density Declared in library mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral, line 220, characters 11-29

Used by
  • mathcomp.analysis.probability_theory.normal_distribution
Source code (fSource code : T -> R) (mfSource code : measurable_fun [set: T] f)
    (f0Source code : forall xSource code, 0 <= f x) :=
  fun ASource code => (\int[mu]_(tSource code in A) (f t)%:E)%E.

End measure_of_density_def.

Section measure_of_density.
Import MeasurableR.
Context {dSource code} {TSource code : measurableType d} {RSource code : realType}
  (muSource code : {measure set T -> \bar R}) (fSource code : T -> R).

Hypotheses (mfSource code : measurable_fun [set: T] f) (f0Source code : forall xSource code, (0 <= f x)%R).

Local Notation m'Source code := (measure_of_density mu mf f0).

Let m'0Source code : m' set0 = 0
Proof.
exact: integral_set0. Qed.

Let m'_ge0Source code ASource code : (0 <= m' A)%E.
Proof.
by apply: integral_ge0 => t At; rewrite lee_fin. Qed.

Let m'_semi_sigma_additiveSource code : semi_sigma_additive m'.
Proof.
by apply: semi_sigma_additive_measure_of_density => //; exact/measurable_EFinP.
Qed.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code isMeasureSource code.Build d T R m'
  m'0 m'_ge0 m'_semi_sigma_additive.

End measure_of_density.

Section integral_measure_of_density.
Import MeasurableR.
Local Open Scope ereal_scope.
Context {dSource code} {TSource code : measurableType d} {RSource code : realType}
  (muSource code : {measure set T -> \bar R}) (hSource code : T -> R).

Hypothesis mhSource code : measurable_fun [set: T] h.
Hypothesis h0Source code : forall xSource code, (0 <= h x)%R.

Let mu'Source code : {measure set _ -> \bar _} := measure_of_density mu mh h0.

#[local] Lemma integral_measure_of_density_indicSource code (ASource code : set T) : measurable A ->
  \int[mu]_xSource code ((\1_A x)%:E * (h x)%:E) = mu' A.
Proof.
move=> mA; rewrite [RHS]integral_mkcond; apply: eq_integral => x _.
rewrite patchE indicE; case: ifP => _; first by rewrite mul1e.
by rewrite mul0e.
Qed.

#[local] Lemma integral_measure_of_densityMindicSource code (rSource code : R) (ASource code : set T) : measurable A ->
  \int[mu]_xSource code (r%:E * (\1_A x)%:E * (h x)%:E) = r%:E * mu' A.
Proof.
move=> mA.
under eq_integral do rewrite -muleA.
rewrite ge0_integralZl//=.
- by move=> x _; apply: mule_ge0; rewrite ?lee_fin.
- apply: emeasurable_funM => //; by apply /measurable_EFinP.
- by rewrite integral_measure_of_density_indic.
Qed.

Import HBNNSimple.

#[local] Lemma sintegral_measure_of_densitySource code (gSource code : {nnsfun T >-> R}) :
  sintegral mu' g = \int[mu]_xSource code ((g x)%:E * (h x)%:E).
Proof.
transitivity (\sum_(rSource code \in range g)
    \int[mu]_xSource code (r%:E * (\1_(g @^-1` [set r]) x)%:E * (h x)%:E)).
  rewrite sintegralE; apply: eq_fsbigr => r /set_mem[x0 _ <-].
  by rewrite integral_measure_of_densityMindic.
transitivity (\int[mu]_xSource code (\sum_(rSource code \in range g)
    ((r * (\1_(g @^-1` [set r]) x))%:E * (h x)%:E))).
  rewrite ge0_integral_fsum//=.
  - move=> r.
    under eq_fun do rewrite EFinM -muleA.
    apply: measurable_funeM.
    by apply: emeasurable_funM => //; exact/measurable_EFinP.
  - move=> r x _; have [r0|r0] := leP 0%R r.
      by rewrite mule_ge0// lee_fin// mulr_ge0.
    by rewrite preimage_nnfun0// indic0/= mulr0 mul0e.
apply: eq_integral => x _.
rewrite -ge0_mule_fsuml; first by move=> _ [t _ <-]; rewrite lee_fin mulr_ge0.
by rewrite fsumEFin// [in RHS](fimfunE g).
Qed.

Lemma integral_measure_of_densitySource code (fSource code : T -> \bar R) :
    measurable_fun [set: T] f -> (forall xSource code, 0 <= f x) ->
  \int[mu']_xSource code f x = \int[mu]_xSource code (f x * (h x)%:E).
Proof.
move=> mf f0.
pose g := nnsfun_approx measurableT mf.
pose gE := fun nSource code => EFin \o g n.
have mgE n : measurable_fun [set: T] (EFin \o g n) by exact/measurable_EFinP.
have gE_ge0 n x : 0 <= gE n x by rewrite lee_fin.
have nd_gE x : {homo gE ^~ x : nSource code pSource code / (n <= p)%O >-> n <= p}.
  by move=> *; exact/lefP/nd_nnsfun_approx.
transitivity (limn (fun nSource code => \int[mu']_xSource code gE n x)).
  rewrite -monotone_convergence//; apply: eq_integral => t _.
  by apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx.
transitivity (limn (fun nSource code => \int[mu]_xSource code (gE n x * (h x)%:E))).
  apply: congr_lim; apply/funext => n.
  by rewrite integralT_nnsfun sintegral_measure_of_density.
have mgEh n : measurable_fun [set: T] (fun xSource code => gE n x * (h x)%:E).
  by apply: emeasurable_funM => //; exact/measurable_EFinP.
have gEh_ge0 n x : 0 <= gE n x * (h x)%:E by rewrite mule_ge0// lee_fin.
have nd_gEh x :
    {homo (fun nSource code => gE n x * (h x)%:E) : nSource code pSource code / (n <= p)%O >-> n <= p}.
  by move=> p q pq; rewrite lee_wpmul2r ?lee_fin//; exact: nd_gE.
rewrite -monotone_convergence//.
apply: eq_integral => x _.
apply: cvg_lim => //; apply: cvgeZr => //.
exact: cvg_nnsfun_approx.
Qed.

End integral_measure_of_density.

Section Rintegral_lebesgue_measure.
Context {RSource code : realType}.
Notation muSource code := (@lebesgue_measure R).
Implicit Type f : R -> R.

Import MeasurableR.

Lemma Rintegral_itvbo_itvbcSource code (aSource code : itv_bound R) (rSource code : R) fSource code :
  mu.-integrable [set` Interval a (BLeft r)] (EFin \o f) ->
   \int[mu]_(xSource code in [set` Interval a (BLeft r)]) (f x) =
   \int[mu]_(xSource code in [set` Interval a (BRight r)]) (f x).
Proof.
move=> mf; rewrite /Rintegral integral_itvbo_itvbc//.
exact: (measurable_int mu).
Qed.

Lemma Rintegral_itvob_itvcbUsed by
  • mathcomp.analysis.ftc
Source code (rSource code : R) (bSource code : itv_bound R) fSource code :
  mu.-integrable [set` Interval (BRight r) b] (EFin \o f) ->
  \int[mu]_(xSource code in [set` Interval (BRight r) b]) (f x) =
  \int[mu]_(xSource code in [set` Interval (BLeft r) b]) (f x).
Proof.
move=> mf; rewrite /Rintegral integral_itvob_itvcb//.
exact: (measurable_int mu).
Qed.

Lemma Rintegral_set1Used by
  • mathcomp.analysis.ftc
  • mathcomp.analysis.gauss_integral
  • mathcomp.analysis.elementary_functions.trigonometry_integral
Source code fSource code (rSource code : R) : \int[mu]_(xSource code in [set r]) f x = 0.
Proof.
by rewrite /Rintegral integral_set1. Qed.

Lemma Rintegral_itvBUsed by
  • mathcomp.analysis.ftc
Source code fSource code (aSource code bSource code : itv_bound R) xSource code :
  mu.-integrable [set` (Interval a b)] (EFin \o f) ->
  (a <= BRight x)%O -> (BRight x <= b)%O ->
  \int[mu]_(tSource code in [set` Interval a b]) f t -
  \int[mu]_(tSource code in [set` Interval a (BRight x)]) f t =
  \int[mu]_(xSource code in [set` Interval (BRight x) b]) f x.
Proof.
move=> itf; rewrite le_eqVlt => /predU1P[ax|ax xb].
  rewrite ax => _; rewrite [in X in _ - X]set_itv_ge ?bnd_simp//.
  by rewrite Rintegral_set0 subr0.
rewrite (@itv_bndbnd_setU _ _ _ (BLeft x)).
  by case: a ax {itf} => -[].
  by rewrite (le_trans _ xb)// bnd_simp.
rewrite Rintegral_setU//=.
- by rewrite -itv_bndbnd_setU -?ltBRight_leBLeft// ltW.
- apply/disj_setPS => y [/=]; rewrite 2!in_itv/= => /andP[_ yx] /andP[].
  by rewrite leNgt yx.
rewrite Rintegral_itvbo_itvbc//.
  apply: integrableS itf => //; apply: subset_itvl.
  by rewrite (le_trans _ xb)// bnd_simp.
rewrite addrC addKr Rintegral_itvob_itvcb//.
by apply: integrableS itf => //; exact/subset_itvr/ltW.
Qed.

End Rintegral_lebesgue_measure.
#[deprecated(since="mathcomp-analysis 1.17.0", use=Rintegral_itvbo_itvbc)]
Notation Rintegral_itv_bndo_bndcSource code := Rintegral_itvbo_itvbc (only parsing).
#[deprecated(since="mathcomp-analysis 1.17.0", use=Rintegral_itvob_itvcb)]
Notation Rintegral_itv_obnd_cbndSource code := Rintegral_itvob_itvcb (only parsing).

Section Rdominated_convergence.
Context {dSource code} {TSource code : measurableType d} {RSource code : realType}
  (muSource code : {measure set T -> \bar R}) (DSource code : set T) (mDSource code : measurable D)
  (f_Source code : (T -> R)^nat) (fSource code gSource code : T -> R).
Import MeasurableR.
Hypotheses (mf_Source code : forall nSource code, measurable_fun D (f_ n))
  (f_fSource code : forall xSource code, D x -> f_ ^~ x @ \oo --> f x)
  (int_gSource code : mu.-integrable D (EFin \o g))
  (absfgSource code : forall nSource code xSource code, D x -> `|f_ n x| <= g x).

Lemma Rdominated_cvgSource code :
  \int[mu]_(xSource code in D) f_ n x @[nSource code \oo] --> \int[mu]_(xSource code in D) f x.
Proof.
rewrite /Rintegral.
have []// := @dominated_convergence _ _ _ mu _ mD (fun nSource code tSource code => (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.
Generated by rocqnavi
Source
Uses
Used By