Module mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral

# The Lebesgue Integral for real-valued functions Detailed contents: ``` Rintegral mu D f := fine (\int[mu]_(x in D) f x). ``` This file recasts lemmas about `integral` to `Rintegral`. It also established that Continuous functions are dense in $L^1$.

Unset SsrOldRewriteGoalsOrder.
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}.
Variable : {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.
#[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `le_normr_Rintegral`")]
Notation := le_normr_Rintegral (only parsing).

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