Module mathcomp.analysis.lebesgue_integral

From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop .
Require Import signed reals ereal topology normedtype sequences real_interval.
Require Import esum measure lebesgue_measure numfun.


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

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Reserved Notation "\int [ mu ]_ ( i 'in' D ) F"
  (at level 36, F at level 36, mu at level 10, i, D at level 50,
  format "'[' \int [ mu ]_ ( i 'in' D ) '/ ' F ']'").
Reserved Notation "\int [ mu ]_ i F"
  (at level 36, F at level 36, mu at level 10, i at level 0,
    right associativity, format "'[' \int [ mu ]_ i '/ ' F ']'").
Reserved Notation "mu .-integrable" (at level 2, format "mu .-integrable").
Reserved Notation "m1 '\x' m2" (at level 40, m2 at next level).
Reserved Notation "m1 '\x^' m2" (at level 40, m2 at next level).

#[global]
Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core.

HB.mixin Record isMeasurableFun d (aT : measurableType d) (rT : realType)
    (f : aT -> rT) := {
  measurable_funP : measurable_fun setT f
}.
HB.structure Definition MeasurableFun d aT rT :=
  {f of @isMeasurableFun d aT rT f}.


Reserved Notation "{ 'mfun' aT >-> T }"
  (at level 0, format "{ 'mfun' aT >-> T }").
Reserved Notation "[ 'mfun' 'of' f ]"
  (at level 0, format "[ 'mfun' 'of' f ]").
Notation "{ 'mfun' aT >-> T }" := (@MeasurableFun.type _ aT T) : form_scope.
Notation "[ 'mfun' 'of' f ]" := [the {mfun _ >-> _} of f] : form_scope.
#[global] Hint Resolve measurable_funP : core.

HB.structure Definition SimpleFun d (aT : measurableType d) (rT : realType) :=
  {f of @isMeasurableFun d aT rT f & @FiniteImage aT rT f}.
Reserved Notation "{ 'sfun' aT >-> T }"
  (at level 0, format "{ 'sfun' aT >-> T }").
Reserved Notation "[ 'sfun' 'of' f ]"
  (at level 0, format "[ 'sfun' 'of' f ]").
Notation "{ 'sfun' aT >-> T }" := (@SimpleFun.type _ aT T) : form_scope.
Notation "[ 'sfun' 'of' f ]" := [the {sfun _ >-> _} of f] : form_scope.

Lemma measurable_sfunP {d} {aT : measurableType d} {rT : realType}
  (f : {mfun aT >-> rT}) (Y : set rT) : measurable Y -> measurable (f @^-1` Y).


HB.mixin Record isNonNegFun (aT : Type) (rT : numDomainType) (f : aT -> rT) := {
  fun_ge0 : forall x, 0 <= f x
}.
HB.structure Definition NonNegFun aT rT := {f of @isNonNegFun aT rT f}.
Reserved Notation "{ 'nnfun' aT >-> T }"
  (at level 0, format "{ 'nnfun' aT >-> T }").
Reserved Notation "[ 'nnfun' 'of' f ]"
  (at level 0, format "[ 'nnfun' 'of' f ]").
Notation "{ 'nnfun' aT >-> T }" := (@NonNegFun.type aT T) : form_scope.
Notation "[ 'nnfun' 'of' f ]" := [the {nnfun _ >-> _} of f] : form_scope.
#[global] Hint Extern 0 (is_true (0 <= _)) => solve [apply: fun_ge0] : core.


HB.structure Definition NonNegSimpleFun
    d (aT : measurableType d) (rT : realType) :=
  {f of @SimpleFun d _ _ f & @NonNegFun aT rT f}.
Reserved Notation "{ 'nnsfun' aT >-> T }"
  (at level 0, format "{ 'nnsfun' aT >-> T }").
Reserved Notation "[ 'nnsfun' 'of' f ]"
  (at level 0, format "[ 'nnsfun' 'of' f ]").
Notation "{ 'nnsfun' aT >-> T }" := (@NonNegSimpleFun.type _ aT%type T) : form_scope.
Notation "[ 'nnsfun' 'of' f ]" := [the {nnsfun _ >-> _} of f] : form_scope.

Section ring.
Context (aT : pointedType) (rT : ringType).

Lemma fimfun_mulr_closed : mulr_closed (@fimfun aT rT).
HB.instance Definition _ := GRing.isMulClosed.Build _ fimfun fimfun_mulr_closed.
HB.instance Definition _ := [SubZmodule_isSubRing of {fimfun aT >-> rT} by <:].

Implicit Types (f g : {fimfun aT >-> rT}).

Lemma fimfunM f g : f * g = f \* g :> (_ -> _)
Lemma fimfun1 : (1 : {fimfun aT >-> rT}) = cst 1 :> (_ -> _)
Lemma fimfun_prod I r (P : {pred I}) (f : I -> {fimfun aT >-> rT}) (x : aT) :
  (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x.
Lemma fimfunX f n : f ^+ n = (fun x => f x ^+ n) :> (_ -> _).

Lemma indic_fimfun_subproof X : @FiniteImage aT rT \1_X.
HB.instance Definition _ X := indic_fimfun_subproof X.
Definition indic_fimfun (X : set aT) := [the {fimfun aT >-> rT} of \1_X].

HB.instance Definition _ k f := FImFun.copy (k \o* f) (f * cst_fimfun k).
Definition scale_fimfun k f := [the {fimfun aT >-> rT} of k \o* f].

End ring.
Arguments indic_fimfun {aT rT} _.

Section comring.
Context (aT : pointedType) (rT : comRingType).
HB.instance Definition _ := [SubRing_isSubComRing of {fimfun aT >-> rT} by <:].

Implicit Types (f g : {fimfun aT >-> rT}).
HB.instance Definition _ f g := FImFun.copy (f \* g) (f * g).
End comring.

Lemma fimfunE T (R : ringType) (f : {fimfun T >-> R}) x :
  f x = \sum_(y \in range f) (y * \1_(f @^-1` [set y]) x).

Lemma fimfunEord T (R : ringType) (f : {fimfun T >-> R})
    (s := fset_set (f @` setT)) :
  forall x, f x = \sum_(i < #|`s|) (s`_i * \1_(f @^-1` [set s`_i]) x).

Lemma trivIset_preimage1 {aT rT} D (f : aT -> rT) :
  trivIset D (fun x => f @^-1` [set x]).

Lemma trivIset_preimage1_in {aT} {rT : choiceType} (D : set rT) (A : set aT)
  (f : aT -> rT) : trivIset D (fun x => A `&` f @^-1` [set x]).

Section fimfun_bin.
Variables (d : measure_display) (T : measurableType d).
Variables (R : numDomainType) (f g : {fimfun T >-> R}).

Lemma max_fimfun_subproof : @FiniteImage T R (f \max g).
HB.instance Definition _ := max_fimfun_subproof.

End fimfun_bin.

HB.factory Record FiniteDecomp (T : pointedType) (R : ringType) (f : T -> R) :=
  { fimfunE : exists (r : seq R) (A_ : R -> set T),
      forall x, f x = \sum_(y <- r) (y * \1_(A_ y) x) }.
HB.builders Context T R f of @FiniteDecomp T R f.
  Lemma finite_subproof: @FiniteImage T R f.
  HB.instance Definition _ := finite_subproof.
HB.end.

Section mfun_pred.
Context {d} {aT : measurableType d} {rT : realType}.
Definition mfun : {pred aT -> rT} := mem [set f | measurable_fun setT f].
Definition mfun_key : pred_key mfun
Canonical mfun_keyed := KeyedPred mfun_key.
End mfun_pred.

Section mfun.
Context {d} {aT : measurableType d} {rT : realType}.
Notation T := {mfun aT >-> rT}.
Notation mfun := (@mfun _ aT rT).
Section Sub.
Context (f : aT -> rT) (fP : f \in mfun).
Definition mfun_Sub_subproof := @isMeasurableFun.Build d aT rT f (set_mem fP).
#[local] HB.instance Definition _ := mfun_Sub_subproof.
Definition mfun_Sub := [mfun of f].
End Sub.

Lemma mfun_rect (K : T -> Type) :
  (forall f (Pf : f \in mfun), K (mfun_Sub Pf)) -> forall u : T, K u.

Lemma mfun_valP f (Pf : f \in mfun) : mfun_Sub Pf = f :> (_ -> _).

HB.instance Definition _ := isSub.Build _ _ T mfun_rect mfun_valP.

Lemma mfuneqP (f g : {mfun aT >-> rT}) : f = g <-> f =1 g.

HB.instance Definition _ := [Choice of {mfun aT >-> rT} by <:].

Lemma cst_mfun_subproof x : @isMeasurableFun d aT rT (cst x).
HB.instance Definition _ x := @cst_mfun_subproof x.
Definition cst_mfun x := [the {mfun aT >-> rT} of cst x].

Lemma mfun_cst x : @cst_mfun x =1 cst x

HB.instance Definition _ := @isMeasurableFun.Build _ _ rT
  (@normr rT rT) (@measurable_normr rT setT).

HB.instance Definition _ :=
  isMeasurableFun.Build _ _ _ (@expR rT) (@measurable_expR rT).

Lemma measurableT_comp_subproof (f : {mfun _ >-> rT}) (g : {mfun aT >-> rT}) :
  measurable_fun setT (f \o g).

HB.instance Definition _ (f : {mfun _ >-> rT}) (g : {mfun aT >-> rT}) :=
  isMeasurableFun.Build _ _ _ (f \o g) (measurableT_comp_subproof _ _).

End mfun.

Section ring.
Context d (aT : measurableType d) (rT : realType).

Lemma mfun_subring_closed : subring_closed (@mfun _ aT rT).
HB.instance Definition _ := GRing.isSubringClosed.Build _ mfun
  mfun_subring_closed.
HB.instance Definition _ := [SubChoice_isSubComRing of {mfun aT >-> rT} by <:].

Implicit Types (f g : {mfun aT >-> rT}).

Lemma mfun0 : (0 : {mfun aT >-> rT}) =1 cst 0 :> (_ -> _)
Lemma mfun1 : (1 : {mfun aT >-> rT}) =1 cst 1 :> (_ -> _)
Lemma mfunN f : - f = \- f :> (_ -> _)
Lemma mfunD f g : f + g = f \+ g :> (_ -> _)
Lemma mfunB f g : f - g = f \- g :> (_ -> _)
Lemma mfunM f g : f * g = f \* g :> (_ -> _)
Lemma mfun_sum I r (P : {pred I}) (f : I -> {mfun aT >-> rT}) (x : aT) :
  (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x.
Lemma mfun_prod I r (P : {pred I}) (f : I -> {mfun aT >-> rT}) (x : aT) :
  (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x.
Lemma mfunX f n : f ^+ n = (fun x => f x ^+ n) :> (_ -> _).

HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g).
HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f).
HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g).
HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g).

Definition mindic (D : set aT) of measurable D : aT -> rT := \1_D.
Lemma mindicE (D : set aT) (mD : measurable D) :
  mindic mD = (fun x => (x \in D)%:R).
HB.instance Definition _ (D : set aT) (mD : measurable D) :
   @FImFun aT rT (mindic mD) := FImFun.on (mindic mD).
Lemma indic_mfun_subproof (D : set aT) (mD : measurable D) :
  @isMeasurableFun d aT rT (mindic mD).
HB.instance Definition _ D mD := @indic_mfun_subproof D mD.

Definition indic_mfun (D : set aT) (mD : measurable D) :=
  [the {mfun aT >-> rT} of mindic mD].

HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_mfun k).
Definition scale_mfun k f := [the {mfun aT >-> rT} of k \o* f].

Lemma max_mfun_subproof f g : @isMeasurableFun d aT rT (f \max g).
HB.instance Definition _ f g := max_mfun_subproof f g.
Definition max_mfun f g := [the {mfun aT >-> _} of f \max g].

End ring.
Arguments indic_mfun {d aT rT} _.

Lemma measurable_indic d (T : measurableType d) (R : realType)
    (D A : set T) : measurable A ->
  measurable_fun D (\1_A : T -> R).
#[global] Hint Extern 0 (measurable_fun _ (\1__ : _ -> _)) =>
  (exact: measurable_indic ) : core.
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_indic` instead")]
Notation measurable_fun_indic := measurable_indic (only parsing).

Section sfun_pred.
Context {d} {aT : measurableType d} {rT : realType}.
Definition sfun : {pred _ -> _} := [predI @mfun _ aT rT & fimfun].
Definition sfun_key : pred_key sfun
Canonical sfun_keyed := KeyedPred sfun_key.
Lemma sub_sfun_mfun : {subset sfun <= mfun}
Lemma sub_sfun_fimfun : {subset sfun <= fimfun}
End sfun_pred.

Section sfun.
Context {d} {aT : measurableType d} {rT : realType}.
Notation T := {sfun aT >-> rT}.
Notation sfun := (@sfun _ aT rT).
Section Sub.
Context (f : aT -> rT) (fP : f \in sfun).
Definition sfun_Sub1_subproof :=
  @isMeasurableFun.Build d aT rT f (set_mem (sub_sfun_mfun fP)).
#[local] HB.instance Definition _ := sfun_Sub1_subproof.
Definition sfun_Sub2_subproof :=
  @FiniteImage.Build aT rT f (set_mem (sub_sfun_fimfun fP)).
#[local] HB.instance Definition _ := sfun_Sub2_subproof.
Definition sfun_Sub := [sfun of f].
End Sub.

Lemma sfun_rect (K : T -> Type) :
  (forall f (Pf : f \in sfun), K (sfun_Sub Pf)) -> forall u : T, K u.

Lemma sfun_valP f (Pf : f \in sfun) : sfun_Sub Pf = f :> (_ -> _).

HB.instance Definition _ := isSub.Build _ _ T sfun_rect sfun_valP.

Lemma sfuneqP (f g : {sfun aT >-> rT}) : f = g <-> f =1 g.

HB.instance Definition _ := [Choice of {sfun aT >-> rT} by <:].

Definition cst_sfun x := [the {sfun aT >-> rT} of cst x].

Lemma cst_sfunE x : @cst_sfun x =1 cst x

End sfun.

Lemma fctD (T : pointedType) (K : ringType) (f g : T -> K) : f + g = f \+ g.
Lemma fctN (T : pointedType) (K : ringType) (f : T -> K) : - f = \- f.
Lemma fctM (T : pointedType) (K : ringType) (f g : T -> K) : f * g = f \* g.
Lemma fctZ (T : pointedType) (K : ringType) (L : lmodType K) k (f : T -> L) :
   k *: f = k \*: f.
Arguments cst _ _ _ _ /.
Definition fctWE := (fctD, fctN, fctM, fctZ).

Section ring.
Context d (aT : measurableType d) (rT : realType).

Lemma sfun_subring_closed : subring_closed (@sfun d aT rT).

HB.instance Definition _ := GRing.isSubringClosed.Build _ sfun
  sfun_subring_closed.
HB.instance Definition _ := [SubChoice_isSubComRing of {sfun aT >-> rT} by <:].

Implicit Types (f g : {sfun aT >-> rT}).

Lemma sfun0 : (0 : {sfun aT >-> rT}) =1 cst 0
Lemma sfun1 : (1 : {sfun aT >-> rT}) =1 cst 1
Lemma sfunN f : - f =1 \- f
Lemma sfunD f g : f + g =1 f \+ g
Lemma sfunB f g : f - g =1 f \- g
Lemma sfunM f g : f * g =1 f \* g
Lemma sfun_sum I r (P : {pred I}) (f : I -> {sfun aT >-> rT}) (x : aT) :
  (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x.
Lemma sfun_prod I r (P : {pred I}) (f : I -> {sfun aT >-> rT}) (x : aT) :
  (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x.
Lemma sfunX f n : f ^+ n =1 (fun x => f x ^+ n).

HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g).
HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f).
HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g).
HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g).

Definition indic_sfun (D : set aT) (mD : measurable D) :=
  [the {sfun aT >-> rT} of mindic rT mD].

HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_sfun k).
Definition scale_sfun k f := [the {sfun aT >-> rT} of k \o* f].

HB.instance Definition _ f g := max_mfun_subproof f g.
Definition max_sfun f g := [the {sfun aT >-> _} of f \max g].

End ring.
Arguments indic_sfun {d aT rT} _.

Lemma fset_set_comp (T1 : Type) (T2 T3 : choiceType) (D : set T1)
    (f : {fimfun T1 >-> T2}) (g : T2 -> T3) :
  fset_set [set (g \o f) x | x in D] =
  [fset g x | x in fset_set [set f x | x in D]]%fset.

Lemma preimage_nnfun0 T (R : realDomainType) (f : {nnfun T >-> R}) t :
  t < 0 -> f @^-1` [set t] = set0.

Lemma preimage_cstM T (R : realFieldType) (x y : R) (f : T -> R) :
  x != 0 -> (cst x \* f) @^-1` [set y] = f @^-1` [set y / x].

Lemma preimage_add T (R : numDomainType) (f g : T -> R) z :
  (f \+ g) @^-1` [set z] = \bigcup_(a in f @` setT)
    ((f @^-1` [set a]) `&` (g @^-1` [set z - a])).

Section simple_bounded.
Context d (T : measurableType d) (R : realType).

Lemma simple_bounded (f : {sfun T >-> R}) : bounded_fun f.

End simple_bounded.

Section nnsfun_functions.
Context d (T : measurableType d) (R : realType).

Lemma cst_nnfun_subproof (x : {nonneg R}) : @isNonNegFun T R (cst x%:num).
HB.instance Definition _ x := @cst_nnfun_subproof x.

Definition cst_nnsfun (r : {nonneg R}) := [the {nnsfun T >-> R} of cst r%:num].

Definition nnsfun0 : {nnsfun T >-> R} := cst_nnsfun 0%R%:nng.

Lemma indic_nnfun_subproof (D : set T) : @isNonNegFun T R (\1_D).
HB.instance Definition _ D := @indic_nnfun_subproof D.

HB.instance Definition _ D (mD : measurable D) :
   @NonNegFun T R (mindic R mD) := NonNegFun.on (mindic R mD).

End nnsfun_functions.
Arguments nnsfun0 {d T R}.

Section nnfun_bin.
Variables (T : Type) (R : numDomainType) (f g : {nnfun T >-> R}).

Lemma add_nnfun_subproof : @isNonNegFun T R (f \+ g).
HB.instance Definition _ := add_nnfun_subproof.

Lemma mul_nnfun_subproof : @isNonNegFun T R (f \* g).
HB.instance Definition _ := mul_nnfun_subproof.

Lemma max_nnfun_subproof : @isNonNegFun T R (f \max g).
HB.instance Definition _ := max_nnfun_subproof.

End nnfun_bin.

Section nnsfun_bin.
Context d (T : measurableType d) (R : realType).
Variables f g : {nnsfun T >-> R}.

HB.instance Definition _ := MeasurableFun.on (f \+ g).
Definition add_nnsfun := [the {nnsfun T >-> R} of f \+ g].

HB.instance Definition _ := MeasurableFun.on (f \* g).
Definition mul_nnsfun := [the {nnsfun T >-> R} of f \* g].

HB.instance Definition _ := MeasurableFun.on (f \max g).
Definition max_nnsfun := [the {nnsfun T >-> R} of f \max g].

Definition indic_nnsfun A (mA : measurable A) := [the {nnsfun T >-> R} of mindic R mA].

End nnsfun_bin.
Arguments add_nnsfun {d T R} _ _.
Arguments mul_nnsfun {d T R} _ _.
Arguments max_nnsfun {d T R} _ _.

Section nnsfun_iter.
Context d (T : measurableType d) (R : realType) (D : set T).
Variable f : {nnsfun T >-> R}^nat.

Definition sum_nnsfun n := \big[add_nnsfun/nnsfun0]_(i < n) f i.

Lemma sum_nnsfunE n t : sum_nnsfun n t = \sum_(i < n) (f i t).

Definition bigmax_nnsfun n := \big[max_nnsfun/nnsfun0]_(i < n) f i.

Lemma bigmax_nnsfunE n t : bigmax_nnsfun n t = \big[maxr/0]_(i < n) (f i t).

End nnsfun_iter.

Section nnsfun_cover.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variable f : {nnsfun T >-> R}.

Lemma nnsfun_cover :
  \big[setU/set0]_(i \in range f) (f @^-1` [set i]) = setT.

Lemma nnsfun_coverT :
  \big[setU/set0]_(i \in [set: R]) (f @^-1` [set i]) = setT.

End nnsfun_cover.

#[global] Hint Extern 0 (measurable (_ @^-1` [set _])) =>
  solve [apply: measurable_sfunP; exact: measurable_set1] : core.

Lemma measurable_sfun_inP {d} {aT : measurableType d} {rT : realType}
   (f : {mfun aT >-> rT}) D (y : rT) :
  measurable D -> measurable (D `&` f @^-1` [set y]).

#[global] Hint Extern 0 (measurable (_ `&` _ @^-1` [set _])) =>
  solve [apply: measurable_sfun_inP; assumption] : core.

#[global] Hint Extern 0 (finite_set _) => solve [apply: fimfunP] : core.

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

Lemma measure_fsbig (I : choiceType) (A : set I) (F : I -> set T) :
  finite_set A ->
  (forall i, A i -> measurable (F i)) -> trivIset A F ->
  m (\big[setU/set0]_(i \in A) F i) = \sum_(i \in A) m (F i).

Lemma additive_nnsfunr (g f : {nnsfun T >-> R}) x :
  \sum_(i \in range g) m (f @^-1` [set x] `&` (g @^-1` [set i])) =
  m (f @^-1` [set x] `&` \big[setU/set0]_(i \in range g) (g @^-1` [set i])).

Lemma additive_nnsfunl (g f : {nnsfun T >-> R}) x :
  \sum_(i \in range g) m (g @^-1` [set i] `&` (f @^-1` [set x])) =
  m (\big[setU/set0]_(i \in range g) (g @^-1` [set i]) `&` f @^-1` [set x]).

End measure_fsbig.

Section mulem_ge0.
Local Open Scope ereal_scope.

Let mulef_ge0 (R : realDomainType) x (f : R -> \bar R) :
  0 <= f x -> ((x < 0)%R -> f x = 0) -> 0 <= x%:E * f x.

Lemma nnfun_muleindic_ge0 d (T : measurableType d) (R : realDomainType)
  (f : {nnfun T >-> R}) r z : 0 <= r%:E * (\1_(f @^-1` [set r]) z)%:E.

Lemma mulemu_ge0 d (T : measurableType d) (R : realType)
    (mu : {measure set T -> \bar R}) x (A : R -> set T) :
  ((x < 0)%R -> A x = set0) -> 0 <= x%:E * mu (A x).
Global Arguments mulemu_ge0 {d T R mu x} A.

Lemma nnsfun_mulemu_ge0 d (T : measurableType d) (R : realType)
    (mu : {measure set T -> \bar R}) (f : {nnsfun T >-> R}) x :
  0 <= x%:E * mu (f @^-1` [set x]).
End mulem_ge0.


Section simple_fun_raw_integral.
Local Open Scope ereal_scope.
Variables (T : Type) (R : numDomainType) (mu : set T -> \bar R) (f : T -> R).

Definition sintegral := \sum_(x \in [set: R]) x%:E * mu (f @^-1` [set x]).

Lemma sintegralET :
  sintegral = \sum_(x \in [set: R]) x%:E * mu (f @^-1` [set x]).

End simple_fun_raw_integral.

#[global] Hint Extern 0 (is_true (0 <= (_ : {measure set _ -> \bar _}) _)%E) =>
  solve [apply: measure_ge0] : core.

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

Lemma sintegralE f :
  sintegral mu f = \sum_(x \in range f) x%:E * mu (f @^-1` [set x]).

Lemma sintegral0 : sintegral mu (cst 0%R) = 0.

Lemma sintegral_ge0 (f : {nnsfun T >-> R}) : 0 <= sintegral mu f.

Lemma sintegral_indic (A : set T) : sintegral mu \1_A = mu A.

Lemma sintegralEnnsfun (f : {nnsfun T >-> R}) : sintegral mu f =
  (\sum_(x \in [set r | r > 0]%R) (x%:E * mu (f @^-1` [set x])))%E.

End sintegral_lemmas.

Lemma eq_sintegral d (T : measurableType d) (R : numDomainType)
     (mu : set T -> \bar R) g f :
   f =1 g -> sintegral mu f = sintegral mu g.
Arguments eq_sintegral {d T R mu} g.

Section sintegralrM.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (m : {measure set T -> \bar R}) (r : R) (f : {nnsfun T >-> R}).

Lemma sintegralrM : sintegral m (cst r \* f)%R = r%:E * sintegral m f.

End sintegralrM.

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

Lemma sintegralD : sintegral m (f \+ g)%R = sintegral m f + sintegral m g.

End sintegralD.

Section le_sintegral.
Context d (T : measurableType d) (R : realType) (m : {measure set T -> \bar R}).
Variables f g : {nnsfun T >-> R}.
Hypothesis fg : forall x, f x <= g x.

Let fgnn : @isNonNegFun T R (g \- f).
#[local] HB.instance Definition _ := fgnn.

Lemma le_sintegral : (sintegral m f <= sintegral m g)%E.

End le_sintegral.

Lemma is_cvg_sintegral d (T : measurableType d) (R : realType)
  (m : {measure set T -> \bar R}) (f : {nnsfun T >-> R}^nat) :
  (forall x, nondecreasing_seq (f ^~ x)) -> cvgn (sintegral m \o f).

Definition proj_nnsfun d (T : measurableType d) (R : realType)
    (f : {nnsfun T >-> R}) (A : set T) (mA : measurable A) :=
  mul_nnsfun f (indic_nnsfun R mA).

Definition mrestrict d (T : measurableType d) (R : realType) (f : {nnsfun T >-> R})
  A (mA : measurable A) : f \_ A = proj_nnsfun f mA.

Definition scale_nnsfun d (T : measurableType d) (R : realType)
    (f : {nnsfun T >-> R}) (k : R) (k0 : 0 <= k) :=
  mul_nnsfun (cst_nnsfun T (NngNum k0)) f.

Section sintegral_nondecreasing_limit_lemma.
Context d (T : measurableType d) (R : realType).
Variable mu : {measure set T -> \bar R}.
Variables (g : {nnsfun T >-> R}^nat) (f : {nnsfun T >-> R}).
Hypothesis nd_g : forall x, nondecreasing_seq (g^~ x).
Hypothesis gf : forall x, cvgn (g^~ x) -> f x <= limn (g^~ x).

Let fleg c : (set T)^nat := fun n => [set x | c * f x <= g n x].

Let nd_fleg c : {homo fleg c : n m / (n <= m)%N >-> (n <= m)%O}.

Let mfleg c n : measurable (fleg c n).

Let g1 c n : {nnsfun T >-> R} := proj_nnsfun f (mfleg c n).

Let le_ffleg c : {homo (fun p x => g1 c p x): m n / (m <= n)%N >-> (m <= n)%O}.

Let bigcup_fleg c : c < 1 -> \bigcup_n fleg c n = setT.

Local Open Scope ereal_scope.

Lemma nd_sintegral_lim_lemma : sintegral mu f <= limn (sintegral mu \o g).

End sintegral_nondecreasing_limit_lemma.

Section sintegral_nondecreasing_limit.
Context d (T : measurableType d) (R : realType).
Variable mu : {measure set T -> \bar R}.
Variables (g : {nnsfun T >-> R}^nat) (f : {nnsfun T >-> R}).
Hypothesis nd_g : forall x, nondecreasing_seq (g^~ x).
Hypothesis gf : forall x, g ^~ x @ \oo --> f x.

Let limg x : limn (g^~ x) = f x.

Lemma nd_sintegral_lim : sintegral mu f = limn (sintegral mu \o g).

End sintegral_nondecreasing_limit.

Section integral.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Implicit Types (f g : T -> \bar R) (D : set T).

Let nnintegral mu f := ereal_sup [set sintegral mu h |
  h in [set h : {nnsfun T >-> R} | forall x, (h x)%:E <= f x]].

Definition integral mu D f (g := f \_ D) :=
  nnintegral mu (g ^\+) - nnintegral mu (g ^\-).

Variable (mu : {measure set T -> \bar R}).

Let nnintegral_ge0 f : (forall x, 0 <= f x) -> 0 <= nnintegral mu f.

Let eq_nnintegral g f : f =1 g -> nnintegral mu f = nnintegral mu g.

Let nnintegral0 : nnintegral mu (cst 0) = 0.

Let nnintegral_nnsfun (h : {nnsfun T >-> R}) :
  nnintegral mu (EFin \o h) = sintegral mu h.

Local Notation "\int_ ( x 'in' D ) F" := (integral mu D (fun x => F))
  (at level 36, F at level 36, x, D at level 50,
  format "'[' \int_ ( x 'in' D ) '/ ' F ']'").

Lemma eq_integral D g f : {in D, f =1 g} ->
  \int_(x in D) f x = \int_(x in D) g x.

Lemma ge0_integralE D f : (forall x, D x -> 0 <= f x) ->
  \int_(x in D) f x = nnintegral mu (f \_ D).

Lemma ge0_integralTE f : (forall x, 0 <= f x) ->
  \int_(x in setT) f x = nnintegral mu f.

Lemma integralE D f :
  \int_(x in D) f x = \int_(x in D) (f ^\+ x) - \int_(x in D) f ^\- x.

Lemma integral0 D : \int_(x in D) (cst 0 x) = 0.

Lemma integral0_eq D f :
  (forall x, D x -> f x = 0) -> \int_(x in D) f x = 0.

Lemma integral_ge0 D f : (forall x, D x -> 0 <= f x) -> 0 <= \int_(x in D) f x.

Lemma integral_nnsfun D (mD : measurable D) (h : {nnsfun T >-> R}) :
  \int_(x in D) (h x)%:E = sintegral mu (h \_ D).

End integral.

Notation "\int [ mu ]_ ( x 'in' D ) f" :=
  (integral mu D (fun x => f)) : ereal_scope.
Notation "\int [ mu ]_ x f" :=
  ((integral mu setT (fun x => f)))%E : ereal_scope.
Arguments eq_integral {d T R mu D} g.

Section eq_measure_integral.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType) (D : set T).
Implicit Types m : {measure set T -> \bar R}.

Let eq_measure_integral0 m2 m1 (f : T -> \bar R) :
  (forall A, measurable A -> A `<=` D -> m1 A = m2 A) ->
  [set sintegral m1 h | h in
    [set h : {nnsfun T >-> R} | (forall x, (h x)%:E <= (f \_ D) x)]] `<=`
  [set sintegral m2 h | h in
    [set h : {nnsfun T >-> R} | (forall x, (h x)%:E <= (f \_ D) x)]].

Lemma eq_measure_integral m2 m1 (f : T -> \bar R) :
    (forall A, measurable A -> A `<=` D -> m1 A = m2 A) ->
  \int[m1]_(x in D) f x = \int[m2]_(x in D) f x.

End eq_measure_integral.
Arguments eq_measure_integral {d T R D} m2 {m1 f}.

Section integral_measure_zero.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).

Let sintegral_measure_zero (f : T -> R) : sintegral mzero f = 0.

Lemma integral_measure_zero (D : set T) (f : T -> \bar R) :
  \int[mzero]_(x in D) f x = 0.

End integral_measure_zero.

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

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

Lemma integralT_nnsfun (h : {nnsfun T >-> R}) :
  \int[mu]_x (h x)%:E = sintegral mu h.

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

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

End domain_change.
Arguments integral_mkcond {d T R mu} D f.

Section nondecreasing_integral_limit.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (mu : {measure set T -> \bar R}) (f : T -> \bar R)
          (g : {nnsfun T >-> R}^nat).
Hypothesis f0 : forall x, 0 <= f x.
Hypothesis mf : measurable_fun setT f.
Hypothesis nd_g : forall x, nondecreasing_seq (g^~x).
Hypothesis gf : forall x, EFin \o g^~ x @ \oo --> f x.
Local Open Scope ereal_scope.

Lemma nd_ge0_integral_lim : \int[mu]_x f x = limn (sintegral mu \o g).

End nondecreasing_integral_limit.

Section dyadic_interval.
Variable R : realType.

Definition dyadic_itv n k : interval R :=
  `[(k%:R * 2 ^- n), (k.+1%:R * 2 ^- n)[.

Local Notation I := dyadic_itv.

Lemma dyadic_itv_subU n k : [set` I n k] `<=`
  [set` I n.+1 k.*2] `|` [set` I n.+1 k.*2.+1].

Lemma bigsetU_dyadic_itv n : `[n%:R, n.+1%:R[%classic =
  \big[setU/set0]_(n * 2 ^ n.+1 <= k < n.+1 * 2 ^ n.+1) [set` I n.+1 k].

Lemma dyadic_itv_image n T (f : T -> \bar R) x :
  (n%:R%:E <= f x < n.+1%:R%:E)%E ->
  exists k, (2 ^ n.+1 * n <= k < 2 ^ n.+1 * n.+1)%N /\
    f x \in EFin @` [set` I n.+1 k].

End dyadic_interval.

Section approximation.
Context d (T : measurableType d) (R : realType).
Variables (D : set T) (mD : measurable D).
Variables (f : T -> \bar R) (mf : measurable_fun D f).

Local Notation I := (@dyadic_itv R).

Let A n k := if (k < n * 2 ^ n)%N then
  D `&` [set x | f x \in EFin @` [set` I n k]] else set0.

Let B n := D `&` [set x | n%:R%:E <= f x]%E.

Definition approx : (T -> R)^nat := fun n x =>
  \sum_(k < n * 2 ^ n) k%:R * 2 ^- n * \1_(A n k) x + n%:R * \1_(B n) x.

Let mA n k : measurable (A n k).

Let trivIsetA n : trivIset setT (A n).

Let f0_A0 n (i : 'I_(n * 2 ^ n)) x : f x = 0%:E -> i != O :> nat ->
  \1_(A n i) x = 0 :> R.

Let fgen_A0 n x (i : 'I_(n * 2 ^ n)) : (n%:R%:E <= f x)%E ->
  \1_(A n i) x = 0 :> R.

Let disj_A0 x n (i k : 'I_(n * 2 ^ n)) : i != k -> x \in A n k ->
  \1_(A n i) x = 0 :> R.
Arguments disj_A0 {x n i} k.

Let mB n : measurable (B n)

Let foo_B1 x n : D x -> f x = +oo%E -> \1_(B n) x = 1 :> R.

Let f0_B0 x n : f x = 0%:E -> n != 0%N -> \1_(B n) x = 0 :> R.

Let fgtn_B0 x n : (f x < n%:R%:E)%E -> \1_(B n) x = 0 :> R.

Let f0_approx0 n x : f x = 0%E -> approx n x = 0.

Let fpos_approx_neq0 x : D x -> (0%E < f x < +oo)%E ->
  \forall n \near \oo, approx n x != 0.

Let f_ub_approx n x : (f x < n%:R%:E)%E ->
  approx n x == 0 \/ exists k,
    [/\ (0 < k < n * 2 ^ n)%N,
       x \in A n k, approx n x = k%:R / 2 ^+ n &
       f x \in EFin @` [set` I n k]].

Let notinD_approx0 x n : ~ D x -> approx n x = 0 :> R.

Lemma nd_approx : nondecreasing_seq approx.

Lemma cvg_approx x (f0 : forall x, D x -> (0 <= f x)%E) : D x ->
  (f x < +oo)%E -> approx^~ x @ \oo --> fine (f x).

Lemma le_approx k x (f0 : forall x, D x -> (0 <= f x)%E) : D x ->
  ((approx k x)%:E <= f x)%E.

Lemma dvg_approx x : D x -> f x = +oo%E -> ~ cvgn (approx^~ x : _ -> R^o).

Lemma ecvg_approx (f0 : forall x, D x -> (0 <= f x)%E) x :
  D x -> EFin \o approx^~x @ \oo --> f x.

Let k2n_ge0 n (k : 'I_(n * 2 ^ n)) : 0 <= k%:R * 2 ^- n :> R.

Definition nnsfun_approx : {nnsfun T >-> R}^nat := fun n => locked (add_nnsfun
  (sum_nnsfun
    (fun k => match Bool.bool_dec (k < (n * 2 ^ n))%N true with
      | left h => scale_nnsfun (indic_nnsfun _ (mA n k)) (k2n_ge0 (Ordinal h))
      | right _ => nnsfun0
     end) (n * 2 ^ n)%N)
  (scale_nnsfun (indic_nnsfun _ (mB n)) (ler0n _ n))).

Lemma nnsfun_approxE n : nnsfun_approx n = approx n :> (T -> R).

Lemma cvg_nnsfun_approx (f0 : forall x, D x -> (0 <= f x)%E) x :
  D x -> EFin \o nnsfun_approx^~x @ \oo --> f x.

Lemma nd_nnsfun_approx : nondecreasing_seq (nnsfun_approx : (T -> R)^nat).

Lemma approximation : (forall t, D t -> (0 <= f t)%E) ->
  exists g : {nnsfun T >-> R}^nat, nondecreasing_seq (g : (T -> R)^nat) /\
                        (forall x, D x -> EFin \o g^~ x @ \oo --> f x).

End approximation.


Section semi_linearity0.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
Variables f1 f2 : T -> \bar R.
Hypothesis f10 : forall x, D x -> 0 <= f1 x.
Hypothesis mf1 : measurable_fun D f1.

Lemma ge0_integralZl_EFin k : (0 <= k)%R ->
  \int[mu]_(x in D) (k%:E * f1 x) = k%:E * \int[mu]_(x in D) f1 x.

End semi_linearity0.
#[deprecated(since="mathcomp-analysis 0.6.4", note="use `ge0_integralZl_EFin` instead")]
Notation ge0_integralM_EFin := ge0_integralZl_EFin (only parsing).

Section semi_linearity.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variable mu : {measure set T -> \bar R}.
Variables (D : set T) (mD : measurable D) (f1 f2 : T -> \bar R).
Hypothesis f10 : forall x, D x -> 0 <= f1 x.
Hypothesis mf1 : measurable_fun D f1.
Hypothesis f20 : forall x, D x -> 0 <= f2 x.
Hypothesis mf2 : measurable_fun D f2.

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

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

End semi_linearity.

Section approximation_sfun.
Context d (T : measurableType d) (R : realType) (f : T -> \bar R).
Variables (D : set T) (mD : measurable D) (mf : measurable_fun D f).

Lemma approximation_sfun :
  exists g : {sfun T >-> R}^nat, (forall x, D x -> EFin \o g^~ x @ \oo --> f x).

End approximation_sfun.

Section lusin.
Hint Extern 0 (hausdorff_space _) => (exact: Rhausdorff ) : core.
Local Open Scope ereal_scope.
Context (rT : realType) (A : set rT).
Let mu := [the measure _ _ of @lebesgue_measure rT].
Let R := [the measurableType _ of measurableTypeR rT].
Hypothesis mA : measurable A.
Hypothesis finA : mu A < +oo.

Let lusin_simple (f : {sfun R >-> rT}) (eps : rT) : (0 < eps)%R ->
  exists K, [/\ compact K, K `<=` A, mu (A `\` K) < eps%:E &
  {within K, continuous f}].

Let measurable_almost_continuous' (f : R -> R) (eps : rT) :
  (0 < eps)%R -> measurable_fun A f -> exists K,
  [/\ measurable K, K `<=` A, mu (A `\` K) < eps%:E &
  {within K, continuous f}].

Lemma measurable_almost_continuous (f : R -> R) (eps : rT) :
  (0 < eps)%R -> measurable_fun A f -> exists K,
  [/\ compact K, K `<=` A, mu (A `\` K) < eps%:E &
  {within K, continuous f}].

End lusin.

Section emeasurable_fun.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Implicit Types (D : set T) (f g : T -> \bar R).

Lemma emeasurable_funD D f g :
  measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \+ g).

Lemma emeasurable_fun_sum D I s (h : I -> (T -> \bar R)) :
  (forall n, measurable_fun D (h n)) ->
  measurable_fun D (fun x => \sum_(i <- s) h i x).

Lemma emeasurable_fun_fsum D (I : choiceType) (A : set I)
    (h : I -> (T -> \bar R)) : finite_set A ->
    (forall n, measurable_fun D (h n)) ->
  measurable_fun D (fun x => \sum_(i \in A) h i x).

Lemma ge0_emeasurable_fun_sum D (h : nat -> (T -> \bar R)) :
  (forall k x, 0 <= h k x) -> (forall k, measurable_fun D (h k)) ->
  measurable_fun D (fun x => \sum_(i <oo) h i x).

Lemma emeasurable_funB D f g :
  measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \- g).

Lemma emeasurable_funM D f g :
  measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \* g).

Lemma measurable_funeM D (f : T -> \bar R) (k : \bar R) :
  measurable_fun D f -> measurable_fun D (fun x => k * f x)%E.

End emeasurable_fun.

Section measurable_fun_measurable2.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (D : set T) (mD : measurable D).
Implicit Types f g : T -> \bar R.

Lemma emeasurable_fun_lt f g : measurable_fun D f -> measurable_fun D g ->
  measurable (D `&` [set x | f x < g x]).

Lemma emeasurable_fun_le f g : measurable_fun D f -> measurable_fun D g ->
  measurable (D `&` [set x | f x <= g x]).

Lemma emeasurable_fun_eq f g : measurable_fun D f -> measurable_fun D g ->
  measurable (D `&` [set x | f x = g x]).

Lemma emeasurable_fun_neq f g : measurable_fun D f -> measurable_fun D g ->
  measurable (D `&` [set x | f x != g x]).

End measurable_fun_measurable2.

Section ge0_integral_sum.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
Variables (I : Type) (f : I -> (T -> \bar R)).
Hypothesis mf : forall n, measurable_fun D (f n).
Hypothesis f0 : forall n x, D x -> 0 <= f n x.

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

End ge0_integral_sum.

Section ge0_integral_fsum.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
Variables (I : choiceType) (f : I -> (T -> \bar R)).
Hypothesis mf : forall n, measurable_fun D (f n).
Hypothesis f0 : forall n x, D x -> 0 <= f n x.

Lemma ge0_integral_fsum (A : set I) : finite_set A ->
  \int[mu]_(x in D) (\sum_(k \in A) f k x) =
  \sum_(k \in A) \int[mu]_(x in D) f k x.

End ge0_integral_fsum.

Section monotone_convergence_theorem.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variable mu : {measure set T -> \bar R}.
Variables (D : set T) (mD : measurable D) (g' : (T -> \bar R)^nat).
Hypothesis mg' : forall n, measurable_fun D (g' n).
Hypothesis g'0 : forall n x, D x -> 0 <= g' n x.
Hypothesis nd_g' : forall x, D x -> nondecreasing_seq (g'^~ x).
Let f' := fun x => limn (g'^~ x).

Let g n := (g' n \_ D).

Let g0 n x : 0 <= g n x

Let mg n : measurable_fun setT (g n).

Let nd_g x : nondecreasing_seq (g^~ x).

Let f := fun x => limn (g^~ x).

Let is_cvg_g t : cvgn (g^~ t).

Local Definition g2' n : (T -> R)^nat := approx setT (g n).
Local Definition g2 n : {nnsfun T >-> R}^nat := nnsfun_approx measurableT (mg n).

Local Definition max_g2' : (T -> R)^nat :=
  fun k t => (\big[maxr/0]_(i < k) (g2' i k) t)%R.
Local Definition max_g2 : {nnsfun T >-> R}^nat :=
  fun k => bigmax_nnsfun (g2^~ k) k.

Let is_cvg_g2 n t : cvgn (EFin \o (g2 n ^~ t)).

Let nd_max_g2 : nondecreasing_seq (max_g2 : (T -> R)^nat).

Let is_cvg_max_g2 t : cvgn (EFin \o max_g2 ^~ t).

Let max_g2_g k x : ((max_g2 k x)%:E <= g k x)%O.

Let lim_max_g2_f t : limn (EFin \o max_g2 ^~ t) <= f t.

Let lim_g2_max_g2 t n : limn (EFin \o g2 n ^~ t) <= limn (EFin \o max_g2 ^~ t).

Let cvg_max_g2_f t : EFin \o max_g2 ^~ t @ \oo --> f t.

Lemma monotone_convergence :
  \int[mu]_(x in D) (f' x) = limn (fun n => \int[mu]_(x in D) (g' n x)).

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

End monotone_convergence_theorem.

Section integral_nneseries.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
Variable f : (T -> \bar R)^nat.
Hypothesis mf : forall n, measurable_fun D (f n).
Hypothesis f0 : forall n x, D x -> 0 <= f n x.

Lemma integral_nneseries : \int[mu]_(x in D) (\sum_(n <oo) f n x) =
                           \sum_(n <oo) (\int[mu]_(x in D) (f n x)).

End integral_nneseries.

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

Lemma ge0_integralZl (k : \bar R) : (forall x, D x -> 0 <= f x) ->
  0 <= k -> \int[mu]_(x in D) (k * f x)%E = k * \int[mu]_(x in D) (f x).

End ge0_integralZl.
#[deprecated(since="mathcomp-analysis 0.6.4", note="use `ge0_integralZl` instead")]
Notation ge0_integralM := ge0_integralZl (only parsing).

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

Lemma integral_indic (E : set T) : measurable E ->
  \int[mu]_(x in D) (\1_E x)%:E = mu (E `&` D).

End integral_indic.

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

Lemma integralZl_indic (f : R -> set T) (k : R) :
    ((k < 0)%R -> f k = set0) -> measurable (f k) ->
  \int[m]_(x in D) (k * \1_(f k) x)%:E =
  k%:E * \int[m]_(x in D) (\1_(f k) x)%:E.

Lemma integralZl_indic_nnsfun (f : {nnsfun T >-> R}) (k : R) :
  \int[m]_(x in D) (k * \1_(f @^-1` [set k]) x)%:E =
  k%:E * \int[m]_(x in D) (\1_(f @^-1` [set k]) x)%:E.

End integralZl_indic.
Arguments integralZl_indic {d T R m D} mD f.
#[deprecated(since="mathcomp-analysis 0.6.4", note="use `integralZl_indic` instead")]
Notation integralM_indic := integralZl_indic (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.4", note="use `integralZl_indic_nnsfun` instead")]
Notation integralM_indic_nnsfun := integralZl_indic_nnsfun (only parsing).

Section integral_mscale.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (m : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
Variables (k : {nonneg R}) (f : T -> \bar R).

Let integral_mscale_indic E : measurable E ->
  \int[mscale k m]_(x in D) (\1_E x)%:E =
  k%:num%:E * \int[m]_(x in D) (\1_E x)%:E.

Let integral_mscale_nnsfun (h : {nnsfun T >-> R}) :
  \int[mscale k m]_(x in D) (h x)%:E = k%:num%:E * \int[m]_(x in D) (h x)%:E.

Lemma ge0_integral_mscale (mf : measurable_fun D f) :
    (forall x, D x -> 0 <= f x) ->
  \int[mscale k m]_(x in D) f x = k%:num%:E * \int[m]_(x in D) f x.

End integral_mscale.

Section fatou.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
Variable (f : (T -> \bar R)^nat).
Hypothesis mf : forall n, measurable_fun D (f n).
Hypothesis f0 : forall n x, D x -> 0 <= f n x.

Lemma fatou : \int[mu]_(x in D) limn_einf (f^~ x) <=
              limn_einf (fun n => \int[mu]_(x in D) f n x).

End fatou.

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

Lemma integralN D (f : T -> \bar R) :
  \int[mu]_(x in D) f^\+ x +? (- \int[mu]_(x in D) f^\- x) ->
  \int[mu]_(x in D) - f x = - \int[mu]_(x in D) f x.

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

End integralN.

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

Lemma sintegral_EFin_cst (x : {nonneg R}) :
  sintegral mu (cst x%:num \_ D) = x%:num%:E * mu D.

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

Local Lemma integral_csty : mu D != 0 -> \int[mu]_(x in D) (cst +oo) x = +oo.

Local Lemma integral_cstNy : mu D != 0 -> \int[mu]_(x in D) (cst -oo) x = -oo.

End integral_cst.

Section transfer.
Local Open Scope ereal_scope.
Context d1 d2 (X : measurableType d1) (Y : measurableType d2) (R : realType).
Variables (phi : X -> Y) (mphi : measurable_fun setT phi).
Variables (mu : {measure set X -> \bar R}).

Lemma integral_pushforward (f : Y -> \bar R) :
  measurable_fun setT f -> (forall y, 0 <= f y) ->
  \int[pushforward mu mphi]_y f y = \int[mu]_x (f \o phi) x.

End transfer.

Section integral_dirac.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (a : T) (R : realType).
Variables (D : set T) (mD : measurable D).

Let ge0_integral_dirac (f : T -> \bar R) (mf : measurable_fun D f)
    (f0 : forall x, D x -> 0 <= f x) :
  D a -> \int[\d_a]_(x in D) (f x) = f a.

Lemma integral_dirac (f : T -> \bar R) (mf : measurable_fun D f) :
  \int[\d_ a]_(x in D) f x = \d_a D * f a.

End integral_dirac.

Section integral_measure_sum_nnsfun.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (m_ : {measure set T -> \bar R}^nat) (N : nat).
Let m := msum m_ N.

Let integral_measure_sum_indic (E D : set T) (mE : measurable E)
    (mD : measurable D) :
  \int[m]_(x in E) (\1_D x)%:E = \sum_(n < N) \int[m_ n]_(x in E) (\1_D x)%:E.

Let integralT_measure_sum (f : {nnsfun T >-> R}) :
  \int[m]_x (f x)%:E = \sum_(n < N) \int[m_ n]_x (f x)%:E.

Lemma integral_measure_sum_nnsfun (D : set T) (mD : measurable D)
  (f : {nnsfun T >-> R}) :
  \int[m]_(x in D) (f x)%:E = \sum_(n < N) \int[m_ n]_(x in D) (f x)%:E.

End integral_measure_sum_nnsfun.

Lemma integral_measure_add_nnsfun d (T : measurableType d) (R : realType)
    (m1 m2 : {measure set T -> \bar R}) (D : set T) (mD : measurable D)
    (f : {nnsfun T >-> R}) :
  (\int[measure_add m1 m2]_(x in D) (f x)%:E =
   \int[m1]_(x in D) (f x)%:E + \int[m2]_(x in D) (f x)%:E)%E.

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

Lemma ge0_integral_measure_sum (D : set T) (mD : measurable D)
    (f : T -> \bar R) :
    (forall x, D x -> 0 <= f x) -> measurable_fun D f -> forall N,
  \int[msum m_ N]_(x in D) f x = \sum_(n < N) \int[m_ n]_(x in D) f x.

End integral_mfun_measure_sum.

Lemma integral_measure_add d (T : measurableType d) (R : realType)
    (m1 m2 : {measure set T -> \bar R}) (D : set T) (mD : measurable D)
    (f : T -> \bar R) :
  (forall x, D x -> 0 <= f x)%E -> measurable_fun D f ->
  (\int[measure_add m1 m2]_(x in D) f x =
   \int[m1]_(x in D) f x + \int[m2]_(x in D) f x)%E.

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

Let integral_measure_series_indic (D : set T) (mD : measurable D) :
  \int[m]_x (\1_D x)%:E = \sum_(n <oo) \int[m_ n]_x (\1_D x)%:E.

Lemma integral_measure_series_nnsfun (D : set T) (mD : measurable D)
    (f : {nnsfun T >-> R}) :
  \int[m]_x (f x)%:E = \sum_(n <oo) \int[m_ n]_x (f x)%:E.

End integral_measure_series.

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

Lemma ge0_integral_measure_series (D : set T) (mD : measurable D) (f : T -> \bar R) :
  (forall t, D t -> 0 <= f t) ->
  measurable_fun D f ->
  \int[m]_(x in D) f x = \sum_(n <oo) \int[m_ n]_(x in D) f x.

End ge0_integral_measure_series.

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

Lemma integral_setU (A B : set T) (mA : measurable A) (mB : measurable B)
    (f : T -> \bar R) : measurable_fun (A `|` B) f ->
  (forall x, (A `|` B) x -> 0 <= f x) -> [disjoint A & B] ->
  \int[mu]_(x in A `|` B) f x = \int[mu]_(x in A) f x + \int[mu]_(x in B) f x.

Lemma subset_integral (A B : set T) (mA : measurable A) (mB : measurable B)
    (f : T -> \bar R) : measurable_fun B f -> (forall x, B x -> 0 <= f x) ->
  A `<=` B -> \int[mu]_(x in A) f x <= \int[mu]_(x in B) f x.

Lemma integral_set0 (f : T -> \bar R) : \int[mu]_(x in set0) f x = 0.

Lemma ge0_integral_bigsetU (I : eqType) (F : I -> set T) (f : T -> \bar R)
    (s : seq I) : (forall n, measurable (F n)) -> uniq s ->
  trivIset [set` s] F ->
  let D := \big[setU/set0]_(i <- s) F i in
  measurable_fun D f ->
  (forall x, D x -> 0 <= f x) ->
  \int[mu]_(x in D) f x = \sum_(i <- s) \int[mu]_(x in F i) f x.

Lemma le_integral_abse (D : set T) (mD : measurable D) (g : T -> \bar R) a :
  measurable_fun D g -> (0 < a)%R ->
  a%:E * mu (D `&` [set x | `|g x| >= a%:E]) <= \int[mu]_(x in D) `|g x|.

End subset_integral.

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

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

End Rintegral.

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

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

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

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

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

Notation mu_int := (integrable mu D).

Lemma integrable0 : mu_int (cst 0).

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

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

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

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

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

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

Lemma integrable_sum (s : seq (T -> \bar R)) :
  (forall h, h \in s -> mu_int h) -> mu_int (fun x => \sum_(h <- s) h x).

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

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

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

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

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

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

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

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

End integrable_theory.
Notation "mu .-integrable" := (integrable mu) : type_scope.
Arguments eq_integrable {d T R mu D} mD f.
#[deprecated(since="mathcomp-analysis 0.6.4", note="use `integrableZl` instead")]
Notation integrablerM := integrableZl (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.4", note="use `integrableZr` instead")]
Notation integrableMr := integrableZr (only parsing).

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

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

End sequence_measure.

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

Lemma ge0_integral_bigcup (F : (set _)^nat) (f : T -> \bar R) :
  (forall k, measurable (F k)) ->
  let D := \bigcup_k F k in
  mu.-integrable D f ->
  (forall x, D x -> 0 <= f x) ->
  trivIset setT F ->
  \int[mu]_(x in D) f x = \sum_(i <oo) \int[mu]_(x in F i) f x.

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

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

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

Lemma finite_measure_integrable_cst d (T : measurableType d) (R : realType)
    (mu : {finite_measure set T -> \bar R}) k :
  mu.-integrable [set: T] (EFin \o cst k).

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

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

End integrable_ae.

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

Let mesf : measurable_fun D f

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

End linearity.
#[deprecated(since="mathcomp-analysis 0.6.4", note="use `integralZl` instead")]
Notation integralM := integralZl (only parsing).

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

Let mf1 : measurable_fun D g1
Let mf2 : measurable_fun D g2

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

End linearity.

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

Lemma le_abse_integral d (T : measurableType d) (R : realType)
  (mu : {measure set T -> \bar R}) (D : set T) (f : T -> \bar R)
  (mD : measurable D) : measurable_fun D f ->
  (`| \int[mu]_(x in D) (f x) | <= \int[mu]_(x in D) `|f x|)%E.

Lemma abse_integralP d (T : measurableType d) (R : realType)
    (mu : {measure set T -> \bar R}) (D : set T) (f : T -> \bar R) :
    measurable D -> measurable_fun D f ->
  (`| \int[mu]_(x in D) f x | < +oo <-> \int[mu]_(x in D) `|f x| < +oo)%E.

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

Lemma integral_setI_indic (E D : set T) (mD : measurable D) (f : T -> \bar R) :
  measurable E ->
  \int[mu]_(x in E `&` D) f x = \int[mu]_(x in E) (f x * (\1_D x)%:E).

Lemma integralEindic (D : set T) (mD : measurable D) (f : T -> \bar R) :
  \int[mu]_(x in D) f x = \int[mu]_(x in D) (f x * (\1_D x)%:E).

End integral_indic.

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

Local Notation ae_eq := (ae_eq mu).

Let ae_eq_integral_abs_bounded (D : set T) (mD : measurable D) (f : T -> \bar R)
    M : measurable_fun D f -> (forall x, D x -> `|f x| <= M%:E) ->
  ae_eq D f (cst 0) -> \int[mu]_(x in D) `|f x|%E = 0.

Lemma ae_eq_integral_abs (D : set T) (mD : measurable D) (f : T -> \bar R) :
  measurable_fun D f -> \int[mu]_(x in D) `|f x| = 0 <-> ae_eq D f (cst 0).

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

Lemma funID (N : set T) (mN : measurable N) (f : T -> \bar R) :
  let oneCN := [the {nnsfun T >-> R} of mindic R (measurableC mN)] in
  let oneN := [the {nnsfun T >-> R} of mindic R mN] in
  f = (fun x => f x * (oneCN x)%:E) \+ (fun x => f x * (oneN x)%:E).

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

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

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

Lemma ae_eq_integral (D : set T) (g f : T -> \bar R) :
  measurable D -> measurable_fun D f -> measurable_fun D g ->
  ae_eq D f g -> integral mu D f = integral mu D g.

End ae_eq_integral.
Arguments ae_eq_integral {d T R mu D} g.

Local Open Scope ereal_scope.

Lemma integral_cst d (T : measurableType d) (R : realType)
    (mu : {measure set T -> \bar R}) (D : set T) : d.-measurable D ->
  forall r, \int[mu]_(x in D) (cst r) x = r * mu D.
Add Search Blacklist "integral_cstr" "integral_csty" "integral_cstNy".

Lemma le_integral_comp_abse d (T : measurableType d) (R : realType)
    (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D)
    (g : T -> \bar R) a (f : \bar R -> \bar R) (mf : measurable_fun setT f)
    (f0 : forall r, 0 <= r -> 0 <= f r)
    (f_nd : {in `[0, +oo[%classic &, {homo f : x y / x <= y}}) :
  measurable_fun D g -> (0 < a)%R ->
  (f a%:E) * mu (D `&` [set x | (`|g x| >= a%:E)%E]) <= \int[mu]_(x in D) f `|g x|.

Local Close Scope ereal_scope.

Section ae_measurable_fun.
Context d (T : measurableType d) (R : realType)
        (mu : {measure set T -> \bar R}).
Hypothesis cmu : measure_is_complete mu.
Variables (D : set T) (f g : T -> \bar R).

Lemma ae_measurable_fun : ae_eq mu D f g ->
  measurable_fun D f -> measurable_fun D g.

End ae_measurable_fun.

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

Let mf1 : measurable_fun D f1
Let mf2 : measurable_fun D f2

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

End integralD.

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

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

End integralB.

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

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

End negligible_integral.
Add Search Blacklist "ge0_negligible_integral".

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

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

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

End integrable_fune.


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

Lemma counting_dirac (A : set nat) :
  counting A = \sum_(n <oo) \d_ n A :> \bar R.

Lemma summable_integral_dirac (a : nat -> \bar R) : summable setT a ->
  \sum_(n <oo) `|\int[\d_ n]_x a x| < +oo.

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

Lemma ge0_integral_count (a : nat -> \bar R) : (forall k, 0 <= a k) ->
  \int[counting]_t (a t) = \sum_(k <oo) (a k).

End integral_counting.

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

Lemma integrable_abse (D : set T) (f : T -> \bar R) :
  mu.-integrable D f -> mu.-integrable D (abse \o f).

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

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

End subadditive_countable.

Section dominated_convergence_lemma.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
Variables (f_ : (T -> \bar R)^nat) (f : T -> \bar R) (g : T -> \bar R).
Hypothesis mf_ : forall n, measurable_fun D (f_ n).
Hypothesis f_f : forall x, D x -> f_ ^~ x @ \oo --> f x.
Hypothesis fing : forall x, D x -> g x \is a fin_num.
Hypothesis ig : mu.-integrable D g.
Hypothesis absfg : forall n x, D x -> `|f_ n x| <= g x.

Let g0 x : D x -> 0 <= g x.

Let mf : measurable_fun D f.

Local Lemma dominated_integrable : mu.-integrable D f.

Let g_ n x := `|f_ n x - f x|.

Let cvg_g_ x : D x -> g_ ^~ x @ \oo --> 0.

Let gg_ n x : D x -> 0 <= 2%:E * g x - g_ n x.

Let mgg n : measurable_fun D (fun x => 2%:E * g x - g_ n x).

Let gg_ge0 n x : D x -> 0 <= 2%:E * g x - g_ n x.

Local Lemma dominated_cvg0 : [sequence \int[mu]_(x in D) g_ n x]_n @ \oo --> 0.

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

End dominated_convergence_lemma.
Arguments dominated_integrable {d T R mu D} _ f_ f g.

Section dominated_convergence_theorem.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
Variables (f_ : (T -> \bar R)^nat) (f : T -> \bar R) (g : T -> \bar R).
Hypothesis mf_ : forall n, measurable_fun D (f_ n).
Hypothesis mf : measurable_fun D f.
Hypothesis f_f : {ae mu, forall x, D x -> f_ ^~ x @ \oo --> f x}.
Hypothesis ig : mu.-integrable D g.
Hypothesis f_g : {ae mu, forall x n, D x -> `|f_ n x| <= g x}.

Let g_ n x := `|f_ n x - f x|.

Theorem dominated_convergence : [/\ mu.-integrable D f,
  [sequence \int[mu]_(x in D) (g_ n x)]_n @ \oo --> 0 &
  [sequence \int[mu]_(x in D) (f_ n x)]_n @ \oo --> \int[mu]_(x in D) (f x) ].

End dominated_convergence_theorem.

Section ae_ge0_le_integral.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variable mu : {measure set T -> \bar R}.
Variables (D : set T) (mD : measurable D) (f1 f2 : T -> \bar R).
Hypothesis f10 : forall x, D x -> 0 <= f1 x.
Hypothesis mf1 : measurable_fun D f1.
Hypothesis f20 : forall x, D x -> 0 <= f2 x.
Hypothesis mf2 : measurable_fun D f2.

Lemma ae_ge0_le_integral : {ae mu, forall x, D x -> f1 x <= f2 x} ->
  \int[mu]_(x in D) f1 x <= \int[mu]_(x in D) f2 x.

End ae_ge0_le_integral.

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

Lemma integral_le_bound (D : set T) (f : T -> \bar R) (M : \bar R) :
  measurable D -> measurable_fun D f -> 0 <= M ->
  {ae mu, forall x, D x -> `|f x| <= M} ->
  \int[mu]_(x in D) `|f x| <= M * mu D.

End integral_bounded.
Arguments integral_le_bound {d T R mu D f} M.

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

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

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

End integral_ae_eq.


Section measurable_section.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
Implicit Types (A : set (T1 * T2)).

Lemma measurable_xsection A x : measurable A -> measurable (xsection A x).

Lemma measurable_ysection A y : measurable A -> measurable (ysection A y).

End measurable_section.

Section ndseq_closed_B.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
Implicit Types A : set (T1 * T2).

Section xsection.
Variables (pt2 : T2) (m2 : T1 -> {measure set T2 -> \bar R}).
Let phi A x := m2 x (xsection A x).
Let B := [set A | measurable A /\ measurable_fun setT (phi A)].

Lemma xsection_ndseq_closed : ndseq_closed B.
End xsection.

Section ysection.
Variable m1 : {measure set T1 -> \bar R}.
Let psi A := m1 \o ysection A.
Let B := [set A | measurable A /\ measurable_fun setT (psi A)].

Lemma ysection_ndseq_closed : ndseq_closed B.
End ysection.

End ndseq_closed_B.

Section measurable_prod_subset.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
Implicit Types A : set (T1 * T2).

Section xsection.
Variable (m2 : {measure set T2 -> \bar R}) (D : set T2) (mD : measurable D).
Let m2D := mrestr m2 mD.
HB.instance Definition _ := Measure.on m2D.
Let phi A := m2D \o xsection A.
Let B := [set A | measurable A /\ measurable_fun setT (phi A)].

Lemma measurable_prod_subset_xsection
    (m2D_bounded : exists M, forall X, measurable X -> (m2D X < M%:E)%E) :
  measurable `<=` B.

End xsection.

Section ysection.
Variable (m1 : {measure set T1 -> \bar R}) (D : set T1) (mD : measurable D).
Let m1D := mrestr m1 mD.
HB.instance Definition _ := Measure.on m1D.
Let psi A := m1D \o ysection A.
Let B := [set A | measurable A /\ measurable_fun setT (psi A)].

Lemma measurable_prod_subset_ysection
    (m1_bounded : exists M, forall X, measurable X -> (m1D X < M%:E)%E) :
  measurable `<=` B.

End ysection.

End measurable_prod_subset.

Section measurable_fun_xsection.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
Variable m2 : {sigma_finite_measure set T2 -> \bar R}.
Implicit Types A : set (T1 * T2).

Let phi A := m2 \o xsection A.
Let B := [set A | measurable A /\ measurable_fun setT (phi A)].

Lemma measurable_fun_xsection A : measurable A -> measurable_fun setT (phi A).

End measurable_fun_xsection.

Section measurable_fun_ysection.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
Variable m1 : {sigma_finite_measure set T1 -> \bar R}.
Implicit Types A : set (T1 * T2).

Let phi A := m1 \o ysection A.
Let B := [set A | measurable A /\ measurable_fun setT (phi A)].

Lemma measurable_fun_ysection A : measurable A -> measurable_fun setT (phi A).

End measurable_fun_ysection.

Section product_measures.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
Context (m1 : set T1 -> \bar R) (m2 : set T2 -> \bar R).

Definition product_measure1 := (fun A => \int[m1]_x (m2 \o xsection A) x)%E.
Definition product_measure2 := (fun A => \int[m2]_x (m1 \o ysection A) x)%E.

End product_measures.

Notation "m1 '\x' m2" := (product_measure1 m1 m2) : ereal_scope.
Notation "m1 '\x^' m2" := (product_measure2 m1 m2) : ereal_scope.

Section product_measure1.
Local Open Scope ereal_scope.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
Variable m1 : {measure set T1 -> \bar R}.
Variable m2 : {sigma_finite_measure set T2 -> \bar R}.
Implicit Types A : set (T1 * T2).

Let pm10 : (m1 \x m2) set0 = 0.

Let pm1_ge0 A : 0 <= (m1 \x m2) A.

Let pm1_sigma_additive : semi_sigma_additive (m1 \x m2).

HB.instance Definition _ := isMeasure.Build _ _ _ (m1 \x m2)
  pm10 pm1_ge0 pm1_sigma_additive.

End product_measure1.

Section product_measure1E.
Local Open Scope ereal_scope.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
Variable m1 : {measure set T1 -> \bar R}.
Variable m2 : {sigma_finite_measure set T2 -> \bar R}.
Implicit Types A : set (T1 * T2).

Lemma product_measure1E (A1 : set T1) (A2 : set T2) :
  measurable A1 -> measurable A2 -> (m1 \x m2) (A1 `*` A2) = m1 A1 * m2 A2.

End product_measure1E.

Section product_measure_unique.
Local Open Scope ereal_scope.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
Variable m1 : {sigma_finite_measure set T1 -> \bar R}.
Variable m2 : {sigma_finite_measure set T2 -> \bar R}.

Let product_measure_sigma_finite : sigma_finite setT (m1 \x m2).

HB.instance Definition _ := Measure_isSigmaFinite.Build _ _ _ (m1 \x m2)
  product_measure_sigma_finite.

Lemma product_measure_unique
    (m' : {measure set [the semiRingOfSetsType _ of T1 * T2] -> \bar R}) :
    (forall A1 A2, measurable A1 -> measurable A2 ->
      m' (A1 `*` A2) = m1 A1 * m2 A2) ->
  forall X : set (T1 * T2), measurable X -> (m1 \x m2) X = m' X.

End product_measure_unique.

Section product_measure2.
Local Open Scope ereal_scope.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
Variable m1 : {sigma_finite_measure set T1 -> \bar R}.
Variable m2 : {measure set T2 -> \bar R}.
Implicit Types A : set (T1 * T2).

Let pm20 : (m1 \x^ m2) set0 = 0.

Let pm2_ge0 A : 0 <= (m1 \x^ m2) A.

Let pm2_sigma_additive : semi_sigma_additive (m1 \x^ m2).

HB.instance Definition _ := isMeasure.Build _ _ _ (m1 \x^ m2)
  pm20 pm2_ge0 pm2_sigma_additive.

End product_measure2.

Section product_measure2E.
Local Open Scope ereal_scope.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
Variable m1 : {sigma_finite_measure set T1 -> \bar R}.
Variable m2 : {measure set T2 -> \bar R}.

Lemma product_measure2E (A1 : set T1) (A2 : set T2)
    (mA1 : measurable A1) (mA2 : measurable A2) :
  (m1 \x^ m2) (A1 `*` A2) = m1 A1 * m2 A2.

End product_measure2E.

Section simple_density_L1.
Context d (T : measurableType d) (R : realType).
Variables (mu : {measure set T -> \bar R}) (E : set T) (mE : measurable E).

Local Open Scope ereal_scope.

Lemma measurable_bounded_integrable (f : T -> R^o) :
  mu E < +oo -> measurable_fun E f ->
  [bounded f x | x in E] -> mu.-integrable E (EFin \o f).

Let sfun_dense_L1_pos (f : T -> \bar R) :
  mu.-integrable E f -> (forall x, E x -> 0 <= f x) ->
  exists g_ : {sfun T >-> R}^nat,
    [/\ forall n, mu.-integrable E (EFin \o g_ n),
        forall x, E x -> EFin \o g_^~ x @ \oo --> f x &
        (fun n => \int[mu]_(z in E) `|f z - (g_ n z)%:E|) @ \oo --> 0].

Lemma approximation_sfun_integrable (f : T -> \bar R):
  mu.-integrable E f ->
  exists g_ : {sfun T >-> R}^nat,
    [/\ forall n, mu.-integrable E (EFin \o g_ n),
        forall x, E x -> EFin \o g_^~ x @ \oo --> f x &
        (fun n => \int[mu]_(z in E) `|f z - (g_ n z)%:E|) @ \oo --> 0].
End simple_density_L1.

Section continuous_density_L1.
Context (rT : realType).
Let mu := [the measure _ _ of @lebesgue_measure rT].
Let R := [the measurableType _ of measurableTypeR rT].
Local Open Scope ereal_scope.

Lemma compact_finite_measure (A : set R^o) : compact A -> mu A < +oo.

Lemma continuous_compact_integrable (f : R -> R^o) (A : set R^o) :
  compact A -> {within A, continuous f} -> mu.-integrable A (EFin \o f).

Lemma approximation_continuous_integrable (E : set R) (f : R -> R^o):
  measurable E -> mu E < +oo -> mu.-integrable E (EFin \o f) ->
  exists g_ : (rT -> rT)^nat,
    [/\ forall n, continuous (g_ n),
        forall n, mu.-integrable E (EFin \o g_ n) &
        \int[mu]_(z in E) `|(f z - g_ n z)%:E| @[n --> \oo] --> 0].

End continuous_density_L1.

Section fubini_functions.
Local Open Scope ereal_scope.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
Variables (m1 : {measure set T1 -> \bar R}) (m2 : {measure set T2 -> \bar R}).
Variable f : T1 * T2 -> \bar R.

Definition fubini_F x := \int[m2]_y f (x, y).
Definition fubini_G y := \int[m1]_x f (x, y).

End fubini_functions.

Section fubini_tonelli.
Local Open Scope ereal_scope.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
Variable m1 : {sigma_finite_measure set T1 -> \bar R}.
Variable m2 : {sigma_finite_measure set T2 -> \bar R}.

Section indic_fubini_tonelli.
Variables (A : set (T1 * T2)) (mA : measurable A).
Implicit Types A : set (T1 * T2).
Let f : (T1 * T2) -> R := \1_A.

Let F := fubini_F m2 (EFin \o f).
Let G := fubini_G m1 (EFin \o f).

Lemma indic_fubini_tonelli_F_ge0 x : 0 <= F x.

Lemma indic_fubini_tonelli_G_ge0 x : 0 <= G x.

Lemma indic_fubini_tonelli_FE : F = m2 \o xsection A.

Lemma indic_fubini_tonelli_GE : G = m1 \o ysection A.

Lemma indic_measurable_fun_fubini_tonelli_F : measurable_fun setT F.

Lemma indic_measurable_fun_fubini_tonelli_G : measurable_fun setT G.

Lemma indic_fubini_tonelli1 : \int[m1 \x m2]_z (f z)%:E = \int[m1]_x F x.

Lemma indic_fubini_tonelli2 : \int[m1 \x^ m2]_z (f z)%:E = \int[m2]_y G y.

Lemma indic_fubini_tonelli : \int[m1]_x F x = \int[m2]_y G y.

End indic_fubini_tonelli.

Section sfun_fubini_tonelli.
Variable f : {nnsfun [the measurableType _ of T1 * T2 : Type] >-> R}.

Let F := fubini_F m2 (EFin \o f).
Let G := fubini_G m1 (EFin \o f).

Lemma sfun_fubini_tonelli_FE : F = fun x =>
  \sum_(k \in range f) k%:E * m2 (xsection (f @^-1` [set k]) x).

Lemma sfun_measurable_fun_fubini_tonelli_F : measurable_fun setT F.

Lemma sfun_fubini_tonelli_GE : G = fun y =>
  \sum_(k \in range f) k%:E * m1 (ysection (f @^-1` [set k]) y).

Lemma sfun_measurable_fun_fubini_tonelli_G : measurable_fun setT G.

Let EFinf x : (f x)%:E =
  \sum_(k \in range f) k%:E * (\1_(f @^-1` [set k]) x)%:E.

Lemma sfun_fubini_tonelli1 : \int[m1 \x m2]_z (f z)%:E = \int[m1]_x F x.

Lemma sfun_fubini_tonelli2 : \int[m1 \x^ m2]_z (f z)%:E = \int[m2]_y G y.

Lemma sfun_fubini_tonelli :
  \int[m1 \x m2]_z (f z)%:E = \int[m1 \x^ m2]_z (f z)%:E.

End sfun_fubini_tonelli.

Section fubini_tonelli.
Variable f : T1 * T2 -> \bar R.
Hypothesis mf : measurable_fun setT f.
Hypothesis f0 : forall x, 0 <= f x.
Let T := [the measurableType _ of T1 * T2 : Type].

Let F := fubini_F m2 f.
Let G := fubini_G m1 f.

Let F_ (g : {nnsfun T >-> R}^nat) n x := \int[m2]_y (g n (x, y))%:E.
Let G_ (g : {nnsfun T >-> R}^nat) n y := \int[m1]_x (g n (x, y))%:E.

Lemma measurable_fun_fubini_tonelli_F : measurable_fun setT F.

Lemma measurable_fun_fubini_tonelli_G : measurable_fun setT G.

Lemma fubini_tonelli1 : \int[m1 \x m2]_z f z = \int[m1]_x F x.

Lemma fubini_tonelli2 : \int[m1 \x m2]_z f z = \int[m2]_y G y.

Lemma fubini_tonelli :
  \int[m1]_x \int[m2]_y f (x, y) = \int[m2]_y \int[m1]_x f (x, y).

End fubini_tonelli.

End fubini_tonelli.
Arguments fubini_tonelli1 {d1 d2 T1 T2 R m1 m2} f.
Arguments fubini_tonelli2 {d1 d2 T1 T2 R m1 m2} f.
Arguments fubini_tonelli {d1 d2 T1 T2 R m1 m2} f.
Arguments measurable_fun_fubini_tonelli_F {d1 d2 T1 T2 R m2} f.
Arguments measurable_fun_fubini_tonelli_G {d1 d2 T1 T2 R m1} f.

Section fubini.
Local Open Scope ereal_scope.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
Variable m1 : {sigma_finite_measure set T1 -> \bar R}.
Variable m2 : {sigma_finite_measure set T2 -> \bar R}.
Variable f : T1 * T2 -> \bar R.

Hypothesis imf : (m1 \x m2).-integrable setT f.
Let mf : measurable_fun setT f

Lemma fubini1a :
  (m1 \x m2).-integrable setT f <-> \int[m1]_x \int[m2]_y `|f (x, y)| < +oo.

Lemma fubini1b :
  (m1 \x m2).-integrable setT f <-> \int[m2]_y \int[m1]_x `|f (x, y)| < +oo.

Let measurable_fun1 : measurable_fun setT (fun x => \int[m2]_y `|f (x, y)|).

Let measurable_fun2 : measurable_fun setT (fun y => \int[m1]_x `|f (x, y)|).

Lemma ae_integrable1 :
  {ae m1, forall x, m2.-integrable setT (fun y => f (x, y))}.

Lemma ae_integrable2 :
  {ae m2, forall y, m1.-integrable setT (fun x => f (x, y))}.

Let F := fubini_F m2 f.

Let Fplus x := \int[m2]_y f^\+ (x, y).
Let Fminus x := \int[m2]_y f^\- (x, y).

Let FE : F = Fplus \- Fminus

Let measurable_Fplus : measurable_fun setT Fplus.

Let measurable_Fminus : measurable_fun setT Fminus.

Lemma measurable_fubini_F : measurable_fun setT F.

Let integrable_Fplus : m1.-integrable setT Fplus.

Let integrable_Fminus : m1.-integrable setT Fminus.

Lemma integrable_fubini_F : m1.-integrable setT F.

Let G := fubini_G m1 f.

Let Gplus y := \int[m1]_x f^\+ (x, y).
Let Gminus y := \int[m1]_x f^\- (x, y).

Let GE : G = Gplus \- Gminus

Let measurable_Gplus : measurable_fun setT Gplus.

Let measurable_Gminus : measurable_fun setT Gminus.

Lemma measurable_fubini_G : measurable_fun setT G.

Let integrable_Gplus : m2.-integrable setT Gplus.

Let integrable_Gminus : m2.-integrable setT Gminus.

Lemma fubini1 : \int[m1]_x F x = \int[m1 \x m2]_z f z.

Lemma fubini2 : \int[m2]_x G x = \int[m1 \x m2]_z f z.

Theorem Fubini :
  \int[m1]_x \int[m2]_y f (x, y) = \int[m2]_y \int[m1]_x f (x, y).

End fubini.

Section sfinite_fubini.
Local Open Scope ereal_scope.
Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
Variables (m1 : {sfinite_measure set X -> \bar R}).
Variables (m2 : {sfinite_measure set Y -> \bar R}).
Variables (f : X * Y -> \bar R) (f0 : forall xy, 0 <= f xy).
Hypothesis mf : measurable_fun setT f.

Lemma sfinite_Fubini :
  \int[m1]_x \int[m2]_y f (x, y) = \int[m2]_y \int[m1]_x f (x, y).

End sfinite_fubini.
Arguments sfinite_Fubini {d d' X Y R} m1 m2 f.

Section lebesgue_differentiation_continuous.
Context (rT : realType).
Let mu := [the measure _ _ of @lebesgue_measure rT].
Let R := [the measurableType _ of measurableTypeR rT].

Let ballE (x : R) (r : {posnum rT}) :
  ball x r%:num = `](x - r%:num), (x + r%:num)[%classic :> set rT.

Lemma lebesgue_differentiation_continuous (f : R -> rT^o) (A : set R) (x : R) :
  open A -> mu.-integrable A (EFin \o f) -> {for x, continuous f} -> A x ->
  (fun r => 1 / (r *+ 2) * \int[mu]_(z in ball x r) f z) @ 0^'+ -->
  (f x : R^o).

End lebesgue_differentiation_continuous.

Section locally_integrable.
Context {R : realType}.
Implicit Types (D : set R) (f g : R -> R).
Local Open Scope ereal_scope.

Local Notation mu := lebesgue_measure.

Definition locally_integrable D f := [/\ measurable_fun D f, open D &
  forall K, K `<=` D -> compact K -> \int[mu]_(x in K) `|f x|%:E < +oo].

Lemma integrable_locally D f : open D ->
  mu.-integrable D (EFin \o f) -> locally_integrable D f.

Lemma locally_integrableN D f :
  locally_integrable D f -> locally_integrable D (\- f)%R.

Lemma locally_integrableD D f g :
  locally_integrable D f -> locally_integrable D g ->
  locally_integrable D (f \+ g)%R.

Lemma locally_integrableB D f g :
  locally_integrable D f -> locally_integrable D g ->
  locally_integrable D (f \- g)%R.

End locally_integrable.

Section iavg.
Context {R : realType}.
Implicit Types (D A : set R) (f g : R -> R).
Local Open Scope ereal_scope.

Local Notation mu := lebesgue_measure.

Definition iavg f A := (fine (mu A))^-1%:E * \int[mu]_(y in A) `| (f y)%:E |.

Lemma iavg0 f : iavg f set0 = 0.

Lemma iavg_ge0 f A : 0 <= iavg f A.

Lemma iavg_restrict f D A : measurable D -> measurable A ->
  iavg (f \_ D) A = ((fine (mu A))^-1)%:E * \int[mu]_(y in D `&` A) `|f y|%:E.

Lemma iavgD f g A : measurable A -> mu A < +oo ->
  measurable_fun A f -> measurable_fun A g ->
  iavg (f \+ g)%R A <= iavg f A + iavg g A.

End iavg.

Section hardy_littlewood.
Context {R : realType}.
Notation mu := (@lebesgue_measure R).
Implicit Types (D : set R) (f : R -> R).
Local Open Scope ereal_scope.

Definition HL_maximal f (x : R) : \bar R :=
  ereal_sup [set iavg f (ball x r) | r in `]0, +oo[%classic%R].

Local Notation HL := HL_maximal.

Lemma HL_maximal_ge0 f D : locally_integrable D f ->
  forall x, 0 <= HL (f \_ D) x.

Lemma HL_maximalT_ge0 f : locally_integrable setT f -> forall x, 0 <= HL f x.

Let locally_integrable_ltbally (f : R -> R) (x r : R) :
  locally_integrable setT f -> \int[mu]_(y in ball x r) `|(f y)%:E| < +oo.

Lemma lower_semicontinuous_HL_maximal f :
  locally_integrable setT f -> lower_semicontinuous (HL f).

Lemma measurable_HL_maximal f :
  locally_integrable setT f -> measurable_fun setT (HL f).

Let norm1 D f := \int[mu]_(y in D) `|(f y)%:E|.

Lemma maximal_inequality f c :
  locally_integrable setT f -> (0 < c)%R ->
  mu [set x | HL f x > c%:E] <= (3%:R / c)%:E * norm1 setT f.

End hardy_littlewood.