Module mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral

# 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 ( : measurableType d) ( : realType)
        ( : {measure set T -> \bar R}).

Definition ( : set T) ( : T -> R) :=
  fine (\int[mu]_( in D) (f x)%:E).

End Rintegral.

Notation :=
  (Rintegral mu D (fun => f)%R) : ring_scope.
Notation :=
  (Rintegral mu setT (fun => f)%R) : ring_scope.

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

Lemma : measurable A ->
  mu.-integrable A (EFin \o f) ->
  `| \int[mu]_( in A) f x |%:E = `| \int[mu]_( 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 : {in D, f =1 g} ->
\int[mu]_( in D) f x = \int[mu]_( in D) g x.

Proof.

by move=> fg; congr fine; apply: eq_integral => /= x xD; rewrite fg. Qed.

Lemma : \int[mu]_( in D) f x = \int[mu]_ (f \_ D) x.

Proof.

rewrite {1}/Rintegral integral_mkcond/=.
by under eq_integral do rewrite restrict_EFin.
Qed.

Lemma :
\int[mu]_( in D `&` P) f x = \int[mu]_( in D) (f \_ P) x.

Proof.

rewrite {1}/Rintegral integral_mkcondr.
by under eq_integral do rewrite restrict_EFin.
Qed.

Lemma :
\int[mu]_( in P `&` D) f x = \int[mu]_( in D) (f \_ P) x.

Proof.

by rewrite setIC Rintegral_mkcondr. Qed.

Lemma : measurable D -> mu.-integrable D (EFin \o f) ->
\int[mu]_( in D) (r * f x) = r * \int[mu]_( 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 : measurable D -> mu.-integrable D (EFin \o f) ->
\int[mu]_( in D) f x * r = (\int[mu]_( in D) f x) * r.

Proof.

move=> mD intf; rewrite mulrC -RintegralZl//.
by under eq_Rintegral do rewrite mulrC.
Qed.

Lemma : (forall , D x -> 0 <= f x) ->
0 <= \int[mu]_( in D) f x.

Proof.

by move=> f0; rewrite fine_ge0// integral_ge0. Qed.

Import MeasurableR.

Lemma : measurable D -> mu.-integrable D (EFin \o f) ->
`|\int[mu]_( in D) f t| <= \int[mu]_( 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]_( 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 ( : set T) ( : T -> R) :
    d.-measurable A -> d.-measurable B ->
    mu.-integrable (A `|` B) (EFin \o f) -> [disjoint A & B] ->
  \int[mu]_( in (A `|` B)) f x = \int[mu]_( in A) f x + \int[mu]_( 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 : \int[mu]_( in set0) f x = 0.

Proof.

by rewrite /Rintegral integral_set0. Qed.

Lemma : d.-measurable D ->
forall , \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 : measurable D ->
  mu.-integrable D (EFin \o f1) ->
  mu.-integrable D (EFin \o f2) ->
  (forall , D x -> f1 x <= f2 x) ->
  \int[mu]_( in D) f1 x <= \int[mu]_( 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 : measurable D ->
  mu.-integrable D (EFin \o f1) -> mu.-integrable D (EFin \o f2) ->
  \int[mu]_( in D) (f1 x + f2 x) =
  \int[mu]_( in D) f1 x + \int[mu]_( in D) f2 x.

Proof.

move=> mD if1 if2.
by rewrite /Rintegral integralD_EFin// fineD//; exact: integrable_fin_num.
Qed.

Lemma : measurable D ->
  mu.-integrable D (EFin \o f1) -> mu.-integrable D (EFin \o f2) ->
  \int[mu]_( in D) (f1 x - f2 x) =
  \int[mu]_( in D) f1 x - \int[mu]_( 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 ( : measurableType d) { : realType} ( : {measure set T -> \bar R}).
Local Open Scope ereal_scope.

Lemma ( : T -> \bar R) :
measurable_fun setT f -> (forall , 0 <= f x) ->
semi_sigma_additive (fun => \int[mu]_( 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_measure_of_density (only parsing).

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

Definition ( : T -> R) ( : measurable_fun [set: T] f)
    ( : forall , 0 <= f x) :=
  fun => (\int[mu]_( in A) (f t)%:E)%E.

End measure_of_density_def.

Section measure_of_density.
Import MeasurableR.
Context {} { : measurableType d} { : realType}
  ( : {measure set T -> \bar R}) ( : T -> R).

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

Local Notation := (measure_of_density mu mf f0).

Let : m' set0 = 0

Proof.

exact: integral_set0. Qed.

Let : (0 <= m' A)%E.

Proof.

by apply: integral_ge0 => t At; rewrite lee_fin. Qed.

Let : semi_sigma_additive m'.

Proof.

by apply: semi_sigma_additive_measure_of_density => //; exact/measurable_EFinP.
Qed.

..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 {} { : measurableType d} { : realType}
  ( : {measure set T -> \bar R}) ( : T -> R).

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

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

#[local] Lemma ( : set T) : measurable A ->
  \int[mu]_ ((\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 ( : R) ( : set T) : measurable A ->
(0 <= r)%R ->
\int[mu]_ (r%:E * (\1_A x)%:E * (h x)%:E) = r%:E * mu' A.

Proof.

move=> mA r0.
under eq_integral do rewrite -muleA.
rewrite ge0_integralZl//=.
- apply: emeasurable_funM => //; by apply /measurable_EFinP.
- by move=> x _; apply: mule_ge0; rewrite ?lee_fin.
- by rewrite integral_measure_of_density_indic.
Qed.

Import HBNNSimple.

#[local] Lemma ( : {nnsfun T >-> R}) :
sintegral mu' g = \int[mu]_ ((g x)%:E * (h x)%:E).

Proof.

transitivity (\sum_( \in range g)
    \int[mu]_ (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]_ (\sum_( \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 ( : T -> \bar R) :
measurable_fun [set: T] f -> (forall , 0 <= f x) ->
\int[mu']_ f x = \int[mu]_ (f x * (h x)%:E).

Proof.

move=> mf f0.
pose g := nnsfun_approx measurableT mf.
pose gE := fun => 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 : / (n <= p)%O >-> n <= p}.
  by move=> *; exact/lefP/nd_nnsfun_approx.
transitivity (limn (fun => \int[mu']_ gE n x)).
  rewrite -monotone_convergence//; apply: eq_integral => t _.
  by apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx.
transitivity (limn (fun => \int[mu]_ (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 => 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 => gE n x * (h x)%:E) : / (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 { : realType}.
Notation := (@lebesgue_measure R).
Implicit Type f : R -> R.

Import MeasurableR.

Lemma ( : itv_bound R) ( : R) :
  mu.-integrable [set` Interval a (BLeft r)] (EFin \o f) ->
   \int[mu]_( in [set` Interval a (BLeft r)]) (f x) =
   \int[mu]_( in [set` Interval a (BRight r)]) (f x).

Proof.

move=> mf; rewrite /Rintegral integral_itvbo_itvbc//.
exact: (measurable_int mu).
Qed.

Lemma ( : R) ( : itv_bound R) :
  mu.-integrable [set` Interval (BRight r) b] (EFin \o f) ->
  \int[mu]_( in [set` Interval (BRight r) b]) (f x) =
  \int[mu]_( in [set` Interval (BLeft r) b]) (f x).

Proof.

move=> mf; rewrite /Rintegral integral_itvob_itvcb//.
exact: (measurable_int mu).
Qed.

Lemma ( : R) : \int[mu]_( in [set r]) f x = 0.

Proof.

by rewrite /Rintegral integral_set1. Qed.

Lemma ( : itv_bound R) :
  mu.-integrable [set` (Interval a b)] (EFin \o f) ->
  (a <= BRight x)%O -> (BRight x <= b)%O ->
  \int[mu]_( in [set` Interval a b]) f t -
  \int[mu]_( in [set` Interval a (BRight x)]) f t =
  \int[mu]_( 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_itvbo_itvbc (only parsing).
#[deprecated(since="mathcomp-analysis 1.17.0", use=Rintegral_itvob_itvcb)]
Notation := Rintegral_itvob_itvcb (only parsing).

Section Rdominated_convergence.
Context {} { : measurableType d} { : realType}
  ( : {measure set T -> \bar R}) ( : set T) ( : measurable D)
  ( : (T -> R)^nat) ( : T -> R).
Import MeasurableR.
Hypotheses ( : forall , measurable_fun D (f_ n))
  ( : forall , D x -> f_ ^~ x @ \oo --> f x)
  ( : mu.-integrable D (EFin \o g))
  ( : forall , D x -> `|f_ n x| <= g x).

Lemma :
  \int[mu]_( in D) f_ n x @[ \oo] --> \int[mu]_( in D) f x.

Proof.

rewrite /Rintegral.
have []// := @dominated_convergence _ _ _ mu _ mD (fun => (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.

Files

Module mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral