Module mathcomp.analysis.lebesgue_integral_theory.lebesgue_integrable

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrnum ssrint interval.
From mathcomp Require Import archimedean interval_inference finmap.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality reals fsbigop topology ereal tvs.
From mathcomp Require Import normedtype sequences real_interval esum measure.
From mathcomp Require Import lebesgue_measure numfun realfun simple_functions.
From mathcomp Require Import measurable_realfun 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.

# Theory of Lebesgue-integrable functions This file contains a theory for Lebesgue-integrable functions: linearity, order, union, subset, etc. of the domain of integration. Main reference: - Daniel Li, Intégration et applications, 2016 Detailed contents: ``` mu.-integrable D f == f is measurable over D and the integral of f w.r.t. D is < +oo ```

Reserved Notation "mu .-integrable" (at level 2, format "mu .-integrable").

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

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

. { : measurableType d} { : realType}
    ( : set T -> \bar R) :=
  `[< measurable_fun D f /\ (\int[mu]_( in D) `|f x| < +oo)%E >].
Canonical := Unlockable integrable.unlock.

Notation := (integrable mu) : type_scope.

Lemma :
  reflect (measurable_fun D f /\ (\int[mu]_( in D) `|f x| < +oo)%E)
    (@integrable d T R mu D f).

Proof.

by rewrite unlock; apply/(iffP (asboolP _)). Qed.

Section negligible_integrable.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType)
  ( : {measure set T -> \bar R}).

Lemma ( : set T) ( : T -> \bar R) :
  measurable N -> measurable D -> measurable_fun D f ->
  mu N = 0 -> mu.-integrable D f <-> mu.-integrable (D `\` N) f.

Proof.

move=> mN mD mf muN0.
pose mCN := measurableC mN.
have /integrableP intone : mu.-integrable D (f \_ N).
  apply/integrableP; split.
    by apply/measurable_restrict => //; exact: measurable_funS mf.
  rewrite (eq_integral ((abse \o f) \_ N)).
    by move=> t _; rewrite restrict_abse.
  rewrite -integral_mkcondr integral_abs_eq0//.
  - exact: measurableI.
  - exact: measurable_funS mf.
  - by apply: (subset_measure0 _ _ _ muN0) => //; exact: measurableI.
have h1 : mu.-integrable D f <-> mu.-integrable D (f \_ (~` N)).
  split=> [/integrableP intf|/integrableP intCf].
    apply/integrableP; split.
      by apply/measurable_restrict => //; exact: measurable_funS mf.
    rewrite (eq_integral ((abse \o f) \_ (~` N))).
      by move=> t _; rewrite restrict_abse.
    rewrite -integral_mkcondr; case: intf => _; apply: le_lt_trans.
    by apply: ge0_subset_integral => //=; [exact:measurableI|
                                           exact:measurableT_comp].
  apply/integrableP; split => //; rewrite (funID N f).
  have mDfcN : measurable_fun D (f \_ (~` N)).
    by apply/measurable_restrict => //; exact: measurable_funS mf.
  have mDfN : measurable_fun D (f \_ N).
    by apply/measurable_restrict => //; exact: measurable_funS mf.
  apply: (@le_lt_trans _ _
    (\int[mu]_( in D) (`|(f \_ (~` N)) x| + `|(f \_ N) x|))).
    apply: ge0_le_integral => //.
    - by apply: measurableT_comp => //; exact: emeasurable_funD.
    - by apply: emeasurable_funD; exact: measurableT_comp.
    - by move=> *; rewrite lee_abs_add.
  rewrite ge0_integralD//; [exact: measurableT_comp..|].
  by apply: lte_add_pinfty; [case: intCf|case: intone].
suff : mu.-integrable D (f \_ (~` N)) <-> mu.-integrable (D `\` N) f.
  exact: iff_trans.
apply: iff_sym.
split=> [/integrableP intCf|/integrableP intCf]; apply/integrableP.
- split.
  + by apply/measurable_restrict => //; exact: measurable_funS mf.
  + rewrite (eq_integral ((abse \o f) \_ (~` N))).
      by move=> t _; rewrite restrict_abse.
    rewrite -integral_mkcondr //; case: intCf => _; apply: le_lt_trans.
    apply: ge0_subset_integral => //=; [exact: measurableI|exact: measurableD|].
    by apply: measurableT_comp => //; apply: measurable_funS mf => // ? [].
- split.
  + move=> mDN A mA; rewrite setDE (setIC D) -setIA; apply: measurableI => //.
    exact: mf.
  + rewrite integral_mkcondr/=.
    under eq_integral do rewrite restrict_abse.
    by case: intCf.
Qed.

End negligible_integrable.

Lemma :
@integrable d T R mu D f -> measurable_fun D f.

Proof.

by rewrite unlock => /asboolP[]. Qed.

Arguments measurable_int {d T R} mu {D f}.

Section integrable_theory.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType).
Variables : {measure set T -> \bar R}.
Variables ( : set T) ( : measurable D).
Implicit Type f g : T -> \bar R.

Notation := (integrable mu D).

Lemma : mu_int (cst 0).

Proof.

apply/integrableP; split=> //; under eq_integral do rewrite (gee0_abs (lexx 0)).
by rewrite integral0.
Qed.

Lemma : mu.-integrable set0 f.

Proof.

apply/integrableP; split; first exact: measurable_fun_set0.
by rewrite integral_set0.
Qed.

Lemma : {in D, f =1 g} -> mu_int f -> mu_int g.

Proof.

move=> fg /integrableP[mf fi]; apply/integrableP; split.
  exact: eq_measurable_fun mf.
rewrite (le_lt_trans _ fi)//; apply: ge0_le_integral=> //.
  by apply: measurableT_comp => //; exact: eq_measurable_fun mf.
  by apply: measurableT_comp => //; exact: eq_measurable_fun mf.
by move=> x Dx; rewrite fg// inE.
Qed.

Lemma : measurable_fun D f ->
(forall , D x -> `|f x| <= `|g x|) -> mu_int g -> mu_int f.

Proof.

move=> mf fg /integrableP[mfg goo]; apply/integrableP; split => //.
by apply: le_lt_trans goo; apply: ge0_le_integral => //; exact: measurableT_comp.
Qed.

Lemma : mu_int f -> mu_int (-%E \o f).

Proof.

move=> /integrableP[mf foo]; apply/integrableP; split; last first.
by rewrite /comp; under eq_fun do rewrite abseN.
by rewrite /comp; exact: measurableT_comp.
Qed.

Lemma ( : R) : mu_int f -> mu_int (fun => k%:E * f x).

Proof.

move=> /integrableP[mf foo]; apply/integrableP; split.
exact: measurable_funeM.
under eq_fun do rewrite abseM.
by rewrite ge0_integralZl// ?lte_mul_pinfty//; exact: measurableT_comp.
Qed.

Lemma ( : R) : mu_int f -> mu_int (f \* cst k%:E).

Proof.

by move=> mf; apply: eq_integrable (integrableZl k mf) => // x; rewrite muleC.
Qed.

Lemma : mu_int f -> mu_int g -> mu_int (f \+ g).

Proof.

move=> /integrableP[mf foo] /integrableP[mg goo]; apply/integrableP; split.
  exact: emeasurable_funD.
apply: (@le_lt_trans _ _ (\int[mu]_( in D) (`|f x| + `|g x|))).
  apply: ge0_le_integral => //.
  - by apply: measurableT_comp => //; exact: emeasurable_funD.
  - by apply: emeasurable_funD; apply: measurableT_comp.
  - by move=> *; exact: lee_abs_add.
by rewrite ge0_integralD //; [exact: measurableT_comp..|exact: lte_add_pinfty].
Qed.

Lemma ( : seq I) ( : pred I) ( : I -> T -> \bar R) :
(forall , P i -> mu_int (h i)) ->
mu_int (fun => \sum_( <- s | P i) h i x).

Proof.

elim: s => [_|i s ih hs].
by under eq_fun do rewrite big_nil; exact: integrable0.
under eq_fun do rewrite big_cons.
have [Pi|Pi] := boolP (P i); last exact: ih.
by apply: integrableD => //; [exact: hs|exact: ih].
Qed.

Lemma : mu_int f -> mu_int g -> mu_int (f \- g).

Proof.

by move=> fi gi; exact/(integrableD fi)/integrableN. Qed.

Lemma : mu_int f ->
\int[mu]_( in D) f^\+ x +? - (\int[mu]_( in D) f^\- x).

Proof.

move=> /integrableP[mf]; rewrite -[fun => _]/(abse \o f) -funeposDneg => foo.
rewrite ge0_integralD // in foo; [exact: measurable_funepos|
exact: measurable_funeneg|].
apply: ltpinfty_adde_def.
- by apply: le_lt_trans foo; rewrite leeDl// integral_ge0.
- by rewrite inE (@le_lt_trans _ _ 0)// leeNl oppe0 integral_ge0.
Qed.

Lemma : mu_int f -> mu_int f^\+.

Proof.

move=> /integrableP[Df foo]; apply/integrableP; split.
exact: measurable_funepos.
apply: le_lt_trans foo; apply: ge0_le_integral => //.
- by apply/measurableT_comp => //; exact: measurable_funepos.
- exact/measurableT_comp.
- by move=> t Dt; rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDl.
Qed.

Lemma : mu_int f -> mu_int f^\-.

Proof.

move=> /integrableP[Df foo]; apply/integrableP; split.
exact: measurable_funeneg.
apply: le_lt_trans foo; apply: ge0_le_integral => //.
- by apply/measurableT_comp => //; exact: measurable_funeneg.
- exact/measurableT_comp.
- by move=> t Dt; rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDr.
Qed.

Lemma : mu_int f -> \int[mu]_( in D) f^\- x < +oo.

Proof.

move=> /integrableP[mf]; apply: le_lt_trans; apply: ge0_le_integral => //.
- exact: measurable_funeneg.
- exact: measurableT_comp.
- move=> x Dx; have /orP[fx0|fx0] := le_total (f x) 0.
    by rewrite lee0_abs// funenegE ge_max lexx leeNr oppe0 fx0.
  rewrite gee0_abs// funenegE.
  by move: (fx0); rewrite -{1}oppe0 -leeNl => /max_idPr ->.
Qed.

Lemma : mu_int f -> \int[mu]_( in D) f^\+ x < +oo.

Proof.

move=> /integrableP[mf]; apply: le_lt_trans; apply: ge0_le_integral => //.
- exact: measurable_funepos.
- exact: measurableT_comp.
- move=> x Dx; have [fx0|/ltW fx0] := leP (f x) 0.
    rewrite lee0_abs// funeposE.
    by move: (fx0) => /max_idPr ->; rewrite -leeNr oppe0.
  by rewrite gee0_abs// funeposE; move: (fx0) => /max_idPl ->.
Qed.

Lemma :
mu_int f -> \int[mu]_( in D) f^\- x \is a fin_num.

Proof.

move=> /integrableP fi.
rewrite fin_numElt; apply/andP; split.
by rewrite (@lt_le_trans _ _ 0) ?lte_ninfty//; exact: integral_ge0.
case: fi => mf; apply: le_lt_trans; apply: ge0_le_integral => //.
- exact/measurable_funeneg.
- exact/measurableT_comp.
- by move=> x Dx; rewrite -/((abse \o f) x) -funeposDneg leeDr.
Qed.

Lemma :
mu_int f -> \int[mu]_( in D) f^\+ x \is a fin_num.

Proof.

move=> /integrableP fi.
rewrite fin_numElt; apply/andP; split.
by rewrite (@lt_le_trans _ _ 0) ?lte_ninfty//; exact: integral_ge0.
case: fi => mf; apply: le_lt_trans; apply: ge0_le_integral => //.
- exact/measurable_funepos.
- exact/measurableT_comp.
- by move=> x Dx; rewrite -/((abse \o f) x) -funeposDneg leeDl.
Qed.

Import MeasurableR.

Lemma ( : T -> R) :
measurable_fun D h -> [bounded h x | in D] ->
mu_int g -> mu_int ((EFin \o h) \* g).

Proof.

move=> mh [M [Mreal Mh]] gi; apply/integrableP; split.
  by apply: emeasurable_funM => //; [exact: measurableT_comp|
                                     exact: measurable_int gi].
under eq_integral do rewrite abseM.
have: \int[mu]_( in D) (`|M + 1|%:E * `|g x|) < +oo.
  rewrite ge0_integralZl ?lte_mul_pinfty//; last by case/integrableP : gi.
  by apply: measurableT_comp => //; exact: measurable_int gi.
apply/le_lt_trans/ge0_le_integral => //.
- apply/emeasurable_funM; last exact/measurableT_comp/(measurable_int _ gi).
  exact/measurable_EFinP/measurableT_comp.
- apply/emeasurable_funM => //; apply/measurableT_comp => //.
  exact: measurable_int gi.
- move=> x Dx; rewrite lee_wpmul2r//= lee_fin Mh//=.
  by rewrite (lt_le_trans _ (ler_norm _))// ltrDl.
Qed.

Lemma ( : T -> R) :
mu_int f -> measurable_fun D h -> [bounded h x | in D] ->
mu_int (f \* (EFin \o h)).

Proof.

move=> fi mh mg; rewrite /is_true -(integrableMr mh mg fi).
by apply/congr1/funext => ?; rewrite muleC.
Qed.

Lemma ( : set T) ( : d.-measurable E) :
integrable mu (E `&` D) f <-> integrable mu E (f \_ D).

Proof.

split; move=> /integrableP[mf intfoo]; apply/integrableP; split.
- exact/measurable_restrict.
- by move: intfoo; rewrite integral_mkcondr/= restrict_abse.
- exact/measurable_restrict.
- by move: intfoo; rewrite integral_mkcondr/= restrict_abse.
Qed.

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

Proof.

move=> intf intg fg; rewrite integralE [leRHS]integralE leeB//.
- apply: ge0_le_integral => //.
  + by move/integrableP : intf => [+ _]; exact: measurable_funepos.
  + by move/integrableP : intg => [+ _]; exact: measurable_funepos.
  + by move=> x /mem_set; exact: funepos_le.
- apply: ge0_le_integral => //.
  + by move/integrableP : intg => [+ _]; exact: measurable_funeneg.
  + by move/integrableP : intf => [+ _]; exact: measurable_funeneg.
  + by move=> x /mem_set; exact: funeneg_le.
Qed.

Lemma : mu_int f -> mu_int (abse \o f).

Proof.

move=> /integrableP[mf foo]; apply/integrableP; split.
exact: measurableT_comp.
by under eq_integral do rewrite abse_id.
Qed.

End integrable_theory.
Arguments eq_integrable {d T R mu D} mD f.

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

Import MeasurableR.

Lemma : mu.-integrable D (EFin \o f) ->
mu.-integrable D (EFin \o (normr \o f)).

Proof.

move=> /integrableP[mf foo]; apply/integrableP; split.
do 2 apply: measurableT_comp => //.
exact/measurable_EFinP.
by under eq_integral do rewrite /= normr_id.
Qed.

Lemma ( : measurable A) :
(mu A < +oo)%E -> measurable_fun A f ->
[bounded f x | in A] -> mu.-integrable A (EFin \o f).

Proof.

move=> Afin mfA bdA; apply/integrableP; split; first exact/measurable_EFinP.
have [M [_ mrt]] := bdA; apply: le_lt_trans.
apply: (integral_le_bound (`|M| + 1)%:E) => //; first exact: measurableT_comp.
by apply: aeW => z Az; rewrite lee_fin mrt// ltr_pwDr// ler_norm.
by rewrite lte_mul_pinfty.
Qed.

Lemma : measurable A ->
mu.-integrable A (EFin \o f) -> mu.-integrable A (EFin \o f^\+).

Proof.

by move/integrable_funepos => /[apply]; rewrite funerpos. Qed.

Lemma : measurable A ->
mu.-integrable A (EFin \o f) -> mu.-integrable A (EFin \o f^\-).

Proof.

by move/integrable_funeneg => /[apply]; rewrite funerneg. Qed.

End Rintegrable.

Import MeasurableR.

Lemma { : realType} ( : R) ( : bool) :
let := lebesgue_measure in
mu.-integrable setT (EFin \o \1_[set` Interval (BSide b0 a) (BSide b1 b)]).

Proof.

have [ab|ba] := leP a b; last first.
  rewrite set_itv_ge//; last by rewrite indic0//; exact: integrable0.
  by rewrite -leNgt leBSide; move: b0 b1 => [] []//=; exact/ltW.
set i := [set` _]; rewrite (_ : _ \o _ = (cst 1%E) \_ i).
  by apply/funext => r/=; rewrite indic_restrict restrict_EFin.
rewrite {}/i; apply/integrable_restrict => //=.
rewrite setTI; apply: measurable_bounded_integrable => //=.
  rewrite lebesgue_measure_itv//=.
  by case: ifPn => // _; rewrite -EFinB ltry.
exact: bounded_cst.
Qed.

Section integrable_finite_measure.
Context ( : measurableType d) { : realType}.
Variable : {finite_measure set T -> \bar R}.
Local Open Scope ereal_scope.

Lemma : measurable A ->
mu.-integrable [set: T] (fun : T => (\1_A x)%:E).

Proof.

move=> mA; apply/integrableP; split; first exact/measurable_EFinP.
rewrite (eq_integral (fun => (\1_A x)%:E)).
by move=> t _; rewrite gee0_abs// lee_fin.
rewrite integral_indic// setIT.
rewrite (@le_lt_trans _ _ (mu setT)) ?le_measure ?inE//.
by rewrite ?ltry ?fin_num_fun_lty//; exact: fin_num_measure.
Qed.

Lemma :
measurable A -> mu.-integrable A (EFin \o cst k).

Proof.

move=> mA; apply/integrableP; split; first exact/measurable_EFinP.
have [k0|k0] := leP 0%R k.
- under eq_integral do rewrite /= ger0_norm//.
  rewrite lebesgue_integral_nonneg.integral_cstr//= lte_mul_pinfty//.
  by rewrite -ge0_fin_numE// fin_num_measure.
- under eq_integral do rewrite /= ltr0_norm//.
  rewrite lebesgue_integral_nonneg.integral_cstr//= lte_mul_pinfty//.
    by rewrite lee_fin lerNr oppr0 ltW.
  by rewrite -ge0_fin_numE// fin_num_measure.
Qed.

End integrable_finite_measure.

Section integrable_domain.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType)
        ( : {measure set T -> \bar R}).

Lemma ( : set T) ( : T -> \bar R) :
  measurable E -> measurable D -> D `<=` E ->
  mu.-integrable E f -> mu.-integrable D f.

Proof.

move=> mE mD DE /integrableP[mf ifoo]; apply/integrableP; split.
exact: measurable_funS mf.
apply: le_lt_trans ifoo; apply: ge0_subset_integral => //.
exact: measurableT_comp.
Qed.

Lemma : measurable D ->
mu.-integrable D f <-> mu.-integrable setT (f \_ D).

Proof.

move=> mD.
rewrite unlock; apply: asbool_equiv; rewrite [in X in X <-> _]integral_mkcond.
under [in X in X <-> _]eq_integral do rewrite restrict_abse.
split => [|] [mf foo].
- by split; [exact/(measurable_restrictT _ _).1| exact: le_lt_trans foo].
- by split; [exact/(measurable_restrictT _ _).2| exact: le_lt_trans foo].
Qed.

End integrable_domain.
Arguments integrable_mkcond {d T R mu D} f.

Section integrable_ae.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType).
Variables ( : {measure set T -> \bar R}) ( : set T) ( : measurable D).
Variable : T -> \bar R.
Hypotheses : mu.-integrable D f.

Lemma : {ae mu, forall , D x -> f x \is a fin_num}.

Proof.

have [muD0|muD0] := eqVneq (mu D) 0.
  by exists D; split => // t /= /not_implyP[].
pose E := [set | `|f x| = +oo /\ D x ].
have mE : measurable E.
  rewrite (_ : E = D `&` f @^-1` [set -oo; +oo]); last first.
    by apply: (measurable_int _ fint) => //; exact: measurableU.
  rewrite /E predeqE => t; split=> [[/eqP]|[Dt [|]/= ->//]].
  by rewrite eqe_absl leey andbT /preimage/= => /orP[|]/eqP; tauto.
have [ET|ET] := eqVneq E setT.
  have foo t : `|f t| = +oo by have [] : E t by rewrite ET.
  suff: \int[mu]_( in D) `|f x| = +oo.
    by case: (integrableP _ _ _ fint) => _; rewrite ltey => /eqP.
  by rewrite -(lebesgue_integral_nonneg.integral_csty mD muD0)//; exact: eq_integral.
suff: mu E = 0.
  move=> muE0; exists E; split => // t /= /not_implyP[Dt].
  by rewrite fin_num_abs => /negP; rewrite -leNgt leye_eq => /eqP.
have [->|/set0P E0] := eqVneq E set0; first by rewrite measure0.
have [M M0 muM] : exists2 , (0 <= M)%R &
    forall , n%:R%:E * mu (E `&` D) <= M%:E.
  exists (fine (\int[mu]_( in D) `|f x|)); first exact/fine_ge0/integral_ge0.
  move=> n; rewrite -integral_indic// -ge0_integralZl//.
    exact: measurableT_comp.
  rewrite fineK//.
    case: (integrableP _ _ _ fint) => _ foo.
    by rewrite ge0_fin_numE// integral_ge0.
  apply: ge0_le_integral => //.
  - exact/measurable_EFinP/measurableT_comp.
  - by apply: measurableT_comp => //; exact: measurable_int fint.
  - move=> x Dx; rewrite /= indicE.
    have [|xE] := boolP (x \in E); last by rewrite mule0.
    by rewrite /E inE /= => -[->]; rewrite leey.
apply/eqP/negPn/negP => /eqP muED0; move/not_forallP : muM; apply.
have [muEDoo|] := ltP (mu (E `&` D)) +oo; last first.
  by rewrite leye_eq => /eqP ->; exists 1%N; rewrite mul1e leye_eq.
exists (truncn (M * (fine (mu (E `&` D)))^-1)).+1.
apply/negP; rewrite -ltNge.
rewrite -[X in _ * X](@fineK _ (mu (E `&` D))).
  by rewrite fin_numElt muEDoo (lt_le_trans _ (measure_ge0 _ _)).
rewrite lte_fin -ltr_pdivrMr; last by rewrite truncnS_gt.
rewrite -lte_fin fineK.
  by rewrite ge0_fin_numE// measure_ge0//; exact: measurableI.
rewrite lt0e measure_ge0 andbT.
suff: E `&` D = E by move=> ->; exact/eqP.
by rewrite predeqE => t; split=> -[].
Qed.

End integrable_ae.

Section integralZl.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType).
Variables ( : {measure set T -> \bar R}) ( : set T) ( : measurable D).
Variable ( : T -> \bar R).
Hypothesis : mu.-integrable D f.

Let : measurable_fun D f

Proof.

exact: measurable_int intf. Qed.

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

Proof.

have /orP[r0|r0] := le_total r 0%R.
- rewrite [in LHS]integralE// le0_funeposM// le0_funenegM//.
  rewrite (ge0_integralZl_EFin _ _ _ (measurable_funeneg _)) ?oppr_ge0//.
  rewrite (ge0_integralZl_EFin _ _ _ (measurable_funepos _)) ?oppr_ge0//.
  rewrite !EFinN addeC !mulNe oppeK -muleBr ?integrable_add_def//.
  by rewrite [in RHS]integralE.
- rewrite [in LHS]integralE// ge0_funeposM// ge0_funenegM//=.
  rewrite (ge0_integralZl_EFin _ _ _ (measurable_funepos _) r0)//.
  rewrite (ge0_integralZl_EFin _ _ _ (measurable_funeneg _) r0)//.
  by rewrite -muleBr 1?[in RHS]integralE// integrable_add_def.
Qed.

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

Proof.

by rewrite muleC -integralZl; under eq_integral do rewrite muleC. Qed.

End integralZl.

Section integralD_EFin.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType).
Variables ( : {measure set T -> \bar R}) ( : set T) ( : measurable D).
Variables : T -> R.
Let := EFin \o f1.
Let := EFin \o f2.
Hypothesis : mu.-integrable D g1.
Hypothesis : mu.-integrable D g2.

Let : measurable_fun D g1

Proof.

exact: measurable_int if1. Qed.

Let : measurable_fun D g2

Proof.

exact: measurable_int if2. Qed.

Lemma :
\int[mu]_( in D) (g1 \+ g2) x =
\int[mu]_( in D) g1 x + \int[mu]_( in D) g2 x.

Proof.

suff: \int[mu]_( in D) ((g1 \+ g2)^\+ x) + \int[mu]_( in D) (g1^\- x) +
        \int[mu]_( in D) (g2^\- x) =
      \int[mu]_( in D) ((g1 \+ g2)^\- x) + \int[mu]_( in D) (g1^\+ x) +
        \int[mu]_( in D) (g2^\+ x).
  move=> h; rewrite [in LHS]integralE.
  move/eqP : h; rewrite -[in eqbRHS]addeA [in eqbRHS]addeC.
  have g12pos :
      \int[mu]_( in D) (g1^\+ x) + \int[mu]_( in D) (g2^\+ x) \is a fin_num.
    rewrite ge0_fin_numE//.
      by rewrite adde_ge0// integral_ge0.
    by rewrite lte_add_pinfty//; exact: integral_funepos_lt_pinfty.
  have g12neg :
      \int[mu]_( in D) (g1^\- x) + \int[mu]_( in D) (g2^\- x) \is a fin_num.
    rewrite ge0_fin_numE//.
      by rewrite adde_ge0// integral_ge0.
    by rewrite lte_add_pinfty// ; exact: integral_funeneg_lt_pinfty.
  rewrite -sube_eq.
  - rewrite ge0_fin_numE.
      apply: adde_ge0; last exact: integral_ge0.
      by apply: adde_ge0; apply: integral_ge0.
    apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty.
    apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty.
    exact: integral_funepos_lt_pinfty (integrableD _ _ _).
  - exact/fin_num_adde_defr/g12pos.
  rewrite -[X in X - _ == _]addeA [X in X - _ == _]addeC -[eqbLHS]addeA.
  rewrite [eqbLHS]addeC eq_sym.
  rewrite -(sube_eq g12pos) ?fin_num_adde_defl// => /eqP g12E.
  rewrite -{}[LHS]g12E fin_num_oppeD; last first.
    by rewrite addeACA (integralE _ _ g1) (integralE _ _ g2).
  rewrite ge0_fin_numE; last exact: integral_funeneg_lt_pinfty if2.
  exact: integral_ge0.
have : (g1 \+ g2)^\+ \+ g1^\- \+ g2^\- = (g1 \+ g2)^\- \+ g1^\+ \+ g2^\+.
  rewrite funeqE => x.
  apply/eqP; rewrite -2!addeA [in eqbRHS]addeC -sube_eq.
  - by rewrite funeposE !funenegE -!fine_max.
  - by rewrite !funeposE funenegE -!fine_max.
  rewrite addeAC eq_sym -sube_eq.
  - by rewrite !funeposE -!fine_max.
  - by rewrite funeposE !funenegE -!fine_max.
  apply/eqP.
  rewrite -[LHS]/((g1^\+ \+ g2^\+ \- (g1^\- \+ g2^\-)) x) funeDB.
  by rewrite -[RHS]/((_ \- _) x) funeposBneg.
move/(congr1 (fun => \int[mu]_( in D) (y x) )).
rewrite (ge0_integralD mu mD).
  - by move=> x _; rewrite adde_ge0.
  - apply: emeasurable_funD; last exact: measurable_funeneg.
    exact/measurable_funepos/emeasurable_funD.
  - by [].
  - exact: measurable_funeneg.
rewrite (ge0_integralD mu mD).
  - by [].
  - exact/measurable_funepos/emeasurable_funD.
  - by [].
  - exact/measurable_funeneg.
move=> g12E; rewrite {}[LHS]g12E.
rewrite (ge0_integralD mu mD).
  - by move=> x _; exact: adde_ge0.
  - apply: emeasurable_funD; last exact: measurable_funepos.
    exact/measurable_funeneg/emeasurable_funD.
  - by [].
  - exact: measurable_funepos.
rewrite (ge0_integralD mu mD) //; last exact: measurable_funepos.
exact/measurable_funeneg/emeasurable_funD.
Qed.

End integralD_EFin.

Lemma ( : measurableType d) ( : realType)
  ( : {measure set T -> \bar R}) ( : set T) ( : T -> R)
  ( : measurable D) :
  mu.-integrable D (EFin \o f1) -> mu.-integrable D (EFin \o f2) ->
  (\int[mu]_( in D) ((f1 x)%:E - (f2 x)%:E) =
    (\int[mu]_( in D) (f1 x)%:E - \int[mu]_( in D) (f2 x)%:E))%E.

Proof.

move=> if1 if2; rewrite (integralD_EFin mD if1).
by rewrite (_ : _ \o _ = (fun => - (f2 x)%:E))%E; [by []|exact: integrableN].
by rewrite -integralN//; exact: integrable_add_def.
Qed.

Section integralD.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType).
Variables ( : {measure set T -> \bar R}) ( : set T) ( : measurable D).
Variables : T -> \bar R.
Hypotheses ( : mu.-integrable D f1) ( : mu.-integrable D f2).

Let : measurable_fun D f1

Proof.

exact: measurable_int if1. Qed.

Let : measurable_fun D f2

Proof.

exact: measurable_int if2. Qed.

Lemma : \int[mu]_( in D) (f1 x + f2 x) =
\int[mu]_( in D) f1 x + \int[mu]_( in D) f2 x.

Proof.

pose A := D `&` [set | f1 x \is a fin_num].
pose B := D `&` [set | f2 x \is a fin_num].
have mA : measurable A by exact: emeasurable_fin_num.
have mB : measurable B by exact: emeasurable_fin_num.
have mAB : measurable (A `&` B) by apply: measurableI.
pose g1 := (fine \o f1 \_ (A `&` B))%R.
pose g2 := (fine \o f2 \_ (A `&` B))%R.
have ig1 : mu.-integrable D (EFin \o g1).
  rewrite (_ : _ \o _ = f1 \_ (A `&` B)) //; last first.
    apply: (integrableS measurableT)=>//; apply/(integrable_mkcond _ _).1 => //.
    by apply: integrableS if1=>//; rewrite -setIAC -setIA; apply: subIset; left.
  rewrite /g1 funeqE => x //=; rewrite !/restrict; case: ifPn => //.
  rewrite 2!in_setI => /andP[/andP[xA f1xfin] _] /=.
  by rewrite fineK//; rewrite inE in f1xfin.
have mg1 := measurable_int _ ig1.
have ig2 : mu.-integrable D (EFin \o g2).
  rewrite (_ : _ \o _ = f2 \_ (A `&` B)) //; last first.
    apply: (integrableS measurableT)=>//; apply/(integrable_mkcond _ _).1 => //.
    by apply: integrableS if2=>//; rewrite -setIAC -setIA; apply: subIset; left.
  rewrite /g2 funeqE => x //=; rewrite !/restrict; case: ifPn => //.
  rewrite in_setI => /andP[_]; rewrite in_setI => /andP[xB f2xfin] /=.
  by rewrite fineK//; rewrite inE in f2xfin.
have mg2 := measurable_int _ ig2.
transitivity (\int[mu]_( in D) (EFin \o (g1 \+ g2)%R) x).
  apply: ae_eq_integral => //.
  - exact: emeasurable_funD.
  - rewrite (_ : _ \o _ = (EFin \o g1) \+ (EFin \o g2))//.
    exact: emeasurable_funD.
  - apply: (filterS2 _ _ (integrable_ae mD if1) (integrable_ae mD if2)).
    move=> x + + Dx => /(_ Dx) f1fin /(_ Dx) f2fin /=.
    rewrite EFinD /g1 /g2 /restrict /=; have [|] := boolP (x \in A `&` B).
      by rewrite in_setI => /andP[xA xB] /=; rewrite !fineK.
    by rewrite in_setI negb_and => /orP[|];
      rewrite in_setI negb_and /= (mem_set Dx)/= notin_setE/=.
- rewrite (_ : _ \o _ = (EFin \o g1) \+ (EFin \o g2))// integralD_EFin//.
  congr (_ + _); apply: ae_eq_integral => //.
  + apply: (filterS2 _ _ (integrable_ae mD if1) (integrable_ae mD if2)).
    move=> x + + Dx => /(_ Dx) f1fin /(_ Dx) f2fin /=; rewrite /g1 /restrict /=.
    have [/=|] := boolP (x \in A `&` B); first by rewrite fineK.
    by rewrite in_setI negb_and => /orP[|];
      rewrite in_setI negb_and /= (mem_set Dx) /= notin_setE/=.
  + apply: (filterS2 _ _ (integrable_ae mD if1) (integrable_ae mD if2)).
    move=> x + + Dx => /(_ Dx) f1fin /(_ Dx) f2fin /=; rewrite /g2 /restrict /=.
    have [/=|] := boolP (x \in A `&` B); first by rewrite fineK.
    by rewrite in_setI negb_and => /orP[|];
      rewrite in_setI negb_and /= (mem_set Dx) /= notin_setE.
Qed.

End integralD.

Section integral_sum.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType).
Variables ( : {measure set T -> \bar R}) ( : set T) ( : measurable D).
Variables ( : Type) ( : I -> (T -> \bar R)).
Hypothesis : forall , mu.-integrable D (f n).

Lemma ( : seq I) ( : pred I) :
\int[mu]_( in D) (\sum_( <- s | P k) f k x) =
\sum_( <- s | P k) \int[mu]_( in D) (f k x).

Proof.

elim: s => [|h t ih].
  under eq_integral do rewrite big_nil.
  by rewrite integral0 big_nil.
rewrite big_cons -ih -integralD//; first exact: integrable_sum.
case: ifPn => Ph.
  by apply: eq_integral => x xD; rewrite big_cons Ph.
by apply: eq_integral => x xD; rewrite big_cons/= (negbTE Ph).
Qed.

End integral_sum.

Section integralB.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType).
Variables ( : {measure set T -> \bar R}) ( : set T).
Variables ( : measurable D) ( : T -> \bar R).
Hypotheses ( : mu.-integrable D f1) ( : mu.-integrable D f2).

Lemma : \int[mu]_( in D) (f1 \- f2) x =
\int[mu]_( in D) f1 x - \int[mu]_( in D) f2 x.

Proof.

rewrite -[in RHS](@integralN _ _ _ _ _ f2); first exact: integrable_add_def.
by rewrite -[in RHS]integralD//; exact: integrableN.
Qed.

End integralB.

Section integrable_lty_fin_num.
Context ( : measurableType d) ( : realType).
Variables ( : {measure set T -> \bar R}) ( : set T) ( : measurable D).
Local Open Scope ereal_scope.

Lemma ( : T -> \bar R) :
mu.-integrable D f -> \int[mu]_( in D) f x < +oo.

Proof.

move=> intf; rewrite -(funeposBneg f) integralB//;
[exact: integrable_funepos|exact: integrable_funeneg|].
rewrite lte_add_pinfty ?integral_funepos_lt_pinfty// lteNl ltNye_eq.
by rewrite integrable_neg_fin_num.
Qed.

Lemma ( : T -> \bar R) :
mu.-integrable D f -> \int[mu]_( in D) f x \is a fin_num.

Proof.

move=> h; apply/fin_numPlt; rewrite integrable_lty// andbC/= -/(- +oo).
rewrite lteNl -integralN; last exact/integrable_lty/integrableN.
by rewrite fin_num_adde_defl// fin_numN integrable_neg_fin_num.
Qed.

End integrable_lty_fin_num.
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `integrable_lty`")]
Notation := integrable_lty (only parsing).
#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `integrable_fin_num`")]
Notation := integrable_fin_num (only parsing).

Section transfer.
Context ( : measurableType d1) ( : measurableType d2) ( : realType).
Variable : X -> Y.
Hypothesis : measurable_fun [set: X] phi.
Variable : {measure set X -> \bar R}.
Variables : set Y.
Variables : Y -> \bar R.
Hypotheses ( : measurable_fun [set: Y] f)
( : mu.-integrable (phi @^-1` D) (f \o phi)).
Let := isMeasurableFun.Build _ _ _ _ _ mf.
Let := MeasurableFun.Pack (MeasurableFun.Class mf_mixin).

Lemma :
measurable D -> (pushforward mu phi).-integrable D f.

Proof.

move=> mD; apply/integrableP; split; first exact: (measurable_funP mf_pack).
move/integrableP : (intf) => [_]; apply: le_lt_trans.
rewrite ge0_integral_pushforward//.
by apply: measurableT_comp => //; exact: measurable_funTS.
Qed.

Local Open Scope ereal_scope.

Lemma : measurable D ->
\int[pushforward mu phi]_( in D) f y =
\int[mu]_( in phi @^-1` D) (f \o phi) x.

Proof.

move=> mD.
rewrite [RHS]integralE.
under [X in X - _]eq_integral do rewrite funepos_comp/=.
under [X in _ - X]eq_integral do rewrite funeneg_comp.
rewrite -[X in _ = X - _]ge0_integral_pushforward//.
exact/measurable_funepos/measurable_funTS.
rewrite -[X in _ = _ - X]ge0_integral_pushforward//.
exact/measurable_funeneg/measurable_funTS.
rewrite -integralB//=.
- by apply: integrable_funepos => //=; exact: integrable_pushforward.
- by apply: integrable_funeneg => //=; exact: integrable_pushforward.
- by apply/eq_integral=> // x _; rewrite -[in LHS](funeposBneg f).
Qed.

End transfer.

Section negligible_integral.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType)
        ( : {measure set T -> \bar R}).

Lemma ( : set T) ( : T -> \bar R) :
  measurable N -> measurable D -> mu.-integrable D f ->
  mu N = 0 -> \int[mu]_( in D) f x = \int[mu]_( in D `\` N) f x.

Proof.

move=> mN mD mf muN0; rewrite -[f]funeposBneg ?integralB//.
- exact: integrable_funepos.
- exact: integrable_funeneg.
- exact: measurableD.
- apply: (integrableS mD) => //; first exact: measurableD.
  exact: integrable_funepos.
- apply: (integrableS mD) => //; first exact: measurableD.
  exact: integrable_funeneg.
congr (_ - _); apply: ge0_negligible_integral => //; apply: (measurable_int mu).
  exact: integrable_funepos.
exact: integrable_funeneg.
Qed.

Lemma ( : set T) ( : T -> \bar R) :
measurable N -> measurable_fun N f -> mu N = 0 -> mu.-integrable N f.

Proof.

move=> mN mf muN0.
by rewrite (negligible_integrable mN) ?setDv//; exact: integrable_set0.
Qed.

Lemma ( : set T) ( : T -> \bar R) :
measurable N -> measurable_fun N f -> mu N = 0 -> \int[mu]_( in N) f x = 0.

Proof.

move=> mN mf N0.
rewrite (negligible_integral mN mN) ?setDv ?integral_set0//.
exact: null_set_integrable.
Qed.

End negligible_integral.
Add Search Blacklist "ge0_negligible_integral".

Section integral_measure_add.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType)
( : {measure set T -> \bar R}) ( : set T).
Hypothesis : measurable D.
Variable : T -> \bar R.
Hypothesis : m1.-integrable D f.
Hypothesis : m2.-integrable D f.
Hypothesis : measurable_fun D f.

Lemma : \int[measure_add m1 m2]_( in D) f x =
\int[m1]_( in D) f x + \int[m2]_( in D) f x.

Proof.

transitivity (\int[m1]_( in D) (f^\+ \- f^\-) x +
              \int[m2]_( in D) (f^\+ \- f^\-) x); last first.
  by congr +%E; apply: eq_integral => x _; rewrite -[in RHS](funeposBneg f).
rewrite integralB//; [exact: integrable_funepos|exact: integrable_funeneg|].
rewrite integralB//; [exact: integrable_funepos|exact: integrable_funeneg|].
rewrite addeACA -ge0_integral_measure_add//.
  by apply: measurable_funepos; exact: measurable_int intf1.
rewrite -oppeD; first by rewrite ge0_adde_def// inE integral_ge0.
rewrite -ge0_integral_measure_add// 1?integralE//.
by apply: measurable_funeneg; exact: measurable_int intf1.
Qed.

End integral_measure_add.

Section subadditive_countable.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType).
Variable ( : {measure set T -> \bar R}).

Lemma ( : (set T)^nat) ( : T -> \bar R):
  trivIset setT F -> (forall , measurable (F k)) ->
  mu.-integrable (\bigcup_ F k) g ->
  summable [set: nat] (fun => \int[mu]_( in F i) g x).

Proof.

move=> tF mF fi.
rewrite /summable -(_ : [set _ | true] = setT); first exact/seteqP.
rewrite -nneseries_esum//.
have [mf {fi}] := integrableP _ _ _ fi.
rewrite ge0_integral_bigcup//; first exact: measurableT_comp.
apply: le_lt_trans; apply: lee_lim.
- exact: is_cvg_ereal_nneg_natsum_cond.
- by apply: is_cvg_ereal_nneg_natsum_cond => n _ _; exact: integral_ge0.
- apply: nearW => n; apply: lee_sum => m _; apply: le_abse_integral => //.
apply: measurable_funS mf => //; [exact: bigcup_measurable|].
exact: bigcup_sup.
Qed.

Lemma ( : (set _)^nat) ( : T -> \bar R) :
  trivIset setT F -> (forall , measurable (F k)) ->
  mu.-integrable (\bigcup_ F k) g ->
  (\int[mu]_( in \bigcup_ F i) g x = \sum_( <oo) \int[mu]_( in F i) g x)%E.

Proof.

move=> tF mF fi.
have ? : \int[mu]_( in \bigcup_ F i) g x \is a fin_num.
  rewrite fin_numElt -(lte_absl _ +oo).
  apply: le_lt_trans (integrableP _ _ _ fi).2; apply: le_abse_integral => //.
    exact: bigcupT_measurable.
  exact: measurable_int fi.
transitivity (\int[mu]_( in \bigcup_ F i) g^\+ x -
              \int[mu]_( in \bigcup_ F i) g^\- x)%E.
  rewrite -integralB.
  - exact: bigcupT_measurable.
  - by apply: integrable_funepos => //; exact: bigcupT_measurable.
  - by apply: integrable_funeneg => //; exact: bigcupT_measurable.
  - by apply: eq_integral => t Ft; rewrite -[in LHS](funeposBneg g).
transitivity (\sum_( <oo) (\int[mu]_( in F i) g^\+ x -
                            \int[mu]_( in F i) g^\- x)); last first.
  by apply: eq_eseriesr => // i; rewrite [RHS]integralE.
transitivity ((\sum_( <oo) \int[mu]_( in F i) g^\+ x) -
              (\sum_( <oo) \int[mu]_( in F i) g^\- x))%E.
  rewrite ge0_integral_bigcup//.
    by apply: measurable_funepos; case/integrableP : fi.
  rewrite ge0_integral_bigcup//.
  by apply: measurable_funeneg; case/integrableP : fi.
rewrite [X in X - _]nneseries_esum; first by move=> n _; exact: integral_ge0.
rewrite [X in _ - X]nneseries_esum; first by move=> n _; exact: integral_ge0.
rewrite set_true -esumB//=.
  - apply: integrable_summable => //; apply: integrable_funepos => //.
    exact: bigcup_measurable.
  - apply: integrable_summable => //; apply: integrable_funeneg => //.
    exact: bigcup_measurable.
  - by move=> n _; exact: integral_ge0.
  - by move=> n _; exact: integral_ge0.
rewrite summable_eseries.
  under [X in summable _ X]eq_fun do rewrite -integralE.
  by rewrite fun_true; exact: integrable_summable.
by congr (_ - _)%E; rewrite nneseries_esum// set_true.
Qed.

End subadditive_countable.

Section sequence_of_measures.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType).
Variable : {measure set T -> \bar R}^nat.
Let := mseries m_ O.

Lemma ( : set T) ( : measurable D) ( : T -> \bar R) :
  (forall , integrable (m_ n) D f) ->
  measurable_fun D f ->
  \sum_( <oo) `|\int[m_ n]_( in D) f^\- x | < +oo%E ->
  \sum_( <oo) `|\int[m_ n]_( in D) f^\+ x | < +oo%E ->
  \int[m]_( in D) f x = \sum_( <oo) \int[m_ n]_( in D) f x.

Proof.

move=> fi mf fmoo fpoo; rewrite integralE.
rewrite ge0_integral_measure_series//; first exact/measurable_funepos.
rewrite ge0_integral_measure_series//; first exact/measurable_funeneg.
transitivity (\sum_( <oo) (fine (\int[m_ n]_( in D) f^\+ x)%E)%:E -
              \sum_( <oo) (fine (\int[m_ n]_( in D) f^\- x))%:E).
  by congr (_ - _); apply: eq_eseriesr => n _; rewrite fineK//;
    [exact: integrable_pos_fin_num|exact: integrable_neg_fin_num].
have fineKn : \sum_( <oo) `|\int[m_ n]_( in D) f^\- x| =
          \sum_( <oo) `|(fine (\int[m_ n]_( in D) f^\- x))%:E|.
  apply: eq_eseriesr => n _; congr abse; rewrite fineK//.
  exact: integrable_neg_fin_num.
have fineKp : \sum_( <oo) `|\int[m_ n]_( in D) f^\+ x| =
          \sum_( <oo) `|(fine (\int[m_ n]_( in D) f^\+ x))%:E|.
  apply: eq_eseriesr => n _; congr abse; rewrite fineK//.
  exact: integrable_pos_fin_num.
rewrite nneseries_esum; first by move=> n _; exact/fine_ge0/integral_ge0.
rewrite nneseries_esum; first by move=> n _; exact/fine_ge0/integral_ge0.
rewrite -esumB//.
  - by rewrite /= /summable -nneseries_esum// -fineKp.
  - by rewrite /summable /= -nneseries_esum// -fineKn; exact: fmoo.
  - by move=> n _; exact/fine_ge0/integral_ge0.
  - by move=> n _; exact/fine_ge0/integral_ge0.
rewrite -summable_eseries_esum.
  apply: (@le_lt_trans _ _ (\esum_( in (fun=> true))
     `|(fine (\int[m_ i]_( in D) f x))%:E|)).
    do 2 rewrite ge0_esum//.
    by apply: PosEsum.le_pos_esum => k _; rewrite -EFinB -fineB// -?integralE//;
      [exact: integrable_pos_fin_num|exact: integrable_neg_fin_num].
  rewrite -nneseries_esum; first by [].
  apply: (@le_lt_trans _ _
      (\sum_( <oo) `|(fine (\int[m_ n]_( in D) f^\+ x))%:E| +
       \sum_( <oo) `|(fine (\int[m_ n]_( in D) f^\- x))%:E|)).
    rewrite -nneseriesD//; apply: lee_nneseries => // n _.
    rewrite integralE fineB// ?EFinB.
    - exact: integrable_pos_fin_num.
    - exact: integrable_neg_fin_num.
    - exact: (le_trans (lee_abs_sub _ _)).
  apply: lte_add_pinfty; first by rewrite -fineKp.
  by rewrite -fineKn; exact: fmoo.
by apply: eq_eseriesr => k _; rewrite !fineK// -?integralE//;
  [exact: integrable_pos_fin_num|exact: integrable_neg_fin_num].
Qed.

End sequence_of_measures.

Section integral_counting.
Local Open Scope ereal_scope.
Variable : realType.

Lemma ( : nat -> \bar R) : summable setT a ->
\int[counting]_ (a t) = \sum_( <oo) (a k).

Proof.

move=> sa.
transitivity (\int[mseries (fun => \d_ n) O]_ a t).
  congr (integral _ _ _); apply/funext => A.
  by rewrite /= counting_dirac.
rewrite (@integral_measure_series _ _ R (fun => \d_ n) setT)//=.
- move=> n; apply/integrableP; split=> [//|].
  by rewrite integral_dirac//= diracT mul1e (summable_pinfty sa).
- by apply: summable_integral_dirac => //; exact: summable_funeneg.
- by apply: summable_integral_dirac => //; exact: summable_funepos.
- by apply: eq_eseriesr=> i _; rewrite integral_dirac//= diracT mul1e.
Qed.

End integral_counting.

Section integral_ae_eq.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType) ( : {measure set T -> \bar R}).

Let ( : set T) ( : measurable D) ( : T -> \bar R) :
  mu.-integrable D f -> mu.-integrable D g ->
  (forall , E `<=` D -> measurable E ->
    \int[mu]_( in E) f x = \int[mu]_( in E) g x) ->
  mu (D `&` [set | g x < f x]) = 0.

Proof.

move=> itf itg fg; pose E := D `&` [set | f x - g x >= j.+1%:R^-1%:E].
have msf := measurable_int _ itf.
have msg := measurable_int _ itg.
have mE j : measurable (E j).
  rewrite /E; apply: measurable_lee => //.
  by apply/(emeasurable_funD msf)/measurableT_comp => //; case: mg.
have muE j : mu (E j) = 0.
  apply/eqP; rewrite -measure_le0.
  have fg0 : \int[mu]_( in E j) (f \- g) x = 0.
    rewrite integralB//.
    - by apply: integrableS itf => //; exact: subIsetl.
    - by apply: integrableS itg => //; exact: subIsetl.
    rewrite fg//; first apply: subIsetl.
    rewrite subee// fin_num_abs (le_lt_trans (le_abse_integral _ _ _))//.
      by apply: measurable_funS msg => //; first exact: subIsetl.
    apply: le_lt_trans (integrableP _ _ _ itg).2.
    apply: ge0_subset_integral => //; first exact: measurableT_comp msg.
    exact: subIsetl.
  suff : mu (E j) <= j.+1%:R%:E * \int[mu]_( in E j) (f \- g) x.
    by rewrite fg0 mule0.
  apply: (@le_trans _ _ (j.+1%:R%:E * \int[mu]_( in E j) j.+1%:R^-1%:E)).
    by rewrite integral_cst// muleA -EFinM divff// mul1e.
  rewrite lee_pmul//; first exact: integral_ge0.
  apply: ge0_le_integral => //; last by move=> x [].
  apply: emeasurable_funB.
  - by apply: measurable_funS msf => //; exact: subIsetl.
  - by apply: measurable_funS msg => //; exact: subIsetl.
have nd_E : {homo E : / (n0 <= m)%N >-> (n0 <= m)%O}.
  move=> i j ij; apply/subsetPset => x [Dx /= ifg]; split => //.
  by move: ifg; apply: le_trans; rewrite lee_fin lef_pV2// ?posrE// ler_nat.
rewrite set_lte_bigcup.
have /cvg_lim h1 : (mu \o E) x @[ --> \oo]--> 0.
  by apply: cvg_near_cst; exact: nearW.
have := @nondecreasing_cvg_measure _ _ _ mu E mE (bigcupT_measurable E mE) nd_E.
by move/cvg_lim => h2; rewrite setI_bigcupr -h2// h1.
Qed.

Lemma ( : set T) ( : measurable D) ( : T -> \bar R) :
  mu.-integrable D f -> measurable_fun D g ->
  (forall , E `<=` D -> measurable E ->
    \int[mu]_( in E) f x = \int[mu]_( in E) g x) ->
  ae_eq mu D f g.

Proof.

move=> fi mg fg; have mf := measurable_int _ fi; have gi : mu.-integrable D g.
  apply/integrableP; split => //; apply/abse_integralP => //; rewrite -fg//.
  by apply/abse_integralP => //; case/integrableP : fi.
have mugf : mu (D `&` [set | g x < f x]) = 0 by apply: integral_measure_lt.
have mufg : mu (D `&` [set | f x < g x]) = 0.
  by apply: integral_measure_lt => // E ED mE; rewrite fg.
have h : ~` [set | D x -> f x = g x] = D `&` [set | f x != g x].
  apply/seteqP; split => [x/= /not_implyP[? /eqP]//|x/= [Dx fgx]].
  by apply/not_implyP; split => //; exact/eqP.
apply/negligibleP; first by rewrite h; apply: measurable_neqe.
rewrite h set_neq_lt setIUr measureU//; [exact: measurable_lte..| |].
- apply/seteqP; split => [x [[Dx/= + [_]]]|//].
  by move=> /lt_trans => /[apply]; rewrite ltxx.
- by rewrite [X in X + _]mufg add0e [LHS]mugf.
Qed.

End integral_ae_eq.

Files

Module mathcomp.analysis.lebesgue_integral_theory.lebesgue_integrable