Library mathcomp.analysis.lebesgue_integral
(* 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.
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.
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.
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 {mfun T >-> R} == type of real-valued measurable functions {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 \int[mu]_(x in D) f x == integral of the measurable function f over the domain D with measure mu \int[mu]_x f x := \int[mu]_(x in setT) f x dyadic_itv n k == the interval `[(k%:R * 2 ^- n), (k.+1%:R * 2 ^- n) [ approx D f == nondecreasing sequence of functions that approximates f over D using dyadic intervals Rintegral mu D f := fine (\int[mu]_(x in D) f x). mu.-integrable D f == f is measurable over D and the integral of f w.r.t. D is < +oo ae_eq D f g == f is equal to g almost everywhere m1 \x m2 == product measure over T1 * T2, m1 is a measure measure over T1, and m2 is a sigma finite measure over T2 m1 \x^ m2 == product measure over T1 * T2, m2 is a measure measure over T1, and m1 is a sigma finite measure over T2
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 [ 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.
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 {d} {aT : measurableType d} {rT : realType}
(f : {mfun aT >-> rT}) (Y : set rT) : measurable Y → measurable (f @^-1` Y).
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 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) :
(∀ 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 d 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 d (aT : measurableType d) (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 d 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 d aT rT (f \max 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.
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) :
(∀ 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 d (aT : measurableType d) (rT : realType).
Lemma sfun_subring_closed : subring_closed (@sfun d 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 {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 : T → [normedModType R of R^o]).
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).
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).
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).
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.
Context d (T : measurableType d) (R : realType).
Variables 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 {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 →
(∀ 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.
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).
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 {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 : T → [normedModType R of R^o]).
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).
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).
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).
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.
Context d (T : measurableType d) (R : realType).
Variables 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 {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 →
(∀ 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.
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.
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.
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 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 : ∀ 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) :
(∀ x, nondecreasing_seq (f ^~ x)) → cvg (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 : ∀ 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.
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 : ∀ 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.
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} | ∀ 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 : (∀ 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.
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 : (∀ x, D x → 0 ≤ f x) →
\int_(x in D) f x = nnintegral mu (f \_ D).
Lemma ge0_integralTE f : (∀ 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 :
(∀ x, D x → f x = 0) → \int_(x in D) f x = 0.
Lemma integral_ge0 D f : (∀ 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) :
(∀ A, measurable A → A `<=` D → m1 A = m2 A) →
[set sintegral m1 h | h in
[set h : {nnsfun T >-> R} | (∀ x, (h x)%:E ≤ (f \_ D) x)]] `<=`
[set sintegral m2 h | h in
[set h : {nnsfun T >-> R} | (∀ x, (h x)%:E ≤ (f \_ D) x)]].
Lemma eq_measure_integral m2 m1 (f : T → \bar R) :
(∀ 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 : ∀ 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[mu]_x f 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.
Context d (T : measurableType d) (R : realType).
Variables (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 × \1_(A n k) x + n%:R × \1_(B n) x.
(\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 : ∀ 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) :
(∀ x, nondecreasing_seq (f ^~ x)) → cvg (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 : ∀ 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.
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 : ∀ 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.
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} | ∀ 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 : (∀ 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.
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 : (∀ x, D x → 0 ≤ f x) →
\int_(x in D) f x = nnintegral mu (f \_ D).
Lemma ge0_integralTE f : (∀ 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 :
(∀ x, D x → f x = 0) → \int_(x in D) f x = 0.
Lemma integral_ge0 D f : (∀ 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) :
(∀ A, measurable A → A `<=` D → m1 A = m2 A) →
[set sintegral m1 h | h in
[set h : {nnsfun T >-> R} | (∀ x, (h x)%:E ≤ (f \_ D) x)]] `<=`
[set sintegral m2 h | h in
[set h : {nnsfun T >-> R} | (∀ x, (h x)%:E ≤ (f \_ D) x)]].
Lemma eq_measure_integral m2 m1 (f : T → \bar R) :
(∀ 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 : ∀ 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[mu]_x f 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.
Context d (T : measurableType d) (R : realType).
Variables (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 × \1_(A n k) x + n%:R × \1_(B n) x.
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 →
\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 →
\∀ 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_approx0 x n : ¬ D x → approx n x = 0 :> R.
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, 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 → ¬ 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.
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 : ∀ 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.
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 : ∀ 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[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 : (∀ 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 :
∃ g : {sfun T >-> R}^nat, (∀ x, D x → EFin \o g^~x --> 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 →
∃ 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 → ∃ 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 → ∃ 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)) :
(∀ 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 →
(∀ 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)) :
(∀ k x, 0 ≤ h k x) → (∀ 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 : ∀ n, measurable_fun D (f n).
Hypothesis f0 : ∀ 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 : ∀ n, measurable_fun D (f n).
Hypothesis f0 : ∀ 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' : ∀ 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[mu]_(x in D) (f' x) = lim (fun n ⇒ \int[mu]_(x in D) (g' n x)).
Lemma cvg_monotone_convergence :
(fun n ⇒ \int[mu]_(x in D) g' n x) --> \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 : ∀ n, measurable_fun D (f n).
Hypothesis f0 : ∀ 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.
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 →
\∀ 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_approx0 x n : ¬ D x → approx n x = 0 :> R.
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, 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 → ¬ 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.
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 : ∀ 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.
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 : ∀ 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[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 : (∀ 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 :
∃ g : {sfun T >-> R}^nat, (∀ x, D x → EFin \o g^~x --> 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 →
∃ 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 → ∃ 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 → ∃ 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)) :
(∀ 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 →
(∀ 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)) :
(∀ k x, 0 ≤ h k x) → (∀ 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 : ∀ n, measurable_fun D (f n).
Hypothesis f0 : ∀ 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 : ∀ n, measurable_fun D (f n).
Hypothesis f0 : ∀ 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' : ∀ 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[mu]_(x in D) (f' x) = lim (fun n ⇒ \int[mu]_(x in D) (g' n x)).
Lemma cvg_monotone_convergence :
(fun n ⇒ \int[mu]_(x in D) g' n x) --> \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 : ∀ n, measurable_fun D (f n).
Hypothesis f0 : ∀ 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.
generalization of ge0_integralZl_EFin to a constant potentially +oo
using the monotone convergence theorem
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) : (∀ 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.
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.
#[deprecated(since="mathcomp-analysis 0.6.4", note="use `integralZl_indic_nnsfun` instead")]
Notation integralM_indic_nnsfun := integralZl_indic_nnsfun.
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) :
(∀ 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 : ∀ n, measurable_fun D (f n).
Hypothesis f0 : ∀ n x, D x → 0 ≤ f n x.
Lemma fatou : \int[mu]_(x in D) lim_einf (f^~ x) ≤
lim_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) :
(∀ 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.
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 → (∀ 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 : ∀ 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 = (\1_D a)%:E × 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) :
(∀ x, D x → 0 ≤ f x) → measurable_fun D f → ∀ 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) :
(∀ 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) :
(∀ 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 →
(∀ 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 → (∀ 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 (F : (set T)^nat) (f : T → \bar R) n :
(∀ n, measurable (F n)) →
let D := \big[setU/set0]_(i < n) F i in
measurable_fun D f →
(∀ x, D x → 0 ≤ f x) →
trivIset `I_n F →
\int[mu]_(x in D) f x = \sum_(i < n) \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.
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 →
(∀ 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)) :
(∀ 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.
#[deprecated(since="mathcomp-analysis 0.6.4", note="use `integrableZr` instead")]
Notation integrableMr := integrableZr.
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) :
(∀ 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) :
(∀ k, measurable (F k)) →
let D := \bigcup_k F k in
mu.-integrable D f →
(∀ 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, ∀ 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.
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 (R : realType) (T : measurableType d)
(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.
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.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (mu : {measure set T → \bar R}) (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_eq0 f g : measurable D → mu D = 0 → ae_eq f g.
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_funeposneg f g : ae_eq f g ↔ ae_eq f^\+ g^\+ ∧ ae_eq f^\- g^\-.
Lemma ae_eq_refl f : ae_eq f f.
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_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.
Context d (T : measurableType d) (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[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 →
(∀ 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 →
(∀ x, D x → 0 ≤ f x) → (∀ 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 →
∀ 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 : ∀ 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) : (∀ 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 → (∀ 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 → (∀ 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_ : ∀ 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 {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_ : ∀ 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,
[sequence \int[mu]_(x in D) (g_ n x)]_n --> 0 &
[sequence \int[mu]_(x in D) (f_ n x)]_n --> \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 : ∀ 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 ae_ge0_le_integral : {ae mu, ∀ 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, ∀ 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 →
(∀ E, 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 → mu.-integrable D g →
(∀ E, 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.
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) : (∀ 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.
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.
#[deprecated(since="mathcomp-analysis 0.6.4", note="use `integralZl_indic_nnsfun` instead")]
Notation integralM_indic_nnsfun := integralZl_indic_nnsfun.
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) :
(∀ 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 : ∀ n, measurable_fun D (f n).
Hypothesis f0 : ∀ n x, D x → 0 ≤ f n x.
Lemma fatou : \int[mu]_(x in D) lim_einf (f^~ x) ≤
lim_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) :
(∀ 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.
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 → (∀ 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 : ∀ 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 = (\1_D a)%:E × 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) :
(∀ x, D x → 0 ≤ f x) → measurable_fun D f → ∀ 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) :
(∀ 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) :
(∀ 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 →
(∀ 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 → (∀ 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 (F : (set T)^nat) (f : T → \bar R) n :
(∀ n, measurable (F n)) →
let D := \big[setU/set0]_(i < n) F i in
measurable_fun D f →
(∀ x, D x → 0 ≤ f x) →
trivIset `I_n F →
\int[mu]_(x in D) f x = \sum_(i < n) \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.
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 →
(∀ 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)) :
(∀ 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.
#[deprecated(since="mathcomp-analysis 0.6.4", note="use `integrableZr` instead")]
Notation integrableMr := integrableZr.
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) :
(∀ 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) :
(∀ k, measurable (F k)) →
let D := \bigcup_k F k in
mu.-integrable D f →
(∀ 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, ∀ 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.
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 (R : realType) (T : measurableType d)
(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.
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.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (mu : {measure set T → \bar R}) (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_eq0 f g : measurable D → mu D = 0 → ae_eq f g.
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_funeposneg f g : ae_eq f g ↔ ae_eq f^\+ g^\+ ∧ ae_eq f^\- g^\-.
Lemma ae_eq_refl f : ae_eq f f.
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_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.
Context d (T : measurableType d) (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[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 →
(∀ 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 →
(∀ x, D x → 0 ≤ f x) → (∀ 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 →
∀ 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 : ∀ 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) : (∀ 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 → (∀ 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 → (∀ 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_ : ∀ 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 {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_ : ∀ 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,
[sequence \int[mu]_(x in D) (g_ n x)]_n --> 0 &
[sequence \int[mu]_(x in D) (f_ n x)]_n --> \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 : ∀ 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 ae_ge0_le_integral : {ae mu, ∀ 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, ∀ 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 →
(∀ E, 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 → mu.-integrable D g →
(∀ E, 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}).
the generalization from m2 : {measure set T2 -> \bar R}t to
T1 -> {measure set T2 -> \bar R} is needed to develop the theory
of kernels; the original type was sufficient for the development
of the theory of integration
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.
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 : ∃ M, ∀ 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.
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 : ∃ M, ∀ 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 : {measure set T1 → \bar R}) (m2 : {measure 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).
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}.
Lemma product_measure_unique
(m' : {measure set [the semiRingOfSetsType _ of T1 × T2] → \bar R}) :
(∀ A1 A2, measurable A1 → measurable A2 →
m' (A1 `*` A2) = m1 A1 × m2 A2) →
∀ 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).
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 → (∀ x, E x → 0 ≤ f x) →
∃ g_ : {sfun T >-> R}^nat,
[/\ ∀ n, mu.-integrable E (EFin \o g_ n),
∀ x, E x → EFin \o g_^~ x @ \oo --> f x &
(fun n ⇒ \int[mu]_(z in E) `|f z - (g_ n z)%:E|) --> 0].
Lemma approximation_sfun_integrable (f : T → \bar R):
mu.-integrable E f →
∃ g_ : {sfun T >-> R}^nat,
[/\ ∀ n, mu.-integrable E (EFin \o g_ n),
∀ x, E x → EFin \o g_^~ x @ \oo --> f x &
(fun n ⇒ \int[mu]_(z in E) `|f z - (g_ n z)%:E|) --> 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) →
∃ g_ : (rT → rT)^nat,
[/\ ∀ n, continuous (g_ n),
∀ n, mu.-integrable E (EFin \o g_ n) &
(fun n ⇒ \int[mu]_(z in E) `|(f z - g_ n z)%:E|) --> 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 : ∀ 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.
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.
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 : ∃ M, ∀ 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.
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 : ∃ M, ∀ 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 : {measure set T1 → \bar R}) (m2 : {measure 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).
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}.
Lemma product_measure_unique
(m' : {measure set [the semiRingOfSetsType _ of T1 × T2] → \bar R}) :
(∀ A1 A2, measurable A1 → measurable A2 →
m' (A1 `*` A2) = m1 A1 × m2 A2) →
∀ 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).
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 → (∀ x, E x → 0 ≤ f x) →
∃ g_ : {sfun T >-> R}^nat,
[/\ ∀ n, mu.-integrable E (EFin \o g_ n),
∀ x, E x → EFin \o g_^~ x @ \oo --> f x &
(fun n ⇒ \int[mu]_(z in E) `|f z - (g_ n z)%:E|) --> 0].
Lemma approximation_sfun_integrable (f : T → \bar R):
mu.-integrable E f →
∃ g_ : {sfun T >-> R}^nat,
[/\ ∀ n, mu.-integrable E (EFin \o g_ n),
∀ x, E x → EFin \o g_^~ x @ \oo --> f x &
(fun n ⇒ \int[mu]_(z in E) `|f z - (g_ n z)%:E|) --> 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) →
∃ g_ : (rT → rT)^nat,
[/\ ∀ n, continuous (g_ n),
∀ n, mu.-integrable E (EFin \o g_ n) &
(fun n ⇒ \int[mu]_(z in E) `|(f z - g_ n z)%:E|) --> 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 : ∀ 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.
NB: only relies on mf
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)|).
(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)|).
/NB: only relies on mf
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[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 : ∀ 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.
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.