Library mathcomp.analysis.lebesgue_integral
(* -*- company-coq-local-symbols: (("\\int" . ?β«) ("\\int_" . ?β«) ("'d" . ?π)); -*-
mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
Require Import mathcomp_extra boolp classical_sets posnum functions cardinality.
Require Import reals ereal topology normedtype sequences measure.
Require Import nngnum lebesgue_measure fsbigop numfun.
mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
Require Import mathcomp_extra boolp classical_sets posnum functions cardinality.
Require Import reals ereal topology normedtype sequences measure.
Require Import nngnum lebesgue_measure fsbigop numfun.
Lebesgue Integral
This file contains a formalization of the Lebesgue integral. It starts
with simple functions and their integral, provides basic operations
(addition, etc.), and proves the properties of their integral
(semi-linearity, non-decreasingness). It then defines the integral of
measurable functions, proves the approximation theorem, the properties of
their integral (semi-linearity, non-decreasingness), the monotone
convergence theorem, and Fatou's lemma. Finally, it proves the linearity
properties of the integral, the dominated convergence theorem and Fubini's
theorem.
Main reference:
- Daniel Li, IntΓ©gration et applications, 2016
{nnfun T >-> R} == type of non-negative functions {fimfun T >-> R} == type of functions with a finite image {sfun T >-> R} == type of simple functions {nnsfun T >-> R} == type of non-negative simple functions cst_nnsfun r == constant simple function nnsfun0 := cst_nnsfun 0 sintegral mu f == integral of the function f with the measure mu
Set Implicit Arguments.
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_' D f ''d' mu [ x ]" (at level 36, D at level 0,
f at level 36, mu at level 0, x at level 35,
format "'\int_' D f ''d' mu [ x ]").
Reserved Notation "'\int' f ''d' mu [ x ]" (at level 36, f at level 36,
mu at level 0, x at level 3, format "'\int' f ''d' mu [ x ]").
Reserved Notation "mu .-integrable" (at level 2, format "mu .-integrable").
#[global]
Hint Extern 0 (measurable [set _]) β solve [apply: measurable_set1] : core.
#[global] Hint Resolve fimfun_inP : core.
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.
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 {aT : measurableType} {rT : realType} (f : {mfun aT >-> rT}) (y : rT) :
measurable (f @^-1` [set y]).
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.
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 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).
Canonical fimfun_mul := MulrPred fimfun_mulr_closed.
Canonical fimfun_ring := SubringPred fimfun_mulr_closed.
Definition fimfun_ringMixin := [ringMixin of {fimfun aT >-> rT} by <:].
Canonical fimfun_ringType := RingType {fimfun aT >-> rT} fimfun_ringMixin.
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.
Definition indic_fimfun (X : set aT) := [the {fimfun aT >-> rT} of \1_X].
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).
Definition fimfun_comRingMixin := [comRingMixin of {fimfun aT >-> rT} by <:].
Canonical fimfun_comRingType :=
ComRingType {fimfun aT >-> rT} fimfun_comRingMixin.
Implicit Types (f g : {fimfun aT >-> rT}).
End comring.
Lemma fimfunE T (R : ringType) (f : {fimfun T >-> R}) x :
f x = \sum_(y <- fset_set (range f)) (y Γ \1_(f @^-1` [set y]) x).
Lemma fimfunEord T (R : ringType) (f : {fimfun T >-> R})
(s := fset_set (f @` setT)) :
β 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 (T : measurableType) (R : numDomainType) (f g : {fimfun T >-> R}).
Lemma max_fimfun_subproof : @FiniteImage T R (f \max g).
End fimfun_bin.
Lemma finite_subproof: @FiniteImage T R f.
Section mfun_pred.
Context {aT : measurableType} {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 {aT : measurableType} {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 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) :
(β f (Pf : f \in mfun), K (mfun_Sub Pf)) β β u : T, K u.
Lemma mfun_valP f (Pf : f \in mfun) : mfun_Sub Pf = f :> (_ β _).
Canonical mfun_subType := SubType T _ _ mfun_rect mfun_valP.
Lemma mfuneqP (f g : {mfun aT >-> rT}) : f = g β f =1 g.
Definition mfuneqMixin := [eqMixin of {mfun aT >-> rT} by <:].
Canonical mfuneqType := EqType {mfun aT >-> rT} mfuneqMixin.
Definition mfunchoiceMixin := [choiceMixin of {mfun aT >-> rT} by <:].
Canonical mfunchoiceType := ChoiceType {mfun aT >-> rT} mfunchoiceMixin.
Lemma cst_mfun_subproof x : @IsMeasurableFun aT rT (cst x).
Definition cst_mfun x := [the {mfun aT >-> rT} of cst x].
Lemma mfun_cst x : @cst_mfun x =1 cst x.
End mfun.
Section ring.
Context (aT : measurableType) (rT : realType).
Lemma mfun_subring_closed : subring_closed (@mfun aT rT).
Canonical mfun_add := AddrPred mfun_subring_closed.
Canonical mfun_zmod := ZmodPred mfun_subring_closed.
Canonical mfun_mul := MulrPred mfun_subring_closed.
Canonical mfun_subring := SubringPred mfun_subring_closed.
Definition mfun_zmodMixin := [zmodMixin of {mfun aT >-> rT} by <:].
Canonical mfun_zmodType := ZmodType {mfun aT >-> rT} mfun_zmodMixin.
Definition mfun_ringMixin := [ringMixin of {mfun aT >-> rT} by <:].
Canonical mfun_ringType := RingType {mfun aT >-> rT} mfun_ringMixin.
Definition mfun_comRingMixin := [comRingMixin of {mfun aT >-> rT} by <:].
Canonical mfun_comRingType := ComRingType {mfun aT >-> rT} mfun_comRingMixin.
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) :> (_ β _).
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).
Lemma indic_mfun_subproof (D : set aT) (mD : measurable D) :
@IsMeasurableFun aT rT (mindic mD).
Definition indic_mfun (D : set aT) (mD : measurable D) :=
[the {mfun aT >-> rT} of mindic mD].
Definition scale_mfun k f := [the {mfun aT >-> rT} of k \oΓ f].
Lemma max_mfun_subproof f g : @IsMeasurableFun aT rT (f \max g).
Definition max_mfun f g := [the {mfun aT >-> _} of f \max g].
End ring.
Arguments indic_mfun {aT rT} _.
Section sfun_pred.
Context {aT : measurableType} {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 {aT : measurableType} {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 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) :
(β f (Pf : f \in sfun), K (sfun_Sub Pf)) β β u : T, K u.
Lemma sfun_valP f (Pf : f \in sfun) : sfun_Sub Pf = f :> (_ β _).
Canonical sfun_subType := SubType T _ _ sfun_rect sfun_valP.
Lemma sfuneqP (f g : {sfun aT >-> rT}) : f = g β f =1 g.
Definition sfuneqMixin := [eqMixin of {sfun aT >-> rT} by <:].
Canonical sfuneqType := EqType {sfun aT >-> rT} sfuneqMixin.
Definition sfunchoiceMixin := [choiceMixin of {sfun aT >-> rT} by <:].
Canonical sfunchoiceType := ChoiceType {sfun aT >-> rT} sfunchoiceMixin.
TODO: BUG: HB
HB.instance Definition _ (x : rT) := @cst_mfun_subproof aT rT x.
Definition cst_sfun x := [the {sfun aT >-> rT} of cst x].
Lemma cst_sfunE x : @cst_sfun x =1 cst x.
End sfun.
Lemma cst_sfunE x : @cst_sfun x =1 cst x.
End sfun.
a better way to refactor function stuffs
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 (aT : measurableType) (rT : realType).
Lemma sfun_subring_closed : subring_closed (@sfun aT rT).
Canonical sfun_add := AddrPred sfun_subring_closed.
Canonical sfun_zmod := ZmodPred sfun_subring_closed.
Canonical sfun_mul := MulrPred sfun_subring_closed.
Canonical sfun_subring := SubringPred sfun_subring_closed.
Definition sfun_zmodMixin := [zmodMixin of {sfun aT >-> rT} by <:].
Canonical sfun_zmodType := ZmodType {sfun aT >-> rT} sfun_zmodMixin.
Definition sfun_ringMixin := [ringMixin of {sfun aT >-> rT} by <:].
Canonical sfun_ringType := RingType {sfun aT >-> rT} sfun_ringMixin.
Definition sfun_comRingMixin := [comRingMixin of {sfun aT >-> rT} by <:].
Canonical sfun_comRingType := ComRingType {sfun aT >-> rT} sfun_comRingMixin.
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).
Definition indic_sfun (D : set aT) (mD : measurable D) :=
[the {sfun aT >-> rT} of mindic rT mD].
Definition scale_sfun k f := [the {sfun aT >-> rT} of k \oΓ f].
Definition max_sfun f g := [the {sfun aT >-> _} of f \max g].
End ring.
Arguments indic_sfun {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_cst T (R : eqType) (x y : R) :
@cst T _ x @^-1` [set y] = if x == y then setT else 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 nnsfun_functions.
Variables (T : measurableType) (R : realType).
Lemma cst_nnfun_subproof (x : {nonneg R}) : @IsNonNegFun T R (cst x%:nngnum).
Definition cst_nnsfun (r : {nonneg R}) := [the {nnsfun T >-> R} of cst r%:nngnum].
Definition nnsfun0 : {nnsfun T >-> R} := cst_nnsfun 0%R%:nng.
Lemma indic_nnfun_subproof (D : set T) : @IsNonNegFun T R (\1_D).
End nnsfun_functions.
Arguments nnsfun0 {T R}.
Section nnfun_bin.
Variables (T : Type) (R : numDomainType) (f g : {nnfun T >-> R}).
Lemma add_nnfun_subproof : @IsNonNegFun T R (f \+ g).
Lemma mul_nnfun_subproof : @IsNonNegFun T R (f \* g).
Lemma max_nnfun_subproof : @IsNonNegFun T R (f \max g).
End nnfun_bin.
Section nnsfun_bin.
Variables (T : measurableType) (R : realType) (f g : {nnsfun T >-> R}).
Definition add_nnsfun := [the {nnsfun T >-> R} of f \+ g].
Definition mul_nnsfun := [the {nnsfun T >-> R} of f \* 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 {T R} _ _.
Arguments mul_nnsfun {T R} _ _.
Arguments max_nnsfun {T R} _ _.
Section nnsfun_iter.
Variables (T : measurableType) (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.
Variables (T : measurableType) (R : realType) (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] : core.
Lemma measurable_sfun_inP {aT : measurableType} {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.
Variables (T : measurableType) (R : realType) (m : {measure set T β \bar R}).
Lemma measure_fsbig (I : choiceType) (A : set I) (F : I β set T) :
finite_set A β
(β 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) :
(β x, 0 β€ f x) β ((x < 0)%R β f x = 0) β 0 β€ x%:E Γ f x.
Lemma muleindic_ge0 T (R : realDomainType) (f : {nnfun T >-> R}) r z :
0 β€ r%:E Γ (\1_(f @^-1` [set r]) z)%:E.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Lemma mulem_ge0 x (A : R β set T) :
((x < 0)%R β A x = set0) β 0 β€ x%:E Γ mu (A x).
Lemma nnfun_mulem_ge0 (f : {nnfun T >-> R}) x :
0 β€ x%:E Γ mu (f @^-1` [set x]).
End mulem_ge0.
Arguments mulem_ge0 {T R mu x} A.
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 (aT : measurableType) (rT : realType).
Lemma sfun_subring_closed : subring_closed (@sfun aT rT).
Canonical sfun_add := AddrPred sfun_subring_closed.
Canonical sfun_zmod := ZmodPred sfun_subring_closed.
Canonical sfun_mul := MulrPred sfun_subring_closed.
Canonical sfun_subring := SubringPred sfun_subring_closed.
Definition sfun_zmodMixin := [zmodMixin of {sfun aT >-> rT} by <:].
Canonical sfun_zmodType := ZmodType {sfun aT >-> rT} sfun_zmodMixin.
Definition sfun_ringMixin := [ringMixin of {sfun aT >-> rT} by <:].
Canonical sfun_ringType := RingType {sfun aT >-> rT} sfun_ringMixin.
Definition sfun_comRingMixin := [comRingMixin of {sfun aT >-> rT} by <:].
Canonical sfun_comRingType := ComRingType {sfun aT >-> rT} sfun_comRingMixin.
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).
Definition indic_sfun (D : set aT) (mD : measurable D) :=
[the {sfun aT >-> rT} of mindic rT mD].
Definition scale_sfun k f := [the {sfun aT >-> rT} of k \oΓ f].
Definition max_sfun f g := [the {sfun aT >-> _} of f \max g].
End ring.
Arguments indic_sfun {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_cst T (R : eqType) (x y : R) :
@cst T _ x @^-1` [set y] = if x == y then setT else 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 nnsfun_functions.
Variables (T : measurableType) (R : realType).
Lemma cst_nnfun_subproof (x : {nonneg R}) : @IsNonNegFun T R (cst x%:nngnum).
Definition cst_nnsfun (r : {nonneg R}) := [the {nnsfun T >-> R} of cst r%:nngnum].
Definition nnsfun0 : {nnsfun T >-> R} := cst_nnsfun 0%R%:nng.
Lemma indic_nnfun_subproof (D : set T) : @IsNonNegFun T R (\1_D).
End nnsfun_functions.
Arguments nnsfun0 {T R}.
Section nnfun_bin.
Variables (T : Type) (R : numDomainType) (f g : {nnfun T >-> R}).
Lemma add_nnfun_subproof : @IsNonNegFun T R (f \+ g).
Lemma mul_nnfun_subproof : @IsNonNegFun T R (f \* g).
Lemma max_nnfun_subproof : @IsNonNegFun T R (f \max g).
End nnfun_bin.
Section nnsfun_bin.
Variables (T : measurableType) (R : realType) (f g : {nnsfun T >-> R}).
Definition add_nnsfun := [the {nnsfun T >-> R} of f \+ g].
Definition mul_nnsfun := [the {nnsfun T >-> R} of f \* 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 {T R} _ _.
Arguments mul_nnsfun {T R} _ _.
Arguments max_nnsfun {T R} _ _.
Section nnsfun_iter.
Variables (T : measurableType) (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.
Variables (T : measurableType) (R : realType) (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] : core.
Lemma measurable_sfun_inP {aT : measurableType} {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.
Variables (T : measurableType) (R : realType) (m : {measure set T β \bar R}).
Lemma measure_fsbig (I : choiceType) (A : set I) (F : I β set T) :
finite_set A β
(β 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) :
(β x, 0 β€ f x) β ((x < 0)%R β f x = 0) β 0 β€ x%:E Γ f x.
Lemma muleindic_ge0 T (R : realDomainType) (f : {nnfun T >-> R}) r z :
0 β€ r%:E Γ (\1_(f @^-1` [set r]) z)%:E.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Lemma mulem_ge0 x (A : R β set T) :
((x < 0)%R β A x = set0) β 0 β€ x%:E Γ mu (A x).
Lemma nnfun_mulem_ge0 (f : {nnfun T >-> R}) x :
0 β€ x%:E Γ mu (f @^-1` [set x]).
End mulem_ge0.
Arguments mulem_ge0 {T R mu x} A.
Definition of Simple Integrals
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.
Variables (T : measurableType) (R : realType) (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.
NB: not used
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 (T : measurableType) (R : numDomainType) (mu : set T β \bar R) g f :
f =1 g β sintegral mu f = sintegral mu g.
Arguments eq_sintegral {T R mu} g.
Section sintegralrM.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (m : {measure set T β \bar R}).
Variables (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.
Variables (T : measurableType) (R : realType) (m : {measure set T β \bar R}).
Variables (f g : {nnsfun T >-> R}).
Lemma sintegralD : sintegral m (f \+ g)%R = sintegral m f + sintegral m g.
End sintegralD.
Section le_sintegral.
Variables (T : measurableType) (R : realType) (m : {measure set T β \bar R}).
Variables f g : {nnsfun T >-> R}.
Hypothesis fg : β 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 (T : measurableType) (R : realType)
(m : {measure set T β \bar R}) (f : {nnsfun T >-> R}^nat) :
(β x, nondecreasing_seq (f ^~ x)) β cvg (fun n β sintegral m (f n)).
Definition proj_nnsfun (T : measurableType) (R : realType)
(f : {nnsfun T >-> R}) (A : set T) (mA : measurable A) :=
mul_nnsfun f (indic_nnsfun R mA).
Definition mrestrict (T : measurableType) (R : realType) (f : {nnsfun T >-> R})
A (mA : measurable A) : f \_ A = proj_nnsfun f mA.
Definition scale_nnsfun (T : measurableType) (R : realType)
(f : {nnsfun T >-> R}) (k : R) (k0 : 0 β€ k) :=
mul_nnsfun (cst_nnsfun T (NngNum k0)) f.
Section sintegral_nondecreasing_limit_lemma.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (g : {nnsfun T >-> R}^nat) (f : {nnsfun T >-> R}).
Hypothesis nd_g : β x, nondecreasing_seq (g^~ x).
Hypothesis gf : β x, cvg (g^~ x) β f x β€ lim (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 β€ lim (sintegral mu \o g).
End sintegral_nondecreasing_limit_lemma.
Section sintegral_nondecreasing_limit.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (g : {nnsfun T >-> R}^nat) (f : {nnsfun T >-> R}).
Hypothesis nd_g : β x, nondecreasing_seq (g^~ x).
Hypothesis gf : β x, g ^~ x --> f x.
Let limg x : lim (g^~x) = f x.
Lemma nd_sintegral_lim : sintegral mu f = lim (sintegral mu \o g).
End sintegral_nondecreasing_limit.
Section integral.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Implicit Types (f g : T β \bar R) (D : set T).
Let nnintegral f := ereal_sup [set sintegral mu h |
h in [set h : {nnsfun T >-> R} | β x, (h x)%:E β€ f x]].
Let nnintegral_ge0 f : (β x, 0 β€ f x) β 0 β€ nnintegral f.
Let eq_nnintegral g f : f =1 g β nnintegral f = nnintegral g.
Let nnintegral0 : nnintegral (cst 0) = 0.
Let nnintegral_nnsfun (h : {nnsfun T >-> R}) :
nnintegral (EFin \o h) = sintegral mu h.
Definition integral D f (g := f \_ D) :=
nnintegral (g ^\+) - nnintegral (g ^\-).
Lemma eq_integral D g f : {in D, f =1 g} β
\int_ D (f x) 'd x = \int_ D (g x) 'd x.
Lemma ge0_integralE D f : (β x, D x β 0 β€ f x) β
\int_ D (f x) 'd x = nnintegral (f \_ D).
Lemma ge0_integralTE f : (β x, 0 β€ f x) β
\int_ setT (f x) 'd x = nnintegral f.
Lemma integralE D f :
\int_ D (f x) 'd x = \int_ D (f ^\+ x) 'd x - \int_ D (f ^\- x) 'd x.
Lemma integral0 D : \int_ D (cst 0 x) 'd x = 0.
Lemma integral_ge0 D f : (β x, D x β 0 β€ f x) β 0 β€ \int_ D (f x) 'd x.
Lemma integral_nnsfun D (mD : measurable D) (h : {nnsfun T >-> R}) :
\int_ D ((EFin \o h) x) 'd x = sintegral mu (h \_ D).
End integral.
Notation "\int_ D f 'd mu [ x ]" := (integral mu D (fun x β f)) : ereal_scope.
Notation "\int f 'd mu [ x ]" := (\int_ setT f 'd mu[x])%E : ereal_scope.
Arguments eq_integral {T R mu D} g.
Section domain_change.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Lemma integral_mkcond D f : \int_D f x 'd mu[x] = \int (f \_ D) x 'd mu [x].
Lemma integralT_nnsfun (h : {nnsfun T >-> R}) :
\int ((EFin \o h) x) 'd mu[x] = sintegral mu h.
Lemma integral_mkcondr D P f :
\int_(D `&` P) f x 'd mu[x] = \int_D (f \_ P) x 'd mu [x].
Lemma integral_mkcondl D P f :
\int_(P `&` D) f x 'd mu[x] = \int_D (f \_ P) x 'd mu [x].
End domain_change.
Arguments integral_mkcond {T R mu} D f.
Section nondecreasing_integral_limit.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (f : T β \bar R) (g : {nnsfun T >-> R}^nat).
Hypothesis f0 : β x, 0 β€ f x.
Hypothesis mf : measurable_fun setT f.
Hypothesis nd_g : β x, nondecreasing_seq (g^~x).
Hypothesis gf : β x, EFin \o g^~x --> f x.
Local Open Scope ereal_scope.
Lemma nd_ge0_integral_lim : \int f x 'd mu [x] = lim (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)[.
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 β
β 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.
Variables (T : measurableType) (R : realType) (D : set T) (mD : measurable D).
Variables (f : T β \bar R) (mf : measurable_fun D f).
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 Γ (x \in A n k)%:R +
n%:R Γ (x \in B n)%:R.
(\sum_(x \in [set r | r > 0]%R) (x%:E Γ mu (f @^-1` [set x])))%E.
End sintegral_lemmas.
Lemma eq_sintegral (T : measurableType) (R : numDomainType) (mu : set T β \bar R) g f :
f =1 g β sintegral mu f = sintegral mu g.
Arguments eq_sintegral {T R mu} g.
Section sintegralrM.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (m : {measure set T β \bar R}).
Variables (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.
Variables (T : measurableType) (R : realType) (m : {measure set T β \bar R}).
Variables (f g : {nnsfun T >-> R}).
Lemma sintegralD : sintegral m (f \+ g)%R = sintegral m f + sintegral m g.
End sintegralD.
Section le_sintegral.
Variables (T : measurableType) (R : realType) (m : {measure set T β \bar R}).
Variables f g : {nnsfun T >-> R}.
Hypothesis fg : β 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 (T : measurableType) (R : realType)
(m : {measure set T β \bar R}) (f : {nnsfun T >-> R}^nat) :
(β x, nondecreasing_seq (f ^~ x)) β cvg (fun n β sintegral m (f n)).
Definition proj_nnsfun (T : measurableType) (R : realType)
(f : {nnsfun T >-> R}) (A : set T) (mA : measurable A) :=
mul_nnsfun f (indic_nnsfun R mA).
Definition mrestrict (T : measurableType) (R : realType) (f : {nnsfun T >-> R})
A (mA : measurable A) : f \_ A = proj_nnsfun f mA.
Definition scale_nnsfun (T : measurableType) (R : realType)
(f : {nnsfun T >-> R}) (k : R) (k0 : 0 β€ k) :=
mul_nnsfun (cst_nnsfun T (NngNum k0)) f.
Section sintegral_nondecreasing_limit_lemma.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (g : {nnsfun T >-> R}^nat) (f : {nnsfun T >-> R}).
Hypothesis nd_g : β x, nondecreasing_seq (g^~ x).
Hypothesis gf : β x, cvg (g^~ x) β f x β€ lim (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 β€ lim (sintegral mu \o g).
End sintegral_nondecreasing_limit_lemma.
Section sintegral_nondecreasing_limit.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (g : {nnsfun T >-> R}^nat) (f : {nnsfun T >-> R}).
Hypothesis nd_g : β x, nondecreasing_seq (g^~ x).
Hypothesis gf : β x, g ^~ x --> f x.
Let limg x : lim (g^~x) = f x.
Lemma nd_sintegral_lim : sintegral mu f = lim (sintegral mu \o g).
End sintegral_nondecreasing_limit.
Section integral.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Implicit Types (f g : T β \bar R) (D : set T).
Let nnintegral f := ereal_sup [set sintegral mu h |
h in [set h : {nnsfun T >-> R} | β x, (h x)%:E β€ f x]].
Let nnintegral_ge0 f : (β x, 0 β€ f x) β 0 β€ nnintegral f.
Let eq_nnintegral g f : f =1 g β nnintegral f = nnintegral g.
Let nnintegral0 : nnintegral (cst 0) = 0.
Let nnintegral_nnsfun (h : {nnsfun T >-> R}) :
nnintegral (EFin \o h) = sintegral mu h.
Definition integral D f (g := f \_ D) :=
nnintegral (g ^\+) - nnintegral (g ^\-).
Lemma eq_integral D g f : {in D, f =1 g} β
\int_ D (f x) 'd x = \int_ D (g x) 'd x.
Lemma ge0_integralE D f : (β x, D x β 0 β€ f x) β
\int_ D (f x) 'd x = nnintegral (f \_ D).
Lemma ge0_integralTE f : (β x, 0 β€ f x) β
\int_ setT (f x) 'd x = nnintegral f.
Lemma integralE D f :
\int_ D (f x) 'd x = \int_ D (f ^\+ x) 'd x - \int_ D (f ^\- x) 'd x.
Lemma integral0 D : \int_ D (cst 0 x) 'd x = 0.
Lemma integral_ge0 D f : (β x, D x β 0 β€ f x) β 0 β€ \int_ D (f x) 'd x.
Lemma integral_nnsfun D (mD : measurable D) (h : {nnsfun T >-> R}) :
\int_ D ((EFin \o h) x) 'd x = sintegral mu (h \_ D).
End integral.
Notation "\int_ D f 'd mu [ x ]" := (integral mu D (fun x β f)) : ereal_scope.
Notation "\int f 'd mu [ x ]" := (\int_ setT f 'd mu[x])%E : ereal_scope.
Arguments eq_integral {T R mu D} g.
Section domain_change.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Lemma integral_mkcond D f : \int_D f x 'd mu[x] = \int (f \_ D) x 'd mu [x].
Lemma integralT_nnsfun (h : {nnsfun T >-> R}) :
\int ((EFin \o h) x) 'd mu[x] = sintegral mu h.
Lemma integral_mkcondr D P f :
\int_(D `&` P) f x 'd mu[x] = \int_D (f \_ P) x 'd mu [x].
Lemma integral_mkcondl D P f :
\int_(P `&` D) f x 'd mu[x] = \int_D (f \_ P) x 'd mu [x].
End domain_change.
Arguments integral_mkcond {T R mu} D f.
Section nondecreasing_integral_limit.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (f : T β \bar R) (g : {nnsfun T >-> R}^nat).
Hypothesis f0 : β x, 0 β€ f x.
Hypothesis mf : measurable_fun setT f.
Hypothesis nd_g : β x, nondecreasing_seq (g^~x).
Hypothesis gf : β x, EFin \o g^~x --> f x.
Local Open Scope ereal_scope.
Lemma nd_ge0_integral_lim : \int f x 'd mu [x] = lim (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)[.
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 β
β 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.
Variables (T : measurableType) (R : realType) (D : set T) (mD : measurable D).
Variables (f : T β \bar R) (mf : measurable_fun D f).
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 Γ (x \in A n k)%:R +
n%:R Γ (x \in B n)%:R.
technical properties of the sets A and B
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 β
x \in A n i = false.
Let fgen_A0 n x (i : 'I_(n Γ 2 ^ n)) : (n%:R%:E β€ f x)%E β
x \in A n i = false.
Let disj_A0 x n (i k : 'I_(n Γ 2 ^ n)) : i != k β
x \in A n k β (x \in A n i) = false.
Arguments disj_A0 {x n i} k.
Let mB n : measurable (B n).
Let foo_B1 x n : D x β f x = +oo%E β x \in B n.
Let f0_B0 x n : f x = 0%:E β n != 0%N β (x \in B n) = false.
Let fgtn_B0 x n : (f x < n%:R%:E)%E β (x \in B n) = false.
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 β
\β n \near \oo, approx n x != 0.
Let f_ub_approx n x : (f x < n%:R%:E)%E β
approx n x == 0 β¨ β 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_A0 x n k : Β¬ D x β (x \in A n k) = false.
Let notinD_B0 x n : Β¬ D x β (x \in B n) = false.
Lemma nd_approx : nondecreasing_seq approx.
Lemma cvg_approx x (f0 : β x, D x β (0 β€ f x)%E) : D x β
(f x < +oo)%E β (approx^~ x) --> fine (f x).
Lemma le_approx k x (f0 : β x, (0 β€ f x)%E) : D x β
((approx k x)%:E β€ f x)%E.
Lemma dvg_approx x : D x β f x = +oo%E β Β¬ cvg (approx^~ x : _ β R^o).
Lemma ecvg_approx (f0 : β x, D x β (0 β€ f x)%E) x :
D x β EFin \o approx^~x --> 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 : β x, D x β (0 β€ f x)%E) x :
D x β EFin \o nnsfun_approx^~x --> f x.
Lemma nd_nnsfun_approx : nondecreasing_seq (nnsfun_approx : (T β R)^nat).
Lemma approximation : (β t, D t β (0 β€ f t)%E) β
β g : {nnsfun T >-> R}^nat, nondecreasing_seq (g : (T β R)^nat) β§
(β x, D x β EFin \o g^~x --> f x).
End approximation.
Section semi_linearity0.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (f1 f2 : T β \bar R).
Hypothesis f10 : β x, D x β 0 β€ f1 x.
Hypothesis mf1 : measurable_fun D f1.
Lemma ge0_integralM_EFin k : (0 β€ k)%R β
\int_ D (k%:E Γ f1 x) 'd mu[x] = k%:E Γ \int_ D (f1 x) 'd mu[x].
End semi_linearity0.
Section semi_linearity.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (f1 f2 : T β \bar R).
Hypothesis f10 : β x, D x β 0 β€ f1 x.
Hypothesis mf1 : measurable_fun D f1.
Hypothesis f20 : β x, D x β 0 β€ f2 x.
Hypothesis mf2 : measurable_fun D f2.
Lemma ge0_integralD : \int_ D ((f1 \+ f2) x) 'd mu[x] =
\int_ D (f1 x) 'd mu[x] + \int_ D (f2 x) 'd mu[x].
Lemma ge0_le_integral : (β x, D x β f1 x β€ f2 x) β
\int_ D (f1 x) 'd mu[x] β€ \int_ D (f2 x) 'd mu[x].
End semi_linearity.
Lemma emeasurable_funN (T : measurableType) (R : realType) D (f : T β \bar R) :
measurable D β measurable_fun D f β measurable_fun D (fun x β - f x)%E.
Section approximation_sfun.
Variables (T : measurableType) (R : realType) (f : T β \bar R).
Variables (D : set T) (mD : measurable D) (mf : measurable_fun D f).
Lemma approximation_sfun :
β g : {sfun T >-> R}^nat, (β x, D x β EFin \o g^~x --> f x).
End approximation_sfun.
Section emeasurable_fun.
Local Open Scope ereal_scope.
Variables (T : measurableType) (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_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 emeasurable_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_sum.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (D : set T) (I : Type).
Variables (f : I β (T β \bar R)) (mf : β n, measurable_fun D (f n)).
Lemma measurable_fun_sum s : measurable_fun D (fun x β \sum_(i <- s) f i x).
End measurable_fun_sum.
Section ge0_integral_sum.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (I : Type) (f : I β (T β \bar R)).
Hypothesis mf : β n, measurable_fun D (f n).
Hypothesis f0 : β n x, D x β 0 β€ f n x.
Lemma ge0_integral_sum (s : seq I) :
\int_ D (\sum_(k <- s) f k x) 'd mu[x] =
\sum_(k <- s) \int_ D (f k x) 'd mu[x].
End ge0_integral_sum.
Section monotone_convergence_theorem.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (g' : (T β \bar R)^nat).
Hypothesis mg' : β n, measurable_fun D (g' n).
Hypothesis g'0 : β n x, D x β 0 β€ g' n x.
Hypothesis nd_g' : β x, D x β nondecreasing_seq (g'^~ x).
Let f' := fun x β lim (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 β lim (g^~ x).
Let is_cvg_g t : cvg (g^~ t).
Let is_cvg_g2 n t : cvg (EFin \o (g2 n ^~ t)).
Let nd_max_g2 : nondecreasing_seq (max_g2 : (T β R)^nat).
Let is_cvg_max_g2 t : cvg (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 : lim (EFin \o max_g2 ^~ t) β€ f t.
Let lim_g2_max_g2 t n : lim (EFin\o g2 n ^~ t) β€ lim (EFin \o max_g2 ^~ t).
Let cvg_max_g2_f t : EFin \o max_g2 ^~ t --> f t.
Lemma monotone_convergence :
\int_ D (f' x) 'd mu[x] = lim (fun n β \int_ D (g' n x) 'd mu[x]).
Lemma cvg_monotone_convergence :
(fun n β \int_ D (g' n x) 'd mu[x]) --> \int_ D (f' x) 'd mu[x].
End monotone_convergence_theorem.
Section integral_series.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType).
Variables (mu : {measure set T β \bar R}) (D : set T) (mD : measurable D).
Variable f : (T β \bar R)^nat.
Hypothesis mf : β n, measurable_fun D (f n).
Hypothesis f0 : β n x, D x β 0 β€ f n x.
Lemma integral_sum : \int_ D (\sum_(n <oo) f n x) 'd mu[x] =
\sum_(n <oo) (\int_ D (f n x) 'd mu[x]).
End integral_series.
Let trivIsetA n : trivIset setT (A n).
Let f0_A0 n (i : 'I_(n Γ 2 ^ n)) x : f x = 0%:E β i != O :> nat β
x \in A n i = false.
Let fgen_A0 n x (i : 'I_(n Γ 2 ^ n)) : (n%:R%:E β€ f x)%E β
x \in A n i = false.
Let disj_A0 x n (i k : 'I_(n Γ 2 ^ n)) : i != k β
x \in A n k β (x \in A n i) = false.
Arguments disj_A0 {x n i} k.
Let mB n : measurable (B n).
Let foo_B1 x n : D x β f x = +oo%E β x \in B n.
Let f0_B0 x n : f x = 0%:E β n != 0%N β (x \in B n) = false.
Let fgtn_B0 x n : (f x < n%:R%:E)%E β (x \in B n) = false.
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 β
\β n \near \oo, approx n x != 0.
Let f_ub_approx n x : (f x < n%:R%:E)%E β
approx n x == 0 β¨ β 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_A0 x n k : Β¬ D x β (x \in A n k) = false.
Let notinD_B0 x n : Β¬ D x β (x \in B n) = false.
Lemma nd_approx : nondecreasing_seq approx.
Lemma cvg_approx x (f0 : β x, D x β (0 β€ f x)%E) : D x β
(f x < +oo)%E β (approx^~ x) --> fine (f x).
Lemma le_approx k x (f0 : β x, (0 β€ f x)%E) : D x β
((approx k x)%:E β€ f x)%E.
Lemma dvg_approx x : D x β f x = +oo%E β Β¬ cvg (approx^~ x : _ β R^o).
Lemma ecvg_approx (f0 : β x, D x β (0 β€ f x)%E) x :
D x β EFin \o approx^~x --> 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 : β x, D x β (0 β€ f x)%E) x :
D x β EFin \o nnsfun_approx^~x --> f x.
Lemma nd_nnsfun_approx : nondecreasing_seq (nnsfun_approx : (T β R)^nat).
Lemma approximation : (β t, D t β (0 β€ f t)%E) β
β g : {nnsfun T >-> R}^nat, nondecreasing_seq (g : (T β R)^nat) β§
(β x, D x β EFin \o g^~x --> f x).
End approximation.
Section semi_linearity0.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (f1 f2 : T β \bar R).
Hypothesis f10 : β x, D x β 0 β€ f1 x.
Hypothesis mf1 : measurable_fun D f1.
Lemma ge0_integralM_EFin k : (0 β€ k)%R β
\int_ D (k%:E Γ f1 x) 'd mu[x] = k%:E Γ \int_ D (f1 x) 'd mu[x].
End semi_linearity0.
Section semi_linearity.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (f1 f2 : T β \bar R).
Hypothesis f10 : β x, D x β 0 β€ f1 x.
Hypothesis mf1 : measurable_fun D f1.
Hypothesis f20 : β x, D x β 0 β€ f2 x.
Hypothesis mf2 : measurable_fun D f2.
Lemma ge0_integralD : \int_ D ((f1 \+ f2) x) 'd mu[x] =
\int_ D (f1 x) 'd mu[x] + \int_ D (f2 x) 'd mu[x].
Lemma ge0_le_integral : (β x, D x β f1 x β€ f2 x) β
\int_ D (f1 x) 'd mu[x] β€ \int_ D (f2 x) 'd mu[x].
End semi_linearity.
Lemma emeasurable_funN (T : measurableType) (R : realType) D (f : T β \bar R) :
measurable D β measurable_fun D f β measurable_fun D (fun x β - f x)%E.
Section approximation_sfun.
Variables (T : measurableType) (R : realType) (f : T β \bar R).
Variables (D : set T) (mD : measurable D) (mf : measurable_fun D f).
Lemma approximation_sfun :
β g : {sfun T >-> R}^nat, (β x, D x β EFin \o g^~x --> f x).
End approximation_sfun.
Section emeasurable_fun.
Local Open Scope ereal_scope.
Variables (T : measurableType) (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_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 emeasurable_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_sum.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (D : set T) (I : Type).
Variables (f : I β (T β \bar R)) (mf : β n, measurable_fun D (f n)).
Lemma measurable_fun_sum s : measurable_fun D (fun x β \sum_(i <- s) f i x).
End measurable_fun_sum.
Section ge0_integral_sum.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (I : Type) (f : I β (T β \bar R)).
Hypothesis mf : β n, measurable_fun D (f n).
Hypothesis f0 : β n x, D x β 0 β€ f n x.
Lemma ge0_integral_sum (s : seq I) :
\int_ D (\sum_(k <- s) f k x) 'd mu[x] =
\sum_(k <- s) \int_ D (f k x) 'd mu[x].
End ge0_integral_sum.
Section monotone_convergence_theorem.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (g' : (T β \bar R)^nat).
Hypothesis mg' : β n, measurable_fun D (g' n).
Hypothesis g'0 : β n x, D x β 0 β€ g' n x.
Hypothesis nd_g' : β x, D x β nondecreasing_seq (g'^~ x).
Let f' := fun x β lim (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 β lim (g^~ x).
Let is_cvg_g t : cvg (g^~ t).
Let is_cvg_g2 n t : cvg (EFin \o (g2 n ^~ t)).
Let nd_max_g2 : nondecreasing_seq (max_g2 : (T β R)^nat).
Let is_cvg_max_g2 t : cvg (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 : lim (EFin \o max_g2 ^~ t) β€ f t.
Let lim_g2_max_g2 t n : lim (EFin\o g2 n ^~ t) β€ lim (EFin \o max_g2 ^~ t).
Let cvg_max_g2_f t : EFin \o max_g2 ^~ t --> f t.
Lemma monotone_convergence :
\int_ D (f' x) 'd mu[x] = lim (fun n β \int_ D (g' n x) 'd mu[x]).
Lemma cvg_monotone_convergence :
(fun n β \int_ D (g' n x) 'd mu[x]) --> \int_ D (f' x) 'd mu[x].
End monotone_convergence_theorem.
Section integral_series.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType).
Variables (mu : {measure set T β \bar R}) (D : set T) (mD : measurable D).
Variable f : (T β \bar R)^nat.
Hypothesis mf : β n, measurable_fun D (f n).
Hypothesis f0 : β n x, D x β 0 β€ f n x.
Lemma integral_sum : \int_ D (\sum_(n <oo) f n x) 'd mu[x] =
\sum_(n <oo) (\int_ D (f n x) 'd mu[x]).
End integral_series.
generalization of ge0_integralM_EFin to a constant potentially +oo
using the monotone convergence theorem
Section ge0_integralM.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (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_integralM (k : \bar R) : (β x, D x β 0 β€ f x) β
0 β€ k β \int_ D (k Γ f x)%E 'd mu[x] = k Γ \int_ D (f x) 'd mu[x].
End ge0_integralM.
Section fatou.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (f : (T β \bar R)^nat).
Hypothesis mf : β n, measurable_fun D (f n).
Hypothesis f0 : β n x, D x β 0 β€ f n x.
Lemma fatou : \int_ D (elim_inf (f^~ x)) 'd mu[x] β€
elim_inf (fun n β \int_ D (f n x) 'd mu[x]).
End fatou.
Section integralN.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Lemma integralN D (f : T β \bar R) :
\int_ D (f^\+ x) 'd mu[x] +? (- \int_ D (f^\- x) 'd mu[x]) β
\int_ D ((-%E \o f) x) 'd mu[x] = - \int_ D (f x) 'd mu[x].
Lemma integral_ge0N (D : set T) (f : T β \bar R) :
(β x, D x β 0 β€ f x) β
\int_ D ((-%E \o f) x) 'd mu[x] = - \int_ D (f x) 'd mu[x].
End integralN.
Section integral_cst.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (f : T β \bar R) (D : set T) (mD : measurable D).
Lemma sintegral_cst (x : {nonneg R}) :
sintegral mu (cst x%:nngnum \_ D) = x%:nngnum%:E Γ mu D.
Lemma integral_cst (r : R) : \int_ D ((EFin \o cst r) x) 'd mu[x] = r%:E Γ mu D.
Lemma integral_cst_pinfty : mu D != 0 β \int_ D ((cst +oo) x) 'd mu[x] = +oo.
End integral_cst.
Section integral_ind.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D).
Lemma integral_indic (E : set T) : measurable E β
\int_ D ((EFin \o \1_E) x) 'd mu[x] = mu (E `&` D).
End integral_ind.
Section subset_integral.
Local Open Scope ereal_scope.
Variables (T : measurableType) (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 β
(β x, (A `|` B) x β 0 β€ f x) β [disjoint A & B] β
\int_ (A `|` B) (f x) 'd mu[x] = \int_ A (f x) 'd mu[x] + \int_ B (f x) 'd mu[x].
Lemma subset_integral (A B : set T) (mA : measurable A) (mB : measurable B)
(f : T β \bar R) : measurable_fun B f β (β x, B x β 0 β€ f x) β
A `<=` B β \int_ A (f x) 'd mu[x] β€ \int_ B (f x) 'd mu[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)%E]) β€ \int_ D `|g x| 'd mu[x].
End subset_integral.
Section Rintegral.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Definition Rintegral (D : set T) (f : T β \bar R) :=
fine (\int_ D (f x) 'd mu[x]).
End Rintegral.
Section integrable.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D).
Implicit Type f : T β \bar R.
Definition integrable f :=
measurable_fun D f β§ (\int_ D `|f x| 'd mu[x] < +oo).
Lemma eq_integrable f1 f2 : {in D, f1 =1 f2} β
integrable f1 β integrable f2.
Lemma le_integrable f1 f2 : measurable_fun D f1 β
(β x, D x β `|f1 x| β€ `|f2 x|) β integrable f2 β integrable f1.
Lemma integrableN f : integrable f β integrable (-%E \o f).
Lemma integrableK (k : R) f : integrable f β integrable (fun x β k%:E Γ f x).
Lemma integrableD f1 f2 : integrable f1 β integrable f2 β integrable (f1 \+ f2).
Lemma integrableB f1 f2 : integrable f1 β integrable f2 β
integrable (f1 \- f2).
Lemma integrable_add_def f : integrable f β
\int_ D (f^\+ x) 'd mu[x] +? - \int_ D (f^\- x) 'd mu[x].
Lemma integrable_funenng f : integrable f β integrable f^\+.
Lemma integrable_funennp f : integrable f β integrable f^\-.
Lemma integral_funennp_lt_pinfty f : integrable f β
\int_ D (f^\- x) 'd mu[x] < +oo.
Lemma integral_funenng_lt_pinfty f : integrable f β
\int_ D (f^\+ x) 'd mu[x] < +oo.
End integrable.
Notation "mu .-integrable" := (integrable mu) : type_scope.
Section integrable_lemmas.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
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 {T R mu D} f.
Section integrable_ae.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (f : T β \bar R).
Hypotheses fint : mu.-integrable D f.
Lemma integrable_ae : {ae mu, β x, D x β f x \is a fin_num}.
End integrable_ae.
Section linearityM.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (f : T β \bar R).
Hypothesis intf : mu.-integrable D f.
Lemma integralM r : \int_ D (r%:E Γ f x) 'd mu[x] = r%:E Γ \int_ D (f x) 'd mu[x].
End linearityM.
Section linearity.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (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.
Lemma integralD_EFin :
\int_ D ((g1 \+ g2) x) 'd mu[x] =
\int_ D (g1 x) 'd mu[x] + \int_ D (g2 x) 'd mu[x].
End linearity.
Lemma integralB_EFin (R : realType) (T : measurableType)
(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_ D ((f1 x)%:E - (f2 x)%:E) 'd mu[x] =
(\int_ D ((EFin \o f1) x) 'd mu[x] - \int_ D ((EFin \o f2) x) 'd mu[x]))%E.
Lemma le_abse_integral (T : measurableType) (R : realType)
(mu : {measure set T β \bar R}) (D : set T) (f : T β \bar R)
(mD : measurable D) : measurable_fun D f β
(`| \int_ D (f x) 'd mu[x]| β€ \int_ D `|f x| 'd mu[x])%E.
Section integral_indic.
Variables (T : measurableType) (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_ (E `&` D) (f x) 'd mu[x] = \int_ E f x Γ (\1_D x)%:E 'd mu[x])%E.
Lemma integralEindic (D : set T) (mD : measurable D) (f : T β \bar R) :
(\int_ D (f x) 'd mu[x] = \int_ D f x Γ (\1_D x)%:E 'd mu[x])%E.
End integral_indic.
Section ae_eq.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variable D : set T.
Implicit Types f g h i : T β \bar R.
Definition ae_eq f g := {ae mu, β x, D x β f x = g x}.
Lemma ae_eq_comp (j : \bar R β \bar R) f g :
ae_eq f g β ae_eq (j \o f) (j \o g).
Lemma ae_eq_funenng_funennp f g : ae_eq f g β ae_eq f^\+ g^\+ β§ ae_eq f^\- g^\-.
Lemma ae_eq_sym f g : ae_eq f g β ae_eq g f.
Lemma ae_eq_trans f g h : ae_eq f g β ae_eq g h β ae_eq f h.
Lemma ae_eq_sub f g h i : ae_eq f g β ae_eq h i β ae_eq (f \- h) (g \- i).
Lemma ae_eq_mul2r f g h : ae_eq f g β ae_eq (f \* h) (g \* h).
Lemma ae_eq_mul2l f g h : ae_eq f g β ae_eq (h \* f) (h \* g).
Lemma ae_eq_mul1l f g : ae_eq f (cst 1) β ae_eq g (g \* f).
Lemma ae_eq_mul f g h : ae_eq f g β ae_eq (f \* h) (g \* h).
Lemma ae_eq_abse f g : ae_eq f g β ae_eq (abse \o f) (abse \o g).
End ae_eq.
Section ae_eq_integral.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Let ae_eq_integral_abs_bounded (D : set T) (mD : measurable D) (f : T β \bar R)
M : measurable_fun D f β (β x, D x β `|f x| β€ M%:E) β
ae_eq D f (cst 0) β \int_ D `|f x|%E 'd mu[x] = 0.
Lemma ae_eq_integral_abs (D : set T) (mD : measurable D) (f : T β \bar R) :
measurable_fun D f β \int_ D `|f x| 'd mu[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_ N `|f x| 'd mu[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 negligible_integral (D N : set T) (f : T β \bar R) :
measurable N β measurable D β measurable_fun D f β
(β x, D x β 0 β€ f x) β
mu N = 0 β \int_ D (f x) 'd mu[x] = \int_ (D `\` N) (f x) 'd mu[x].
Lemma ge0_ae_eq_integral (D : set T) (f g : T β \bar R) :
measurable D β measurable_fun D f β measurable_fun D g β
(β x, D x β 0 β€ f x) β (β x, D x β 0 β€ g x) β
ae_eq D f g β \int_ D (f x) 'd mu[x] = \int_ D (g x) 'd mu[x].
Lemma ae_eq_integral (D : set T) (f g : 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.
Section ae_measurable_fun.
Variables (T : measurableType) (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.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (f1 f2 : T β \bar R).
Hypotheses (if1 : mu.-integrable D f1) (if2 : mu.-integrable D f2).
Lemma integralD : \int_ D ((f1 \+ f2) x) 'd mu[x] =
\int_ D (f1 x) 'd mu[x] + \int_ D (f2 x) 'd mu[x].
End integralD.
Section integralB.
Local Open Scope ereal_scope.
Variables (T : measurableType) (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_ D ((f1 \- f2) x) 'd mu[x] =
\int_ D (f1 x) 'd mu[x] - \int_ D (f2 x) 'd mu[x].
End integralB.
Section dominated_convergence_lemma.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (f_ : (T β \bar R)^nat).
Variables (f : T β \bar R) (g : T β \bar R).
Hypothesis mf_ : β n, measurable_fun D (f_ n).
Hypothesis f_f : β x, D x β f_ ^~ x --> f x.
Hypothesis fing : β x, D x β g x \is a fin_num.
Hypothesis ig : mu.-integrable D g.
Hypothesis absfg : β n x, D x β `|f_ n x| β€ g x.
Let g0 x : D x β 0 β€ g x.
Let mf : measurable_fun D f.
Let g_ n x := `|f_ n x - f x|.
Let cvg_g_ x : D x β g_ ^~ x --> 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.
End dominated_convergence_lemma.
Arguments dominated_integrable {T R mu D} _ f_ f g.
Section dominated_convergence_theorem.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D).
Variables (f_ : (T β \bar R)^nat) (f : T β \bar R) (g : T β \bar R).
Hypothesis mf_ : β n, measurable_fun D (f_ n).
Hypothesis mf : measurable_fun D f.
Hypothesis f_f : {ae mu, β x, D x β f_ ^~ x --> f x}.
Hypothesis ig : mu.-integrable D g.
Hypothesis f_g : {ae mu, β 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,
(fun n β \int_ D (g_ n x) 'd mu[x]) --> 0 &
(fun n β \int_ D (f_ n x) 'd mu[x]) --> \int_ D (f x) 'd mu[x]].
End dominated_convergence_theorem.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (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_integralM (k : \bar R) : (β x, D x β 0 β€ f x) β
0 β€ k β \int_ D (k Γ f x)%E 'd mu[x] = k Γ \int_ D (f x) 'd mu[x].
End ge0_integralM.
Section fatou.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (f : (T β \bar R)^nat).
Hypothesis mf : β n, measurable_fun D (f n).
Hypothesis f0 : β n x, D x β 0 β€ f n x.
Lemma fatou : \int_ D (elim_inf (f^~ x)) 'd mu[x] β€
elim_inf (fun n β \int_ D (f n x) 'd mu[x]).
End fatou.
Section integralN.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Lemma integralN D (f : T β \bar R) :
\int_ D (f^\+ x) 'd mu[x] +? (- \int_ D (f^\- x) 'd mu[x]) β
\int_ D ((-%E \o f) x) 'd mu[x] = - \int_ D (f x) 'd mu[x].
Lemma integral_ge0N (D : set T) (f : T β \bar R) :
(β x, D x β 0 β€ f x) β
\int_ D ((-%E \o f) x) 'd mu[x] = - \int_ D (f x) 'd mu[x].
End integralN.
Section integral_cst.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (f : T β \bar R) (D : set T) (mD : measurable D).
Lemma sintegral_cst (x : {nonneg R}) :
sintegral mu (cst x%:nngnum \_ D) = x%:nngnum%:E Γ mu D.
Lemma integral_cst (r : R) : \int_ D ((EFin \o cst r) x) 'd mu[x] = r%:E Γ mu D.
Lemma integral_cst_pinfty : mu D != 0 β \int_ D ((cst +oo) x) 'd mu[x] = +oo.
End integral_cst.
Section integral_ind.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D).
Lemma integral_indic (E : set T) : measurable E β
\int_ D ((EFin \o \1_E) x) 'd mu[x] = mu (E `&` D).
End integral_ind.
Section subset_integral.
Local Open Scope ereal_scope.
Variables (T : measurableType) (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 β
(β x, (A `|` B) x β 0 β€ f x) β [disjoint A & B] β
\int_ (A `|` B) (f x) 'd mu[x] = \int_ A (f x) 'd mu[x] + \int_ B (f x) 'd mu[x].
Lemma subset_integral (A B : set T) (mA : measurable A) (mB : measurable B)
(f : T β \bar R) : measurable_fun B f β (β x, B x β 0 β€ f x) β
A `<=` B β \int_ A (f x) 'd mu[x] β€ \int_ B (f x) 'd mu[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)%E]) β€ \int_ D `|g x| 'd mu[x].
End subset_integral.
Section Rintegral.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Definition Rintegral (D : set T) (f : T β \bar R) :=
fine (\int_ D (f x) 'd mu[x]).
End Rintegral.
Section integrable.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D).
Implicit Type f : T β \bar R.
Definition integrable f :=
measurable_fun D f β§ (\int_ D `|f x| 'd mu[x] < +oo).
Lemma eq_integrable f1 f2 : {in D, f1 =1 f2} β
integrable f1 β integrable f2.
Lemma le_integrable f1 f2 : measurable_fun D f1 β
(β x, D x β `|f1 x| β€ `|f2 x|) β integrable f2 β integrable f1.
Lemma integrableN f : integrable f β integrable (-%E \o f).
Lemma integrableK (k : R) f : integrable f β integrable (fun x β k%:E Γ f x).
Lemma integrableD f1 f2 : integrable f1 β integrable f2 β integrable (f1 \+ f2).
Lemma integrableB f1 f2 : integrable f1 β integrable f2 β
integrable (f1 \- f2).
Lemma integrable_add_def f : integrable f β
\int_ D (f^\+ x) 'd mu[x] +? - \int_ D (f^\- x) 'd mu[x].
Lemma integrable_funenng f : integrable f β integrable f^\+.
Lemma integrable_funennp f : integrable f β integrable f^\-.
Lemma integral_funennp_lt_pinfty f : integrable f β
\int_ D (f^\- x) 'd mu[x] < +oo.
Lemma integral_funenng_lt_pinfty f : integrable f β
\int_ D (f^\+ x) 'd mu[x] < +oo.
End integrable.
Notation "mu .-integrable" := (integrable mu) : type_scope.
Section integrable_lemmas.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
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 {T R mu D} f.
Section integrable_ae.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (f : T β \bar R).
Hypotheses fint : mu.-integrable D f.
Lemma integrable_ae : {ae mu, β x, D x β f x \is a fin_num}.
End integrable_ae.
Section linearityM.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (f : T β \bar R).
Hypothesis intf : mu.-integrable D f.
Lemma integralM r : \int_ D (r%:E Γ f x) 'd mu[x] = r%:E Γ \int_ D (f x) 'd mu[x].
End linearityM.
Section linearity.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (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.
Lemma integralD_EFin :
\int_ D ((g1 \+ g2) x) 'd mu[x] =
\int_ D (g1 x) 'd mu[x] + \int_ D (g2 x) 'd mu[x].
End linearity.
Lemma integralB_EFin (R : realType) (T : measurableType)
(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_ D ((f1 x)%:E - (f2 x)%:E) 'd mu[x] =
(\int_ D ((EFin \o f1) x) 'd mu[x] - \int_ D ((EFin \o f2) x) 'd mu[x]))%E.
Lemma le_abse_integral (T : measurableType) (R : realType)
(mu : {measure set T β \bar R}) (D : set T) (f : T β \bar R)
(mD : measurable D) : measurable_fun D f β
(`| \int_ D (f x) 'd mu[x]| β€ \int_ D `|f x| 'd mu[x])%E.
Section integral_indic.
Variables (T : measurableType) (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_ (E `&` D) (f x) 'd mu[x] = \int_ E f x Γ (\1_D x)%:E 'd mu[x])%E.
Lemma integralEindic (D : set T) (mD : measurable D) (f : T β \bar R) :
(\int_ D (f x) 'd mu[x] = \int_ D f x Γ (\1_D x)%:E 'd mu[x])%E.
End integral_indic.
Section ae_eq.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variable D : set T.
Implicit Types f g h i : T β \bar R.
Definition ae_eq f g := {ae mu, β x, D x β f x = g x}.
Lemma ae_eq_comp (j : \bar R β \bar R) f g :
ae_eq f g β ae_eq (j \o f) (j \o g).
Lemma ae_eq_funenng_funennp f g : ae_eq f g β ae_eq f^\+ g^\+ β§ ae_eq f^\- g^\-.
Lemma ae_eq_sym f g : ae_eq f g β ae_eq g f.
Lemma ae_eq_trans f g h : ae_eq f g β ae_eq g h β ae_eq f h.
Lemma ae_eq_sub f g h i : ae_eq f g β ae_eq h i β ae_eq (f \- h) (g \- i).
Lemma ae_eq_mul2r f g h : ae_eq f g β ae_eq (f \* h) (g \* h).
Lemma ae_eq_mul2l f g h : ae_eq f g β ae_eq (h \* f) (h \* g).
Lemma ae_eq_mul1l f g : ae_eq f (cst 1) β ae_eq g (g \* f).
Lemma ae_eq_mul f g h : ae_eq f g β ae_eq (f \* h) (g \* h).
Lemma ae_eq_abse f g : ae_eq f g β ae_eq (abse \o f) (abse \o g).
End ae_eq.
Section ae_eq_integral.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Let ae_eq_integral_abs_bounded (D : set T) (mD : measurable D) (f : T β \bar R)
M : measurable_fun D f β (β x, D x β `|f x| β€ M%:E) β
ae_eq D f (cst 0) β \int_ D `|f x|%E 'd mu[x] = 0.
Lemma ae_eq_integral_abs (D : set T) (mD : measurable D) (f : T β \bar R) :
measurable_fun D f β \int_ D `|f x| 'd mu[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_ N `|f x| 'd mu[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 negligible_integral (D N : set T) (f : T β \bar R) :
measurable N β measurable D β measurable_fun D f β
(β x, D x β 0 β€ f x) β
mu N = 0 β \int_ D (f x) 'd mu[x] = \int_ (D `\` N) (f x) 'd mu[x].
Lemma ge0_ae_eq_integral (D : set T) (f g : T β \bar R) :
measurable D β measurable_fun D f β measurable_fun D g β
(β x, D x β 0 β€ f x) β (β x, D x β 0 β€ g x) β
ae_eq D f g β \int_ D (f x) 'd mu[x] = \int_ D (g x) 'd mu[x].
Lemma ae_eq_integral (D : set T) (f g : 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.
Section ae_measurable_fun.
Variables (T : measurableType) (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.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (f1 f2 : T β \bar R).
Hypotheses (if1 : mu.-integrable D f1) (if2 : mu.-integrable D f2).
Lemma integralD : \int_ D ((f1 \+ f2) x) 'd mu[x] =
\int_ D (f1 x) 'd mu[x] + \int_ D (f2 x) 'd mu[x].
End integralD.
Section integralB.
Local Open Scope ereal_scope.
Variables (T : measurableType) (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_ D ((f1 \- f2) x) 'd mu[x] =
\int_ D (f1 x) 'd mu[x] - \int_ D (f2 x) 'd mu[x].
End integralB.
Section dominated_convergence_lemma.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D) (f_ : (T β \bar R)^nat).
Variables (f : T β \bar R) (g : T β \bar R).
Hypothesis mf_ : β n, measurable_fun D (f_ n).
Hypothesis f_f : β x, D x β f_ ^~ x --> f x.
Hypothesis fing : β x, D x β g x \is a fin_num.
Hypothesis ig : mu.-integrable D g.
Hypothesis absfg : β n x, D x β `|f_ n x| β€ g x.
Let g0 x : D x β 0 β€ g x.
Let mf : measurable_fun D f.
Let g_ n x := `|f_ n x - f x|.
Let cvg_g_ x : D x β g_ ^~ x --> 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.
End dominated_convergence_lemma.
Arguments dominated_integrable {T R mu D} _ f_ f g.
Section dominated_convergence_theorem.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType) (mu : {measure set T β \bar R}).
Variables (D : set T) (mD : measurable D).
Variables (f_ : (T β \bar R)^nat) (f : T β \bar R) (g : T β \bar R).
Hypothesis mf_ : β n, measurable_fun D (f_ n).
Hypothesis mf : measurable_fun D f.
Hypothesis f_f : {ae mu, β x, D x β f_ ^~ x --> f x}.
Hypothesis ig : mu.-integrable D g.
Hypothesis f_g : {ae mu, β 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,
(fun n β \int_ D (g_ n x) 'd mu[x]) --> 0 &
(fun n β \int_ D (f_ n x) 'd mu[x]) --> \int_ D (f x) 'd mu[x]].
End dominated_convergence_theorem.
Section measurable_section.
Variables (T1 T2 : measurableType) (R : realType).
Implicit Types (A : set (T1 Γ T2)).
Lemma mem_set_pair1 x y A :
(y \in [set y' | (x, y') \in A]) = ((x, y) \in A).
Lemma mem_set_pair2 x y A :
(x \in [set x' | (x', y) \in A]) = ((x, y) \in A).
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.
Variables (T1 T2 : measurableType) (R : realType).
Implicit Types A : set (T1 Γ T2).
Section xsection.
Variables (pt2 : T2) (m2 : {measure set T2 β \bar R}).
Let phi A := m2 \o xsection A.
Let B := [set A | measurable A β§ measurable_fun setT (phi A)].
Lemma xsection_ndseq_closed : ndseq_closed B.
End xsection.
Section ysection.
Variables (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.
Variables (T1 T2 : measurableType) (R : realType).
Implicit Types A : set (T1 Γ T2).
Section xsection.
Variables (m2' : {measure set T2 β \bar R}).
Variables (D : set T2) (mD : measurable D).
Let m2 := measure_restr m2' mD.
Let phi A := m2 \o xsection A.
Let B := [set A | measurable A β§ measurable_fun setT (phi A)].
Lemma measurable_prod_subset_xsection
(m2_bounded : β M, β X, measurable X β (m2 X < M%:E)%E) :
@measurable (prod_measurableType T1 T2) `<=` B.
End xsection.
Section ysection.
Variables (m1' : {measure set T1 β \bar R}).
Variables (D : set T1) (mD : measurable D).
Let m1 := measure_restr m1' mD.
Let psi A := m1 \o ysection A.
Let B := [set A | measurable A β§ measurable_fun setT (psi A)].
Lemma measurable_prod_subset_ysection
(m1_bounded : β M, β X, measurable X β (m1 X < M%:E)%E) :
@measurable (prod_measurableType T1 T2) `<=` B.
End ysection.
End measurable_prod_subset.
Section measurable_fun_xsection.
Variables (T1 T2 : measurableType) (R : realType).
Variables (m2 : {measure set T2 β \bar R}).
Hypothesis sf_m2 : sigma_finite setT m2.
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 : A \in measurable β measurable_fun setT (phi A).
End measurable_fun_xsection.
Section measurable_fun_ysection.
Variables (T1 T2 : measurableType) (R : realType).
Variables (m1 : {measure set T1 β \bar R}).
Hypothesis sf_m1 : sigma_finite setT m1.
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 : A \in measurable β measurable_fun setT (phi A).
End measurable_fun_ysection.
Section product_measure1.
Local Open Scope ereal_scope.
Variables (T1 T2 : measurableType) (R : realType).
Variables (m1 : {measure set T1 β \bar R}) (m2 : {measure set T2 β \bar R}).
Hypothesis (sm2 : sigma_finite setT m2).
Implicit Types A : set (T1 Γ T2).
Let m A := \int ((m2 \o xsection A) x) 'd m1[x].
Let m0 : m set0 = 0.
Let m_ge0 A : 0 β€ m A.
Let m_sigma_additive : semi_sigma_additive m.
Definition product_measure1 : {measure set (T1 Γ T2) β \bar R} :=
Measure.Pack _ (Measure.Axioms m0 m_ge0 m_sigma_additive).
End product_measure1.
Section product_measure1E.
Local Open Scope ereal_scope.
Variables (T1 T2 : measurableType) (R : realType).
Variables (m1 : {measure set T1 β \bar R}) (m2 : {measure set T2 β \bar R}).
Hypothesis (sm2 : sigma_finite setT m2).
Implicit Types A : set (T1 Γ T2).
Lemma product_measure1E (A1 : set T1) (A2 : set T2) :
measurable A1 β measurable A2 β
product_measure1 m1 sm2 (A1 `*` A2) = m1 A1 Γ m2 A2.
End product_measure1E.
Section product_measure_unique.
Local Open Scope ereal_scope.
Variables (T1 T2 : measurableType) (R : realType).
Variables (m1 : {measure set T1 β \bar R}) (m2 : {measure set T2 β \bar R}).
Hypotheses (sf_m1 : sigma_finite setT m1) (sf_m2 : sigma_finite setT m2).
Lemma product_measure_unique (m' : {measure set (T1 Γ T2) β \bar R}) :
(β A1 A2, measurable A1 β measurable A2 β m' (A1 `*` A2) = m1 A1 Γ m2 A2) β
β X : set (T1 Γ T2), measurable X β product_measure1 m1 sf_m2 X = m' X.
End product_measure_unique.
Section product_measure2.
Local Open Scope ereal_scope.
Variables (T1 T2 : measurableType) (R : realType).
Variables (m1 : {measure set T1 β \bar R}) (m2 : {measure set T2 β \bar R}).
Hypothesis (sm1 : sigma_finite setT m1).
Implicit Types A : set (T1 Γ T2).
Let m A := \int ((m1 \o ysection A) x) 'd m2[x].
Let m0 : m set0 = 0.
Definition product_measure2 : {measure set (T1 Γ T2) β \bar R} :=
Measure.Pack _ (Measure.Axioms m0 m_ge0 m2_sigma_additive).
End product_measure2.
Section product_measure2E.
Local Open Scope ereal_scope.
Variables (T1 T2 : measurableType) (R : realType).
Variables (m1 : {measure set T1 β \bar R}) (m2 : {measure set T2 β \bar R}).
Hypothesis sm1 : sigma_finite setT m1.
Lemma product_measure2E (A1 : set T1) (A2 : set T2)
(mA1 : measurable A1) (mA2 : measurable A2) :
product_measure2 m2 sm1 (A1 `*` A2) = m1 A1 Γ m2 A2.
End product_measure2E.
Section fubini_functions.
Local Open Scope ereal_scope.
Variables (T1 T2 : measurableType) (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 (f (x, y)) 'd m2[y].
Definition fubini_G y := \int (f (x, y)) 'd m1[x].
End fubini_functions.
Section fubini_tonelli.
Local Open Scope ereal_scope.
Variables (T1 T2 : measurableType) (R : realType).
Variables (m1 : {measure set T1 β \bar R}) (m2 : {measure set T2 β \bar R}).
Hypotheses (sf_m1 : sigma_finite setT m1) (sf_m2 : sigma_finite setT m2).
Let m : {measure set (T1 Γ T2) β \bar R} := product_measure1 m1 sf_m2.
Let m' : {measure set (T1 Γ T2) β \bar R} := product_measure2 m2 sf_m1.
Section indic_fubini_tonelli.
Variables (A : set (T1 Γ T2)) (mA : measurable A).
Implicit Types A : set (T1 Γ T2).
Let f : (prod_measurableType 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.
par definition de la mesure produit
Let mE : m A = \int (F x) 'd m1[x].
Lemma indic_fubini_tonelli1 :
\int ((EFin \o f) z) 'd m[z] = \int (F x) 'd m1[x].
Lemma indic_fubini_tonelli2 :
\int ((EFin \o f) z) 'd m'[z] = \int (G y) 'd m2[y].
Lemma indic_fubini_tonelli : \int (F x) 'd m1[x] = \int (G y) 'd m2[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 <- fset_set (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 <- fset_set (range f)) k%:E Γ m1 (ysection (f @^-1` [set k]) y)).
Lemma sfun_measurable_fun_fubini_tonelli_G : measurable_fun setT G.
Lemma sfun_fubini_tonelli1 : \int ((EFin \o f) z) 'd m[z] = \int (F x) 'd m1[x].
Lemma sfun_fubini_tonelli2 : \int ((EFin \o f) z) 'd m'[z] = \int (G y) 'd m2[y].
Lemma sfun_fubini_tonelli :
\int ((EFin \o f) z) 'd m[z] = \int ((EFin \o f) z) 'd m'[z].
End sfun_fubini_tonelli.
Section fubini_tonelli.
Variable f : T1 Γ T2 β \bar R.
Hypothesis mf : measurable_fun setT f.
Hypothesis f0 : β 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 ((EFin \o g n) (x, y)) 'd m2[y].
Let G_ (g : {nnsfun T >-> R}^nat) n y := \int ((EFin \o g n) (x, y)) 'd m1[x].
Lemma measurable_fun_fubini_tonelli_F : measurable_fun setT F.
Lemma measurable_fun_fubini_tonelli_G : measurable_fun setT G.
Lemma fubini_tonelli1 : \int (f z) 'd m[z] = \int (F x) 'd m1[x].
Lemma fubini_tonelli2 : \int (f z) 'd m[z] = \int (G y) 'd m2[y].
End fubini_tonelli.
End fubini_tonelli.
Arguments fubini_tonelli1 {T1 T2 R m1 m2} sf_m2 f.
Arguments fubini_tonelli2 {T1 T2 R m1 m2} sf_m1 sf_m2 f.
Arguments measurable_fun_fubini_tonelli_F {T1 T2 R m2} sf_m2 f.
Arguments measurable_fun_fubini_tonelli_G {T1 T2 R m1} sf_m1 f.
Section fubini.
Local Open Scope ereal_scope.
Variables (T1 T2 : measurableType) (R : realType).
Variables (m1 : {measure set T1 β \bar R}) (m2 : {measure set T2 β \bar R}).
Hypotheses (sf_m1 : sigma_finite setT m1) (sf_m2 : sigma_finite setT m2).
Variable f : T1 Γ T2 β \bar R.
Hypothesis mf : measurable_fun setT f.
Let m : {measure set (T1 Γ T2) β \bar R} := product_measure1 m1 sf_m2.
Lemma fubini1a :
m.-integrable setT f β \int (\int `|f (x, y)| 'd m2[y]) 'd m1[x] < +oo.
Lemma fubini1b :
m.-integrable setT f β \int (\int `|f (x, y)| 'd m1[x]) 'd m2[y] < +oo.
Let measurable_fun1 : measurable_fun setT (fun x β \int `|f (x, y)| 'd m2[y]).
Let measurable_fun2 : measurable_fun setT (fun y β \int `|f (x, y)| 'd m1[x]).
Hypothesis imf : m.-integrable setT f.
Lemma ae_integrable1 :
{ae m1, β x, m2.-integrable setT (fun y β f (x, y))}.
Lemma ae_integrable2 :
{ae m2, β y, m1.-integrable setT (fun x β f (x, y))}.
Let F := fubini_F m2 f.
Let Fplus x := \int (f^\+ (x, y)) 'd m2[y].
Let Fminus x := \int (f^\- (x, y)) 'd m2[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 (f^\+ (x, y)) 'd m1[x].
Let Gminus y := \int (f^\- (x, y)) 'd m1[x].
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 (F x) 'd m1[x] = \int (f z) 'd m[z].
Lemma fubini2 : \int (G x) 'd m2[x] = \int (f z) 'd m[z].
Theorem Fubini :
\int (\int (f (x, y)) 'd m2[y]) 'd m1[x] = \int (\int (f (x, y)) 'd m1[x]) 'd m2[y].
End fubini.
Lemma indic_fubini_tonelli1 :
\int ((EFin \o f) z) 'd m[z] = \int (F x) 'd m1[x].
Lemma indic_fubini_tonelli2 :
\int ((EFin \o f) z) 'd m'[z] = \int (G y) 'd m2[y].
Lemma indic_fubini_tonelli : \int (F x) 'd m1[x] = \int (G y) 'd m2[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 <- fset_set (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 <- fset_set (range f)) k%:E Γ m1 (ysection (f @^-1` [set k]) y)).
Lemma sfun_measurable_fun_fubini_tonelli_G : measurable_fun setT G.
Lemma sfun_fubini_tonelli1 : \int ((EFin \o f) z) 'd m[z] = \int (F x) 'd m1[x].
Lemma sfun_fubini_tonelli2 : \int ((EFin \o f) z) 'd m'[z] = \int (G y) 'd m2[y].
Lemma sfun_fubini_tonelli :
\int ((EFin \o f) z) 'd m[z] = \int ((EFin \o f) z) 'd m'[z].
End sfun_fubini_tonelli.
Section fubini_tonelli.
Variable f : T1 Γ T2 β \bar R.
Hypothesis mf : measurable_fun setT f.
Hypothesis f0 : β 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 ((EFin \o g n) (x, y)) 'd m2[y].
Let G_ (g : {nnsfun T >-> R}^nat) n y := \int ((EFin \o g n) (x, y)) 'd m1[x].
Lemma measurable_fun_fubini_tonelli_F : measurable_fun setT F.
Lemma measurable_fun_fubini_tonelli_G : measurable_fun setT G.
Lemma fubini_tonelli1 : \int (f z) 'd m[z] = \int (F x) 'd m1[x].
Lemma fubini_tonelli2 : \int (f z) 'd m[z] = \int (G y) 'd m2[y].
End fubini_tonelli.
End fubini_tonelli.
Arguments fubini_tonelli1 {T1 T2 R m1 m2} sf_m2 f.
Arguments fubini_tonelli2 {T1 T2 R m1 m2} sf_m1 sf_m2 f.
Arguments measurable_fun_fubini_tonelli_F {T1 T2 R m2} sf_m2 f.
Arguments measurable_fun_fubini_tonelli_G {T1 T2 R m1} sf_m1 f.
Section fubini.
Local Open Scope ereal_scope.
Variables (T1 T2 : measurableType) (R : realType).
Variables (m1 : {measure set T1 β \bar R}) (m2 : {measure set T2 β \bar R}).
Hypotheses (sf_m1 : sigma_finite setT m1) (sf_m2 : sigma_finite setT m2).
Variable f : T1 Γ T2 β \bar R.
Hypothesis mf : measurable_fun setT f.
Let m : {measure set (T1 Γ T2) β \bar R} := product_measure1 m1 sf_m2.
Lemma fubini1a :
m.-integrable setT f β \int (\int `|f (x, y)| 'd m2[y]) 'd m1[x] < +oo.
Lemma fubini1b :
m.-integrable setT f β \int (\int `|f (x, y)| 'd m1[x]) 'd m2[y] < +oo.
Let measurable_fun1 : measurable_fun setT (fun x β \int `|f (x, y)| 'd m2[y]).
Let measurable_fun2 : measurable_fun setT (fun y β \int `|f (x, y)| 'd m1[x]).
Hypothesis imf : m.-integrable setT f.
Lemma ae_integrable1 :
{ae m1, β x, m2.-integrable setT (fun y β f (x, y))}.
Lemma ae_integrable2 :
{ae m2, β y, m1.-integrable setT (fun x β f (x, y))}.
Let F := fubini_F m2 f.
Let Fplus x := \int (f^\+ (x, y)) 'd m2[y].
Let Fminus x := \int (f^\- (x, y)) 'd m2[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 (f^\+ (x, y)) 'd m1[x].
Let Gminus y := \int (f^\- (x, y)) 'd m1[x].
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 (F x) 'd m1[x] = \int (f z) 'd m[z].
Lemma fubini2 : \int (G x) 'd m2[x] = \int (f z) 'd m[z].
Theorem Fubini :
\int (\int (f (x, y)) 'd m2[y]) 'd m1[x] = \int (\int (f (x, y)) 'd m1[x]) 'd m2[y].
End fubini.