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, etc.
Main notation:
| Coq notation | | Meaning |
|----------------------:|--|:--------------------------------
| \int[mu]_(x in D) f x |==| $\int_D f(x)\mathbf{d}\mu(x)$
| \int[mu]_x f x |==| $\int f(x)\mathbf{d}\mu(x)$
Main reference:
- Daniel Li, Intégration et applications, 2016
Detailed contents:
````
{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
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
locally_integrable D f == the real number-valued function f is locally
integrable on D
iavg f A := "average" of the real-valued function f over
the set A
HL_maximal == the Hardy–Littlewood maximal operator
input: real number-valued function
output: extended real number-valued function
````
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Reserved Notation "\int [ mu ]_ ( i 'in' D ) F"
(
at level 36, F at level 36, mu at level 10, i, D at level 50,
format "'[' \int [ mu ]_ ( i 'in' D ) '/ ' F ']'").
Reserved Notation "\int [ mu ]_ i F"
(
at level 36, F at level 36, mu at level 10, i at level 0,
right associativity, format "'[' \int [ mu ]_ i '/ ' F ']'").
Reserved Notation "mu .-integrable" (at level 2, format "mu .-integrable").
Reserved Notation "m1 '\x' m2" (
at level 40, m2 at next level).
Reserved Notation "m1 '\x^' m2" (
at level 40, m2 at next level).
#[global]
Hint Extern 0 (
measurable [set _])
=> solve [apply: measurable_set1] : core.
HB.mixin Record isMeasurableFun
d
(
aT
: measurableType d) (
rT
: realType)
(
f
: aT -> rT)
:= {
measurable_funP
: measurable_fun setT f
}.
HB.structure Definition MeasurableFun
d
aT
rT
:=
{f of @isMeasurableFun d aT rT f}.
Reserved Notation "{ 'mfun' aT >-> T }"
(
at level 0, format "{ 'mfun' aT >-> T }").
Reserved Notation "[ 'mfun' 'of' f ]"
(
at level 0, format "[ 'mfun' 'of' f ]").
Notation
"{ 'mfun' aT >-> T }"
:= (
@MeasurableFun.
type _ aT T)
: form_scope.
Notation
"[ 'mfun' 'of' f ]"
:= [the {mfun _ >-> _} of f] : form_scope.
#[global] Hint Resolve measurable_funP : core.
HB.structure Definition SimpleFun
d
(
aT
: measurableType d) (
rT
: realType)
:=
{f of @isMeasurableFun d aT rT f & @FiniteImage aT rT f}.
Reserved Notation "{ 'sfun' aT >-> T }"
(
at level 0, format "{ 'sfun' aT >-> T }").
Reserved Notation "[ 'sfun' 'of' f ]"
(
at level 0, format "[ 'sfun' 'of' f ]").
Notation
"{ 'sfun' aT >-> T }"
:= (
@SimpleFun.
type _ aT T)
: form_scope.
Notation
"[ 'sfun' 'of' f ]"
:= [the {sfun _ >-> _} of f] : form_scope.
Lemma
measurable_sfunP
{d} {aT : measurableType d} {rT : realType}
(
f
: {mfun aT >-> rT}) (
Y
: set rT)
: measurable Y -> measurable (
f @^-1` Y).
Proof.
HB.structure Definition NonNegSimpleFun
d
(
aT
: measurableType d) (
rT
: realType)
:=
{f of @SimpleFun d _ _ f & @NonNegFun aT rT f}.
Reserved Notation "{ 'nnsfun' aT >-> T }"
(
at level 0, format "{ 'nnsfun' aT >-> T }").
Reserved Notation "[ 'nnsfun' 'of' f ]"
(
at level 0, format "[ 'nnsfun' 'of' f ]").
Notation
"{ 'nnsfun' aT >-> T }"
:= (
@NonNegSimpleFun.
type _ aT%type T)
: form_scope.
Notation
"[ 'nnsfun' 'of' f ]"
:= [the {nnsfun _ >-> _} of f] : form_scope.
Section
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
Proof.
exact. Qed.
Canonical
mfun_keyed
:= KeyedPred mfun_key.
End mfun_pred.
Section
mfun
.
Context {d} {aT : measurableType d} {rT : realType}.
Notation
T
:= {mfun aT >-> rT}.
Notation
mfun
:= (
@mfun _ aT rT).
Section
Sub
.
Context (
f
: aT -> rT) (
fP
: f \in mfun).
Definition
mfun_Sub_subproof
:= @isMeasurableFun.
Build d aT rT f (
set_mem fP).
#[local] HB.instance Definition _ := mfun_Sub_subproof.
Definition
mfun_Sub
:= [mfun of f].
End Sub.
Lemma
mfun_rect
(
K
: T -> Type)
:
(
forall
f
(
Pf
: f \in mfun)
, K (
mfun_Sub Pf))
-> forall
u
: T, K u.
Proof.
move=> Ksub [f [[Pf]]]/=.
by suff -> : Pf = (
set_mem (
@mem_set _ [set
f
| _] f Pf))
by apply: Ksub.
Qed.
Lemma
mfun_valP
f
(
Pf
: f \in mfun)
: mfun_Sub Pf = f :> (
_ -> _).
Proof.
by []. Qed.
Canonical
mfun_subType
:= SubType T _ _ mfun_rect mfun_valP.
Lemma
mfuneqP
(
f
g
: {mfun aT >-> rT})
: f = g <-> f =1 g.
Proof.
by split=> [->//|fg]; apply/val_inj/funext. Qed.
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).
Proof.
by split. Qed.
HB.instance Definition _
x
:= @cst_mfun_subproof x.
Definition
cst_mfun
x
:= [the {mfun aT >-> rT} of cst x].
Lemma
mfun_cst
x
: @cst_mfun x =1 cst x
Proof.
by []. Qed.
HB.instance Definition _ := @isMeasurableFun.
Build _ _ rT
(
@normr rT rT) (
@measurable_normr rT setT).
HB.instance Definition _ :=
isMeasurableFun.Build _ _ _ (
@expR rT) (
@measurable_expR rT).
Lemma
measurableT_comp_subproof
(
f
: {mfun _ >-> rT}) (
g
: {mfun aT >-> rT})
:
measurable_fun setT (
f \o g).
Proof.
HB.instance Definition _ (
f
: {mfun _ >-> rT}) (
g
: {mfun aT >-> rT})
:=
isMeasurableFun.Build _ _ _ (
f \o g) (
measurableT_comp_subproof _ _).
End mfun.
Section
ring
.
Context
d
(
aT
: measurableType d) (
rT
: realType).
Lemma
mfun_subring_closed
: subring_closed (
@mfun _ aT rT).
Proof.
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 :> (
_ -> _)
Proof.
by []. Qed.
Lemma
mfun1
: (
1 : {mfun aT >-> rT})
=1 cst 1 :> (
_ -> _)
Proof.
by []. Qed.
Lemma
mfunN
f
: - f = \- f :> (
_ -> _)
Proof.
by []. Qed.
Lemma
mfunD
f
g
: f + g = f \+ g :> (
_ -> _)
Proof.
by []. Qed.
Lemma
mfunB
f
g
: f - g = f \- g :> (
_ -> _)
Proof.
by []. Qed.
Lemma
mfunM
f
g
: f * g = f \* g :> (
_ -> _)
Proof.
by []. Qed.
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.
Proof.
by elim/big_rec2: _ => //= i y ? Pi <-. Qed.
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.
Proof.
by elim/big_rec2: _ => //= i y ? Pi <-. Qed.
Lemma
mfunX
f
n
: f ^+ n = (
fun
x
=> f x ^+ n)
:> (
_ -> _).
Proof.
by apply/funext=> x; elim: n => [|n IHn]//; rewrite !exprS mfunM/= IHn. Qed.
HB.instance Definition _
f
g
:= MeasurableFun.copy (
f \+ g) (
f + g).
HB.instance Definition _
f
g
:= MeasurableFun.copy (
\- f) (
- f).
HB.instance Definition _
f
g
:= MeasurableFun.copy (
f \- g) (
f - g).
HB.instance Definition _
f
g
:= MeasurableFun.copy (
f \* g) (
f * g).
Definition
mindic
(
D
: set aT)
of measurable D : aT -> rT := \1_D.
Lemma
mindicE
(
D
: set aT) (
mD
: measurable D)
:
mindic mD = (
fun
x
=> (
x \in D)
%:R).
Proof.
HB.instance Definition _ (
D
: set aT) (
mD
: measurable D)
:
@FImFun aT rT (
mindic mD)
:= FImFun.on (
mindic mD).
Lemma
indic_mfun_subproof
(
D
: set aT) (
mD
: measurable D)
:
@isMeasurableFun d aT rT (
mindic mD).
Proof.
HB.instance Definition _
D
mD
:= @indic_mfun_subproof D mD.
Definition
indic_mfun
(
D
: set aT) (
mD
: measurable D)
:=
[the {mfun aT >-> rT} of mindic mD].
HB.instance Definition _
k
f
:= MeasurableFun.copy (
k \o* f) (
f * cst_mfun k).
Definition
scale_mfun
k
f
:= [the {mfun aT >-> rT} of k \o* f].
Lemma
max_mfun_subproof
f
g
: @isMeasurableFun d aT rT (
f \max g).
Proof.
HB.instance Definition _
f
g
:= max_mfun_subproof f g.
Definition
max_mfun
f
g
:= [the {mfun aT >-> _} of f \max g].
End ring.
Arguments indic_mfun {d aT rT} _.
Lemma
measurable_indic
d
(
T
: measurableType d) (
R
: realType)
(
D
A
: set T)
: measurable A ->
measurable_fun D (
\1_A : T -> R).
Proof.
by move=> mA; apply/measurable_funTS; rewrite (
_ : \1__ = mindic R mA).
Qed.
#[global] Hint Extern 0 (
measurable_fun _ (
\1__ : _ -> _))
=>
(
exact: measurable_indic )
: core.
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_indic` instead")
]
Notation
measurable_fun_indic
:= measurable_indic (
only parsing).
Section
sfun_pred
.
Context {d} {aT : measurableType d} {rT : realType}.
Definition
sfun
: {pred _ -> _} := [predI @mfun _ aT rT & fimfun].
Definition
sfun_key
: pred_key sfun
Proof.
exact. Qed.
Canonical
sfun_keyed
:= KeyedPred sfun_key.
Lemma
sub_sfun_mfun
: {subset sfun <= mfun}
Proof.
by move=> x /andP[]. Qed.
Lemma
sub_sfun_fimfun
: {subset sfun <= fimfun}
Proof.
by move=> x /andP[]. Qed.
End sfun_pred.
Section
sfun
.
Context {d} {aT : measurableType d} {rT : realType}.
Notation
T
:= {sfun aT >-> rT}.
Notation
sfun
:= (
@sfun _ aT rT).
Section
Sub
.
Context (
f
: aT -> rT) (
fP
: f \in sfun).
Definition
sfun_Sub1_subproof
:=
@isMeasurableFun.
Build d aT rT f (
set_mem (
sub_sfun_mfun fP)).
#[local] HB.instance Definition _ := sfun_Sub1_subproof.
Definition
sfun_Sub2_subproof
:=
@FiniteImage.
Build aT rT f (
set_mem (
sub_sfun_fimfun fP)).
#[local] HB.instance Definition _ := sfun_Sub2_subproof.
Definition
sfun_Sub
:= [sfun of f].
End Sub.
Lemma
sfun_rect
(
K
: T -> Type)
:
(
forall
f
(
Pf
: f \in sfun)
, K (
sfun_Sub Pf))
-> forall
u
: T, K u.
Proof.
Lemma
sfun_valP
f
(
Pf
: f \in sfun)
: sfun_Sub Pf = f :> (
_ -> _).
Proof.
by []. Qed.
Canonical
sfun_subType
:= SubType T _ _ sfun_rect sfun_valP.
Lemma
sfuneqP
(
f
g
: {sfun aT >-> rT})
: f = g <-> f =1 g.
Proof.
by split=> [->//|fg]; apply/val_inj/funext. Qed.
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.
Definition
cst_sfun
x
:= [the {sfun aT >-> rT} of cst x].
Lemma
cst_sfunE
x
: @cst_sfun x =1 cst x
Proof.
by []. Qed.
End sfun.
Lemma
fctD
(
T
: pointedType) (
K
: ringType) (
f
g
: T -> K)
: f + g = f \+ g.
Proof.
by []. Qed.
Lemma
fctN
(
T
: pointedType) (
K
: ringType) (
f
: T -> K)
: - f = \- f.
Proof.
by []. Qed.
Lemma
fctM
(
T
: pointedType) (
K
: ringType) (
f
g
: T -> K)
: f * g = f \* g.
Proof.
by []. Qed.
Lemma
fctZ
(
T
: pointedType) (
K
: ringType) (
L
: lmodType K)
k
(
f
: T -> L)
:
k *: f = k \*: f.
Proof.
by []. Qed.
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).
Proof.
by split=> [|f g|f g]; rewrite ?inE/= ?rpred1//;
move=> /andP[/= mf ff] /andP[/= mg fg]; rewrite !(
rpredB, rpredM).
Qed.
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
Proof.
by []. Qed.
Lemma
sfun1
: (
1 : {sfun aT >-> rT})
=1 cst 1
Proof.
by []. Qed.
Lemma
sfunN
f
: - f =1 \- f
Proof.
by []. Qed.
Lemma
sfunD
f
g
: f + g =1 f \+ g
Proof.
by []. Qed.
Lemma
sfunB
f
g
: f - g =1 f \- g
Proof.
by []. Qed.
Lemma
sfunM
f
g
: f * g =1 f \* g
Proof.
by []. Qed.
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.
Proof.
by elim/big_rec2: _ => //= i y ? Pi <-. Qed.
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.
Proof.
by elim/big_rec2: _ => //= i y ? Pi <-. Qed.
Lemma
sfunX
f
n
: f ^+ n =1 (
fun
x
=> f x ^+ n).
Proof.
by move=> x; elim: n => [|n IHn]//; rewrite !exprS sfunM/= IHn. Qed.
HB.instance Definition _
f
g
:= MeasurableFun.copy (
f \+ g) (
f + g).
HB.instance Definition _
f
g
:= MeasurableFun.copy (
\- f) (
- f).
HB.instance Definition _
f
g
:= MeasurableFun.copy (
f \- g) (
f - g).
HB.instance Definition _
f
g
:= MeasurableFun.copy (
f \* g) (
f * g).
Definition
indic_sfun
(
D
: set aT) (
mD
: measurable D)
:=
[the {sfun aT >-> rT} of mindic rT mD].
HB.instance Definition _
k
f
:= MeasurableFun.copy (
k \o* f) (
f * cst_sfun k).
Definition
scale_sfun
k
f
:= [the {sfun aT >-> rT} of k \o* f].
HB.instance Definition _
f
g
:= max_mfun_subproof f g.
Definition
max_sfun
f
g
:= [the {sfun aT >-> _} of f \max g].
End ring.
Arguments indic_sfun {d aT rT} _.
Lemma
fset_set_comp
(
T1
: Type) (
T2
T3
: choiceType) (
D
: set T1)
(
f
: {fimfun T1 >-> T2}) (
g
: T2 -> T3)
:
fset_set [set (
g \o f)
x |
x
in D] =
[fset g x |
x
in fset_set [set f x |
x
in D]]%fset.
Proof.
Lemma
preimage_nnfun0
T
(
R
: realDomainType) (
f
: {nnfun T >-> R})
t
:
t < 0 -> f @^-1` [set t] = set0.
Proof.
move=> t0.
by apply/preimage10 => -[x _]; apply: contraPnot t0 => <-; rewrite le_gtF.
Qed.
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].
Proof.
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])).
Proof.
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]).
Proof.
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).
Proof.
by split=> /=. Qed.
HB.instance Definition _
x
:= @cst_nnfun_subproof x.
Definition
cst_nnsfun
(
r
: {nonneg R})
:= [the {nnsfun T >-> R} of cst r%:num].
Definition
nnsfun0
: {nnsfun T >-> R} := cst_nnsfun 0%R%:nng.
Lemma
indic_nnfun_subproof
(
D
: set T)
: @isNonNegFun T R (
\1_D).
Proof.
by split=> //=; rewrite /indic. Qed.
HB.instance Definition _
D
:= @indic_nnfun_subproof D.
HB.instance Definition _
D
(
mD
: measurable D)
:
@NonNegFun T R (
mindic R mD)
:= NonNegFun.on (
mindic R mD).
End nnsfun_functions.
Arguments nnsfun0 {d T R}.
Section
nnfun_bin
.
Variables (
T
: Type) (
R
: numDomainType) (
f
g
: {nnfun T >-> R}).
Lemma
add_nnfun_subproof
: @isNonNegFun T R (
f \+ g).
Proof.
HB.instance Definition _ := add_nnfun_subproof.
Lemma
mul_nnfun_subproof
: @isNonNegFun T R (
f \* g).
Proof.
HB.instance Definition _ := mul_nnfun_subproof.
Lemma
max_nnfun_subproof
: @isNonNegFun T R (
f \max g).
Proof.
by split => x /=; rewrite /maxr; case: ifPn => _; apply: fun_ge0. Qed.
HB.instance Definition _ := max_nnfun_subproof.
End nnfun_bin.
Section
nnsfun_bin
.
Context
d
(
T
: measurableType d) (
R
: realType).
Variables
f
g
: {nnsfun T >-> R}.
HB.instance Definition _ := MeasurableFun.on (
f \+ g).
Definition
add_nnsfun
:= [the {nnsfun T >-> R} of f \+ g].
HB.instance Definition _ := MeasurableFun.on (
f \* g).
Definition
mul_nnsfun
:= [the {nnsfun T >-> R} of f \* g].
HB.instance Definition _ := MeasurableFun.on (
f \max g).
Definition
max_nnsfun
:= [the {nnsfun T >-> R} of f \max g].
Definition
indic_nnsfun
A
(
mA
: measurable A)
:= [the {nnsfun T >-> R} of mindic R mA].
End nnsfun_bin.
Arguments add_nnsfun {d T R} _ _.
Arguments mul_nnsfun {d T R} _ _.
Arguments max_nnsfun {d T R} _ _.
Section
nnsfun_iter
.
Context
d
(
T
: measurableType d) (
R
: realType) (
D
: set T).
Variable
f
: {nnsfun T >-> R}^nat.
Definition
sum_nnsfun
n
:= \big[add_nnsfun/nnsfun0]_(
i
< n)
f i.
Lemma
sum_nnsfunE
n
t
: sum_nnsfun n t = \sum_(
i
< n) (
f i t).
Proof.
by rewrite /sum_nnsfun; elim/big_ind2 : _ => [|x g y h <- <-|]. Qed.
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).
Proof.
by rewrite /bigmax_nnsfun; elim/big_ind2 : _ => [|x g y h <- <-|]. Qed.
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.
Proof.
Lemma
nnsfun_coverT
:
\big[setU/set0]_(
i
\in [set: R]) (
f @^-1` [set i])
= setT.
Proof.
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]).
Proof.
#[global] Hint Extern 0 (
measurable (
_ `&` _ @^-1` [set _]))
=>
solve [apply: measurable_sfun_inP; assumption] : core.
#[global] Hint Extern 0 (
finite_set _)
=> solve [apply: fimfunP] : core.
Section
measure_fsbig
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variable
m
: {measure set T -> \bar R}.
Lemma
measure_fsbig
(
I
: choiceType) (
A
: set I) (
F
: I -> set T)
:
finite_set A ->
(
forall
i,
A i -> measurable (
F i))
-> trivIset A F ->
m (
\big[setU/set0]_(
i
\in A)
F i)
= \sum_(
i
\in A)
m (
F i).
Proof.
move=> Afin Fm Ft.
by rewrite fsbig_finite// -measure_fin_bigcup// -bigsetU_fset_set.
Qed.
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])).
Proof.
rewrite -?measure_fsbig//.
- by rewrite !fsbig_finite//= big_distrr//.
- by move=> i Ai; apply: measurableI => //.
- exact/trivIset_setIl/trivIset_preimage1.
Qed.
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]).
Proof.
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.
Proof.
move=> A0 xA /=; have [x0|x0] := ltP x 0%R; first by rewrite (
xA x0)
mule0.
by rewrite mule_ge0.
Qed.
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.
Proof.
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).
Proof.
by move=> xA; rewrite (
@mulef_ge0 _ _ (
mu \o _))
//= => /xA ->; rewrite measure0.
Qed.
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]).
Proof.
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]).
Proof.
by []. Qed.
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]).
Proof.
Lemma
sintegral0
: sintegral mu (
cst 0%R)
= 0.
Proof.
Lemma
sintegral_ge0
(
f
: {nnsfun T >-> R})
: 0 <= sintegral mu f.
Proof.
Lemma
sintegral_indic
(
A
: set T)
: sintegral mu \1_A = mu A.
Proof.
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.
Proof.
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.
Proof.
by move=> /funext->. Qed.
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.
Proof.
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.
Proof.
End sintegralD.
Section
le_sintegral
.
Context
d
(
T
: measurableType d) (
R
: realType) (
m
: {measure set T -> \bar R}).
Variables
f
g
: {nnsfun T >-> R}.
Hypothesis
fg
: forall
x,
f x <= g x.
Let
fgnn
: @isNonNegFun T R (
g \- f).
Proof.
#[local] HB.instance Definition _ := fgnn.
Lemma
le_sintegral
: (
sintegral m f <= sintegral m g)
%E.
Proof.
End le_sintegral.
Lemma
is_cvg_sintegral
d
(
T
: measurableType d) (
R
: realType)
(
m
: {measure set T -> \bar R}) (
f
: {nnsfun T >-> R}^nat)
:
(
forall
x,
nondecreasing_seq (
f ^~ x))
-> cvg (
sintegral m \o f).
Proof.
move=> nd_f; apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvgn => a b ab.
by apply: le_sintegral => // => x; exact/nd_f.
Qed.
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.
Proof.
Definition
scale_nnsfun
d
(
T
: measurableType d) (
R
: realType)
(
f
: {nnsfun T >-> R}) (
k
: R) (
k0
: 0 <= k)
:=
mul_nnsfun (
cst_nnsfun T (
NngNum k0))
f.
Section
sintegral_nondecreasing_limit_lemma
.
Context
d
(
T
: measurableType d) (
R
: realType).
Variable
mu
: {measure set T -> \bar R}.
Variables (
g
: {nnsfun T >-> R}^nat) (
f
: {nnsfun T >-> R}).
Hypothesis
nd_g
: forall
x,
nondecreasing_seq (
g^~ x).
Hypothesis
gf
: forall
x,
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}.
Proof.
move=> n m nm; rewrite /fleg; apply/subsetPset => x /= cfg.
by move: cfg => /le_trans; apply; exact: nd_g.
Qed.
Let
mfleg
c
n
: measurable (
fleg c n).
Proof.
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}.
Proof.
Let
bigcup_fleg
c
: c < 1 -> \bigcup_n fleg c n = setT.
Proof.
move=> c1; rewrite predeqE => x; split=> // _.
have := @fun_ge0 _ _ f x; rewrite le_eqVlt => /predU1P[|] gx0.
by exists O => //; rewrite /fleg /=; rewrite -gx0 mulr0 fun_ge0.
have [cf|df] := pselect (
cvg (
g^~ x)).
have cfg : lim (
g^~ x)
> c * f x.
by rewrite (
lt_le_trans _ (
gf cf))
// gtr_pmull.
suff [n cfgn] : exists
n,
g n x >= c * f x by exists n.
move/(
@lt_lim _ _ _ (
nd_g x)
cf)
: cfg => [n _ nf].
by exists n; apply: nf => /=.
have /cvgryPge/(
_ (
c * f x))
[n _ ncfgn]:= nondecreasing_dvgn_lt (
nd_g x)
df.
by exists n => //; rewrite /fleg /=; apply: ncfgn => /=.
Qed.
Local Open Scope ereal_scope.
Lemma
nd_sintegral_lim_lemma
: sintegral mu f <= lim (
sintegral mu \o g).
Proof.
End sintegral_nondecreasing_limit_lemma.
Section
sintegral_nondecreasing_limit
.
Context
d
(
T
: measurableType d) (
R
: realType).
Variable
mu
: {measure set T -> \bar R}.
Variables (
g
: {nnsfun T >-> R}^nat) (
f
: {nnsfun T >-> R}).
Hypothesis
nd_g
: forall
x,
nondecreasing_seq (
g^~ x).
Hypothesis
gf
: forall
x,
g ^~ x --> f x.
Let
limg
x
: lim (
g^~x)
= f x.
Proof.
Lemma
nd_sintegral_lim
: sintegral mu f = lim (
sintegral mu \o g).
Proof.
End sintegral_nondecreasing_limit.
Section
integral
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Implicit Types (
f g : T -> \bar R) (
D : set T).
Let
nnintegral
mu
f
:= ereal_sup [set sintegral mu h |
h
in [set
h
: {nnsfun T >-> R} | forall
x,
(
h x)
%:E <= f x]].
Definition
integral
mu
D
f
(
g
:= f \_ D)
:=
nnintegral mu (
g ^\+)
- nnintegral mu (
g ^\-).
Variable (
mu
: {measure set T -> \bar R}).
Let
nnintegral_ge0
f
: (
forall
x,
0 <= f x)
-> 0 <= nnintegral mu f.
Proof.
Let
eq_nnintegral
g
f
: f =1 g -> nnintegral mu f = nnintegral mu g.
Proof.
by move=> /funext->. Qed.
Let
nnintegral0
: nnintegral mu (
cst 0)
= 0.
Proof.
rewrite /nnintegral /=; apply/eqP; rewrite eq_le; apply/andP; split; last first.
apply/ereal_sup_ub; exists nnsfun0; last by rewrite sintegral0.
by [].
apply/ub_ereal_sup => /= x [f /= f0 <-]; have {}f0 : forall
x,
f x = 0%R.
by move=> y; apply/eqP; rewrite eq_le -2!lee_fin f0 //= lee_fin//.
by rewrite (
eq_sintegral (
@nnsfun0 _ T R))
?sintegral0.
Qed.
Let
nnintegral_nnsfun
(
h
: {nnsfun T >-> R})
:
nnintegral mu (
EFin \o h)
= sintegral mu h.
Proof.
apply/eqP; rewrite eq_le; apply/andP; split.
by apply/ub_ereal_sup => /= _ -[g /= gh <-]; rewrite le_sintegral.
by apply: ereal_sup_ub => /=; exists h.
Qed.
Local Notation
"\int_ ( x 'in' D ) F"
:= (
integral mu D (
fun
x
=> F))
(
at level 36, F at level 36, x, D at level 50,
format "'[' \int_ ( x 'in' D ) '/ ' F ']'").
Lemma
eq_integral
D
g
f
: {in D, f =1 g} ->
\int_(
x
in D)
f x = \int_(
x
in D)
g x.
Proof.
by rewrite /integral => /eq_restrictP->. Qed.
Lemma
ge0_integralE
D
f
: (
forall
x,
D x -> 0 <= f x)
->
\int_(
x
in D)
f x = nnintegral mu (
f \_ D).
Proof.
Lemma
ge0_integralTE
f
: (
forall
x,
0 <= f x)
->
\int_(
x
in setT)
f x = nnintegral mu f.
Proof.
Lemma
integralE
D
f
:
\int_(
x
in D)
f x = \int_(
x
in D) (
f ^\+ x)
- \int_(
x
in D)
f ^\- x.
Proof.
Lemma
integral0
D
: \int_(
x
in D) (
cst 0 x)
= 0.
Proof.
Lemma
integral0_eq
D
f
:
(
forall
x,
D x -> f x = 0)
-> \int_(
x
in D)
f x = 0.
Proof.
Lemma
integral_ge0
D
f
: (
forall
x,
D x -> 0 <= f x)
-> 0 <= \int_(
x
in D)
f x.
Proof.
Lemma
integral_nnsfun
D
(
mD
: measurable D) (
h
: {nnsfun T >-> R})
:
\int_(
x
in D) (
h x)
%:E = sintegral mu (
h \_ D).
Proof.
End integral.
Notation
"\int [ mu ]_ ( x 'in' D ) f"
:=
(
integral mu D (
fun
x
=> f))
: ereal_scope.
Notation
"\int [ mu ]_ x f"
:=
((
integral mu setT (
fun
x
=> f)))
%E : ereal_scope.
Arguments eq_integral {d T R mu D} g.
Section
eq_measure_integral
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType) (
D
: set T).
Implicit Types m : {measure set T -> \bar R}.
Let
eq_measure_integral0
m2
m1
(
f
: T -> \bar R)
:
(
forall
A,
measurable A -> A `<=` D -> m1 A = m2 A)
->
[set sintegral m1 h |
h
in
[set
h
: {nnsfun T >-> R} | (
forall
x,
(
h x)
%:E <= (
f \_ D)
x)
]] `<=`
[set sintegral m2 h |
h
in
[set
h
: {nnsfun T >-> R} | (
forall
x,
(
h x)
%:E <= (
f \_ D)
x)
]].
Proof.
Lemma
eq_measure_integral
m2
m1
(
f
: T -> \bar R)
:
(
forall
A,
measurable A -> A `<=` D -> m1 A = m2 A)
->
\int[m1]_(
x
in D)
f x = \int[m2]_(
x
in D)
f x.
Proof.
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.
Proof.
Lemma
integral_measure_zero
(
D
: set T) (
f
: T -> \bar R)
:
\int[mzero]_(
x
in D)
f x = 0.
Proof.
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.
Proof.
Lemma
integralT_nnsfun
(
h
: {nnsfun T >-> R})
:
\int[mu]_x (
h x)
%:E = sintegral mu h.
Proof.
Lemma
integral_mkcondr
D
P
f
:
\int[mu]_(
x
in D `&` P)
f x = \int[mu]_(
x
in D) (
f \_ P)
x.
Proof.
Lemma
integral_mkcondl
D
P
f
:
\int[mu]_(
x
in P `&` D)
f x = \int[mu]_(
x
in D) (
f \_ P)
x.
Proof.
End domain_change.
Arguments integral_mkcond {d T R mu} D f.
Section
nondecreasing_integral_limit
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variables (
mu
: {measure set T -> \bar R}) (
f
: T -> \bar R)
(
g
: {nnsfun T >-> R}^nat).
Hypothesis
f0
: forall
x,
0 <= f x.
Hypothesis
mf
: measurable_fun setT f.
Hypothesis
nd_g
: forall
x,
nondecreasing_seq (
g^~x).
Hypothesis
gf
: forall
x,
EFin \o g^~x --> f x.
Local Open Scope ereal_scope.
Lemma
nd_ge0_integral_lim
: \int[mu]_x f x = lim (
sintegral mu \o g).
Proof.
End nondecreasing_integral_limit.
Section
dyadic_interval
.
Variable
R
: realType.
Definition
dyadic_itv
n
k
: interval R :=
`[(
k%:R * 2 ^- n)
, (
k.
+1%:R * 2 ^- n)
[.
Local Notation
I
:= dyadic_itv.
Lemma
dyadic_itv_subU
n
k
: [set` I n k] `<=`
[set` I n.
+1 k.
*2] `|` [set` I n.
+1 k.
*2.
+1].
Proof.
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].
Proof.
Lemma
dyadic_itv_image
n
T
(
f
: T -> \bar R)
x
:
(
n%:R%:E <= f x < n.
+1%:R%:E)
%E ->
exists
k,
(
2 ^ n.
+1 * n <= k < 2 ^ n.
+1 * n.
+1)
%N /\
f x \in EFin @` [set` I n.
+1 k].
Proof.
End dyadic_interval.
Section
approximation
.
Context
d
(
T
: measurableType d) (
R
: realType).
Variables (
D
: set T) (
mD
: measurable D).
Variables (
f
: T -> \bar R) (
mf
: measurable_fun D f).
Local Notation
I
:= (
@dyadic_itv R).
Let
A
n
k
:= if (
k < n * 2 ^ n)
%N then
D `&` [set
x
| f x \in EFin @` [set` I n k]] else set0.
Let
B
n
:= D `&` [set
x
| n%:R%:E <= f x]%E.
Definition
approx
: (
T -> R)
^nat := fun
n
x
=>
\sum_(
k
< n * 2 ^ n)
k%:R * 2 ^- n * \1_(
A n k)
x + n%:R * \1_(
B n)
x.
Let
mA
n
k
: measurable (
A n k).
Proof.
rewrite /A; case: ifPn => [kn|_]//; rewrite -preimage_comp.
by apply: mf => //; apply/measurable_image_EFin; exact: measurable_itv.
Qed.
Let
trivIsetA
n
: trivIset setT (
A n).
Proof.
apply/trivIsetP => i j _ _.
wlog : i j / (
i < j)
%N.
move=> h; rewrite neq_lt => /orP[ij|ji].
by apply: h => //; rewrite lt_eqF.
by rewrite setIC; apply: h => //; rewrite lt_eqF.
move=> ij _.
rewrite /A; case: ifPn => /= ni; last by rewrite set0I.
case: ifPn => /= nj; last by rewrite setI0.
rewrite predeqE => t; split => // -[/=] [_].
rewrite inE => -[r /=]; rewrite in_itv /= => /andP[r1 r2] rft [_].
rewrite inE => -[s /=]; rewrite in_itv /= => /andP[s1 s2].
rewrite -rft => -[sr]; rewrite {}sr {s} in s1 s2.
by have := le_lt_trans s1 r2; rewrite ltr_pmul2r// ltr_nat ltnS leqNgt ij.
Qed.
Let
f0_A0
n
(
i
: 'I_(
n * 2 ^ n))
x
: f x = 0%:E -> i != O :> nat ->
\1_(
A n i)
x = 0 :> R.
Proof.
Let
fgen_A0
n
x
(
i
: 'I_(
n * 2 ^ n))
: (
n%:R%:E <= f x)
%E ->
\1_(
A n i)
x = 0 :> R.
Proof.
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.
Proof.
Arguments disj_A0 {x n i} k.
Let
mB
n
: measurable (
B n)
Proof.
Let
foo_B1
x
n
: D x -> f x = +oo%E -> \1_(
B n)
x = 1 :> R.
Proof.
Let
f0_B0
x
n
: f x = 0%:E -> n != 0%N -> \1_(
B n)
x = 0 :> R.
Proof.
Let
fgtn_B0
x
n
: (
f x < n%:R%:E)
%E -> \1_(
B n)
x = 0 :> R.
Proof.
Let
f0_approx0
n
x
: f x = 0%E -> approx n x = 0.
Proof.
Let
fpos_approx_neq0
x
: D x -> (
0%E < f x < +oo)
%E ->
\forall
n
\near \oo, approx n x != 0.
Proof.
Let
f_ub_approx
n
x
: (
f x < n%:R%:E)
%E ->
approx n x == 0 \/ exists
k,
[/\ (
0 < k < n * 2 ^ n)
%N,
x \in A n k, approx n x = k%:R / 2 ^+ n &
f x \in EFin @` [set` I n k]].
Proof.
Let
notinD_approx0
x
n
: ~ D x -> approx n x = 0 :> R.
Proof.
Lemma
nd_approx
: nondecreasing_seq approx.
Proof.
Lemma
cvg_approx
x
(
f0
: forall
x,
D x -> (
0 <= f x)
%E)
: D x ->
(
f x < +oo)
%E -> (
approx^~ x)
--> fine (
f x).
Proof.
Lemma
le_approx
k
x
(
f0
: forall
x,
D x -> (
0 <= f x)
%E)
: D x ->
((
approx k x)
%:E <= f x)
%E.
Proof.
Lemma
dvg_approx
x
: D x -> f x = +oo%E -> ~ cvg (
approx^~ x : _ -> R^o).
Proof.
Lemma
ecvg_approx
(
f0
: forall
x,
D x -> (
0 <= f x)
%E)
x
:
D x -> EFin \o approx^~x --> f x.
Proof.
Let
k2n_ge0
n
(
k
: 'I_(
n * 2 ^ n))
: 0 <= k%:R * 2 ^- n :> R.
Proof.
by []. Qed.
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).
Proof.
Lemma
cvg_nnsfun_approx
(
f0
: forall
x,
D x -> (
0 <= f x)
%E)
x
:
D x -> EFin \o nnsfun_approx^~x --> f x.
Proof.
Lemma
nd_nnsfun_approx
: nondecreasing_seq (
nnsfun_approx : (
T -> R)
^nat).
Proof.
Lemma
approximation
: (
forall
t,
D t -> (
0 <= f t)
%E)
->
exists
g
: {nnsfun T >-> R}^nat, nondecreasing_seq (
g : (
T -> R)
^nat)
/\
(
forall
x,
D x -> EFin \o g^~x --> f x).
Proof.
End approximation.
Section
semi_linearity0
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variables (
mu
: {measure set T -> \bar R}) (
D
: set T) (
mD
: measurable D).
Variables
f1
f2
: T -> \bar R.
Hypothesis
f10
: forall
x,
D x -> 0 <= f1 x.
Hypothesis
mf1
: measurable_fun D f1.
Lemma
ge0_integralZl_EFin
k
: (
0 <= k)
%R ->
\int[mu]_(
x
in D) (
k%:E * f1 x)
= k%:E * \int[mu]_(
x
in D)
f1 x.
Proof.
End semi_linearity0.
#[deprecated(
since="mathcomp-analysis 0.6.4", note="use `ge0_integralZl_EFin` instead")
]
Notation
ge0_integralM_EFin
:= ge0_integralZl_EFin (
only parsing).
Section
semi_linearity
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variable
mu
: {measure set T -> \bar R}.
Variables (
D
: set T) (
mD
: measurable D) (
f1
f2
: T -> \bar R).
Hypothesis
f10
: forall
x,
D x -> 0 <= f1 x.
Hypothesis
mf1
: measurable_fun D f1.
Hypothesis
f20
: forall
x,
D x -> 0 <= f2 x.
Hypothesis
mf2
: measurable_fun D f2.
Lemma
ge0_integralD
: \int[mu]_(
x
in D) (
f1 x + f2 x)
=
\int[mu]_(
x
in D)
f1 x + \int[mu]_(
x
in D)
f2 x.
Proof.
Lemma
ge0_le_integral
: (
forall
x,
D x -> f1 x <= f2 x)
->
\int[mu]_(
x
in D)
f1 x <= \int[mu]_(
x
in D)
f2 x.
Proof.
End semi_linearity.
Section
approximation_sfun
.
Context
d
(
T
: measurableType d) (
R
: realType) (
f
: T -> \bar R).
Variables (
D
: set T) (
mD
: measurable D) (
mf
: measurable_fun D f).
Lemma
approximation_sfun
:
exists
g
: {sfun T >-> R}^nat, (
forall
x,
D x -> EFin \o g^~x --> f x).
Proof.
End approximation_sfun.
Section
lusin
.
Hint Extern 0 (
hausdorff_space _)
=> (
exact: Rhausdorff )
: core.
Local Open Scope ereal_scope.
Context (
rT
: realType) (
A
: set rT).
Let
mu
:= [the measure _ _ of @lebesgue_measure rT].
Let
R
:= [the measurableType _ of measurableTypeR rT].
Hypothesis
mA
: measurable A.
Hypothesis
finA
: mu A < +oo.
Let
lusin_simple
(
f
: {sfun R >-> rT}) (
eps
: rT)
: (
0 < eps)
%R ->
exists
K,
[/\ compact K, K `<=` A, mu (
A `\` K)
< eps%:E &
{within K, continuous f}].
Proof.
Let
measurable_almost_continuous'
(
f
: R -> R) (
eps
: rT)
:
(
0 < eps)
%R -> measurable_fun A f -> exists
K,
[/\ measurable K, K `<=` A, mu (
A `\` K)
< eps%:E &
{within K, continuous f}].
Proof.
Lemma
measurable_almost_continuous
(
f
: R -> R) (
eps
: rT)
:
(
0 < eps)
%R -> measurable_fun A f -> exists
K,
[/\ compact K, K `<=` A, mu (
A `\` K)
< eps%:E &
{within K, continuous f}].
Proof.
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).
Proof.
Lemma
emeasurable_fun_sum
D
I
s
(
h
: I -> (
T -> \bar R))
:
(
forall
n,
measurable_fun D (
h n))
->
measurable_fun D (
fun
x
=> \sum_(
i
<- s)
h i x).
Proof.
Lemma
emeasurable_fun_fsum
D
(
I
: choiceType) (
A
: set I)
(
h
: I -> (
T -> \bar R))
: finite_set A ->
(
forall
n,
measurable_fun D (
h n))
->
measurable_fun D (
fun
x
=> \sum_(
i
\in A)
h i x).
Proof.
Lemma
ge0_emeasurable_fun_sum
D
(
h
: nat -> (
T -> \bar R))
:
(
forall
k
x,
0 <= h k x)
-> (
forall
k,
measurable_fun D (
h k))
->
measurable_fun D (
fun
x
=> \sum_(
i
<oo)
h i x).
Proof.
Lemma
emeasurable_funB
D
f
g
:
measurable_fun D f -> measurable_fun D g -> measurable_fun D (
f \- g).
Proof.
Lemma
emeasurable_funM
D
f
g
:
measurable_fun D f -> measurable_fun D g -> measurable_fun D (
f \* g).
Proof.
Lemma
measurable_funeM
D
(
f
: T -> \bar R) (
k
: \bar R)
:
measurable_fun D f -> measurable_fun D (
fun
x
=> k * f x)
%E.
Proof.
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]).
Proof.
Lemma
emeasurable_fun_le
f
g
: measurable_fun D f -> measurable_fun D g ->
measurable (
D `&` [set
x
| f x <= g x]).
Proof.
Lemma
emeasurable_fun_eq
f
g
: measurable_fun D f -> measurable_fun D g ->
measurable (
D `&` [set
x
| f x = g x]).
Proof.
Lemma
emeasurable_fun_neq
f
g
: measurable_fun D f -> measurable_fun D g ->
measurable (
D `&` [set
x
| f x != g x]).
Proof.
End measurable_fun_measurable2.
Section
ge0_integral_sum
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variables (
mu
: {measure set T -> \bar R}) (
D
: set T) (
mD
: measurable D).
Variables (
I
: Type) (
f
: I -> (
T -> \bar R)).
Hypothesis
mf
: forall
n,
measurable_fun D (
f n).
Hypothesis
f0
: forall
n
x,
D x -> 0 <= f n x.
Lemma
ge0_integral_sum
(
s
: seq I)
:
\int[mu]_(
x
in D) (
\sum_(
k
<- s)
f k x)
=
\sum_(
k
<- s)
\int[mu]_(
x
in D) (
f k x).
Proof.
End ge0_integral_sum.
Section
ge0_integral_fsum
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variables (
mu
: {measure set T -> \bar R}) (
D
: set T) (
mD
: measurable D).
Variables (
I
: choiceType) (
f
: I -> (
T -> \bar R)).
Hypothesis
mf
: forall
n,
measurable_fun D (
f n).
Hypothesis
f0
: forall
n
x,
D x -> 0 <= f n x.
Lemma
ge0_integral_fsum
(
A
: set I)
: finite_set A ->
\int[mu]_(
x
in D) (
\sum_(
k
\in A)
f k x)
=
\sum_(
k
\in A)
\int[mu]_(
x
in D)
f k x.
Proof.
End ge0_integral_fsum.
Section
monotone_convergence_theorem
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variable
mu
: {measure set T -> \bar R}.
Variables (
D
: set T) (
mD
: measurable D) (
g'
: (
T -> \bar R)
^nat).
Hypothesis
mg'
: forall
n,
measurable_fun D (
g' n).
Hypothesis
g'0
: forall
n
x,
D x -> 0 <= g' n x.
Hypothesis
nd_g'
: forall
x,
D x -> nondecreasing_seq (
g'^~ x).
Let
f'
:= fun
x
=> lim (
g'^~ x).
Let
g
n
:= (
g' n \_ D).
Let
g0
n
x
: 0 <= g n x
Proof.
exact/erestrict_ge0/g'0. Qed.
Let
mg
n
: measurable_fun setT (
g n).
Proof.
Let
nd_g
x
: nondecreasing_seq (
g^~ x).
Proof.
by move=> m n mn; rewrite /g/patch; case: ifP => // /set_mem /nd_g' ->.
Qed.
Let
f
:= fun
x
=> lim (
g^~ x).
Let
is_cvg_g
t
: cvg (
g^~ t).
Proof.
Local Definition
g2'
n
: (
T -> R)
^nat := approx setT (
g n).
Local Definition
g2
n
: {nnsfun T >-> R}^nat := nnsfun_approx measurableT (
mg n).
Local Definition
max_g2'
: (
T -> R)
^nat :=
fun
k
t
=> (
\big[maxr/0]_(
i
< k) (
g2' i k)
t)
%R.
Local Definition
max_g2
: {nnsfun T >-> R}^nat :=
fun
k
=> bigmax_nnsfun (
g2^~ k)
k.
Let
is_cvg_g2
n
t
: cvg (
EFin \o (
g2 n ^~ t)).
Proof.
Let
nd_max_g2
: nondecreasing_seq (
max_g2 : (
T -> R)
^nat).
Proof.
Let
is_cvg_max_g2
t
: cvg (
EFin \o max_g2 ^~ t).
Proof.
Let
max_g2_g
k
x
: ((
max_g2 k x)
%:E <= g k x)
%O.
Proof.
Let
lim_max_g2_f
t
: lim (
EFin \o max_g2 ^~ t)
<= f t.
Proof.
Let
lim_g2_max_g2
t
n
: lim (
EFin\o g2 n ^~ t)
<= lim (
EFin \o max_g2 ^~ t).
Proof.
Let
cvg_max_g2_f
t
: EFin \o max_g2 ^~ t --> f t.
Proof.
Lemma
monotone_convergence
:
\int[mu]_(
x
in D) (
f' x)
= lim (
fun
n
=> \int[mu]_(
x
in D) (
g' n x)).
Proof.
Lemma
cvg_monotone_convergence
:
(
fun
n
=> \int[mu]_(
x
in D)
g' n x)
--> \int[mu]_(
x
in D)
f' x.
Proof.
End monotone_convergence_theorem.
Section
integral_nneseries
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variables (
mu
: {measure set T -> \bar R}) (
D
: set T) (
mD
: measurable D).
Variable
f
: (
T -> \bar R)
^nat.
Hypothesis
mf
: forall
n,
measurable_fun D (
f n).
Hypothesis
f0
: forall
n
x,
D x -> 0 <= f n x.
Lemma
integral_nneseries
: \int[mu]_(
x
in D) (
\sum_(
n
<oo)
f n x)
=
\sum_(
n
<oo) (
\int[mu]_(
x
in D) (
f n x)).
Proof.
End integral_nneseries.
Section
ge0_integralZl
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variable
mu
: {measure set T -> \bar R}.
Variables (
D
: set T) (
mD
: measurable D) (
f
: T -> \bar R).
Hypothesis
mf
: measurable_fun D f.
Lemma
ge0_integralZl
(
k
: \bar R)
: (
forall
x,
D x -> 0 <= f x)
->
0 <= k -> \int[mu]_(
x
in D) (
k * f x)
%E = k * \int[mu]_(
x
in D) (
f x).
Proof.
End ge0_integralZl.
#[deprecated(
since="mathcomp-analysis 0.6.4", note="use `ge0_integralZl` instead")
]
Notation
ge0_integralM
:= ge0_integralZl (
only parsing).
Section
integral_indic
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType)
(
mu
: {measure set T -> \bar R}) (
D
: set T) (
mD
: measurable D).
Lemma
integral_indic
(
E
: set T)
: measurable E ->
\int[mu]_(
x
in D) (
\1_E x)
%:E = mu (
E `&` D).
Proof.
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.
Proof.
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.
Proof.
End integralZl_indic.
Arguments integralZl_indic {d T R m D} mD f.
#[deprecated(
since="mathcomp-analysis 0.6.4", note="use `integralZl_indic` instead")
]
Notation
integralM_indic
:= integralZl_indic (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.4", note="use `integralZl_indic_nnsfun` instead")
]
Notation
integralM_indic_nnsfun
:= integralZl_indic_nnsfun (
only parsing).
Section
integral_mscale
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variables (
m
: {measure set T -> \bar R}) (
D
: set T) (
mD
: measurable D).
Variables (
k
: {nonneg R}) (
f
: T -> \bar R).
Let
integral_mscale_indic
E
: measurable E ->
\int[mscale k m]_(
x
in D) (
\1_E x)
%:E =
k%:num%:E * \int[m]_(
x
in D) (
\1_E x)
%:E.
Proof.
by move=> ?; rewrite !integral_indic. Qed.
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.
Proof.
Lemma
ge0_integral_mscale
(
mf
: measurable_fun D f)
:
(
forall
x,
D x -> 0 <= f x)
->
\int[mscale k m]_(
x
in D)
f x = k%:num%:E * \int[m]_(
x
in D)
f x.
Proof.
move=> f0; have [f_ [ndf_ f_f]] := approximation mD mf f0.
transitivity (
lim (
fun
n
=> \int[mscale k m]_(
x
in D) (
f_ n x)
%:E)).
rewrite -monotone_convergence//=.
- by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //=; exact: f_f.
- by move=> n; exact/EFin_measurable_fun/measurable_funTS.
- by move=> n x _; rewrite lee_fin.
- by move=> x _ a b /ndf_ /lefP; rewrite lee_fin.
rewrite (
_ : \int[m]_(
x
in D)
_ =
lim (
fun
n
=> \int[m]_(
x
in D) (
f_ n x)
%:E))
; last first.
rewrite -monotone_convergence//=.
- by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //; exact: f_f.
- by move=> n; exact/EFin_measurable_fun/measurable_funTS.
- by move=> n x _; rewrite lee_fin.
- by move=> x _ a b /ndf_ /lefP; rewrite lee_fin.
rewrite -limeMl//.
by congr (
lim _)
; apply/funext => n /=; rewrite integral_mscale_nnsfun.
apply/ereal_nondecreasing_is_cvgn => a b ab; apply: ge0_le_integral => //.
- by move=> x _; rewrite lee_fin.
- exact/EFin_measurable_fun/measurable_funTS.
- by move=> x _; rewrite lee_fin.
- exact/EFin_measurable_fun/measurable_funTS.
- by move=> x _; rewrite lee_fin; move/ndf_ : ab => /lefP.
Qed.
End integral_mscale.
Section
fatou
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variables (
mu
: {measure set T -> \bar R}) (
D
: set T) (
mD
: measurable D).
Variable (
f
: (
T -> \bar R)
^nat).
Hypothesis
mf
: forall
n,
measurable_fun D (
f n).
Hypothesis
f0
: forall
n
x,
D x -> 0 <= f n x.
Lemma
fatou
: \int[mu]_(
x
in D)
limn_einf (
f^~ x)
<=
limn_einf (
fun
n
=> \int[mu]_(
x
in D)
f n x).
Proof.
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.
Proof.
Lemma
integral_ge0N
(
D
: set T) (
f
: T -> \bar R)
:
(
forall
x,
D x -> 0 <= f x)
->
\int[mu]_(
x
in D)
- f x = - \int[mu]_(
x
in D)
f x.
Proof.
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.
Proof.
Local Lemma
integral_cstr
r
: \int[mu]_(
x
in D)
r%:E = r%:E * mu D.
Proof.
Local Lemma
integral_csty
: mu D != 0 -> \int[mu]_(
x
in D) (
cst +oo)
x = +oo.
Proof.
Local Lemma
integral_cstNy
: mu D != 0 -> \int[mu]_(
x
in D) (
cst -oo)
x = -oo.
Proof.
End integral_cst.
Section
transfer
.
Local Open Scope ereal_scope.
Context
d1
d2
(
X
: measurableType d1) (
Y
: measurableType d2) (
R
: realType).
Variables (
phi
: X -> Y) (
mphi
: measurable_fun setT phi).
Variables (
mu
: {measure set X -> \bar R}).
Lemma
integral_pushforward
(
f
: Y -> \bar R)
:
measurable_fun setT f -> (
forall
y,
0 <= f y)
->
\int[pushforward mu mphi]_y f y = \int[mu]_x (
f \o phi)
x.
Proof.
End transfer.
Section
integral_dirac
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
a
: T) (
R
: realType).
Variables (
D
: set T) (
mD
: measurable D).
Let
ge0_integral_dirac
(
f
: T -> \bar R) (
mf
: measurable_fun D f)
(
f0
: forall
x,
D x -> 0 <= f x)
:
D a -> \int[\d_a]_(
x
in D) (
f x)
= f a.
Proof.
Lemma
integral_dirac
(
f
: T -> \bar R) (
mf
: measurable_fun D f)
:
\int[\d_ a]_(
x
in D)
f x = \d_a D * f a.
Proof.
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.
Proof.
Let
integralT_measure_sum
(
f
: {nnsfun T >-> R})
:
\int[m]_x (
f x)
%:E = \sum_(
n
< N)
\int[m_ n]_x (
f x)
%:E.
Proof.
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.
Proof.
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.
Proof.
Section
integral_mfun_measure_sum
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variable
m_
: {measure set T -> \bar R}^nat.
Lemma
ge0_integral_measure_sum
(
D
: set T) (
mD
: measurable D)
(
f
: T -> \bar R)
:
(
forall
x,
D x -> 0 <= f x)
-> measurable_fun D f -> forall
N,
\int[msum m_ N]_(
x
in D)
f x = \sum_(
n
< N)
\int[m_ n]_(
x
in D)
f x.
Proof.
End integral_mfun_measure_sum.
Lemma
integral_measure_add
d
(
T
: measurableType d) (
R
: realType)
(
m1
m2
: {measure set T -> \bar R}) (
D
: set T) (
mD
: measurable D)
(
f
: T -> \bar R)
:
(
forall
x,
D x -> 0 <= f x)
%E -> measurable_fun D f ->
(
\int[measure_add m1 m2]_(
x
in D)
f x =
\int[m1]_(
x
in D)
f x + \int[m2]_(
x
in D)
f x)
%E.
Proof.
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.
Proof.
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.
Proof.
End integral_measure_series.
Section
ge0_integral_measure_series
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variable
m_
: {measure set T -> \bar R}^nat.
Let
m
:= mseries m_ O.
Lemma
ge0_integral_measure_series
(
D
: set T) (
mD
: measurable D) (
f
: T -> \bar R)
:
(
forall
t,
D t -> 0 <= f t)
->
measurable_fun D f ->
\int[m]_(
x
in D)
f x = \sum_(
n
<oo)
\int[m_ n]_(
x
in D)
f x.
Proof.
End ge0_integral_measure_series.
Section
subset_integral
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType)
(
mu
: {measure set T -> \bar R}).
Lemma
integral_setU
(
A
B
: set T) (
mA
: measurable A) (
mB
: measurable B)
(
f
: T -> \bar R)
: measurable_fun (
A `|` B)
f ->
(
forall
x,
(
A `|` B)
x -> 0 <= f x)
-> [disjoint A & B] ->
\int[mu]_(
x
in A `|` B)
f x = \int[mu]_(
x
in A)
f x + \int[mu]_(
x
in B)
f x.
Proof.
Lemma
subset_integral
(
A
B
: set T) (
mA
: measurable A) (
mB
: measurable B)
(
f
: T -> \bar R)
: measurable_fun B f -> (
forall
x,
B x -> 0 <= f x)
->
A `<=` B -> \int[mu]_(
x
in A)
f x <= \int[mu]_(
x
in B)
f x.
Proof.
Lemma
integral_set0
(
f
: T -> \bar R)
: \int[mu]_(
x
in set0)
f x = 0.
Proof.
Lemma
ge0_integral_bigsetU
(
I
: eqType) (
F
: I -> set T) (
f
: T -> \bar R)
(
s
: seq I)
: (
forall
n,
measurable (
F n))
-> uniq s ->
trivIset [set` s] F ->
let
D
:= \big[setU/set0]_(
i
<- s)
F i in
measurable_fun D f ->
(
forall
x,
D x -> 0 <= f x)
->
\int[mu]_(
x
in D)
f x = \sum_(
i
<- s)
\int[mu]_(
x
in F i)
f x.
Proof.
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|.
Proof.
End subset_integral.
Section
Rintegral
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType)
(
mu
: {measure set T -> \bar R}).
Definition
Rintegral
(
D
: set T) (
f
: T -> R)
:=
fine (
\int[mu]_(
x
in D) (
f x)
%:E).
End Rintegral.
Notation
"\int [ mu ]_ ( x 'in' D ) f"
:= (
Rintegral mu D (
fun
x
=> f))
: ring_scope.
Notation
"\int [ mu ]_ x f"
:= (
Rintegral mu setT (
fun
x
=> f))
: ring_scope.
HB.lock Definition integrable {d} {T : measurableType d} {R : realType}
(
mu
: set T -> \bar R)
D
f
:=
`[< measurable_fun D f /\ (
\int[mu]_(
x
in D)
`|f x| < +oo)
%E >].
Canonical
integrable_unlockable
:= Unlockable integrable.unlock.
Lemma
integrableP
d
T
R
mu
D
f
:
reflect (
measurable_fun D f /\ (
\int[mu]_(
x
in D)
`|f x| < +oo)
%E)
(
@integrable d T R mu D f).
Proof.
Lemma
measurable_int
d
T
R
mu
D
f
:
@integrable d T R mu D f -> measurable_fun D f.
Proof.
by rewrite unlock => /asboolP[]. Qed.
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).
Proof.
Lemma
eq_integrable
f
g
: {in D, f =1 g} -> mu_int f -> mu_int g.
Proof.
Lemma
le_integrable
f
g
: measurable_fun D f ->
(
forall
x,
D x -> `|f x| <= `|g x|)
-> mu_int g -> mu_int f.
Proof.
Lemma
integrableN
f
: mu_int f -> mu_int (
-%E \o f).
Proof.
Lemma
integrableZl
(
k
: R)
f
: mu_int f -> mu_int (
fun
x
=> k%:E * f x).
Proof.
Lemma
integrableZr
(
k
: R)
f
: mu_int f -> mu_int (
f \* cst k%:E).
Proof.
Lemma
integrableD
f
g
: mu_int f -> mu_int g -> mu_int (
f \+ g).
Proof.
Lemma
integrable_sum
(
s
: seq (
T -> \bar R))
:
(
forall
h,
h \in s -> mu_int h)
-> mu_int (
fun
x
=> \sum_(
h
<- s)
h x).
Proof.
Lemma
integrableB
f
g
: mu_int f -> mu_int g -> mu_int (
f \- g).
Proof.
by move=> fi gi; exact/(
integrableD fi)
/integrableN. Qed.
Lemma
integrable_add_def
f
: mu_int f ->
\int[mu]_(
x
in D)
f^\+ x +? - \int[mu]_(
x
in D)
f^\- x.
Proof.
Lemma
integrable_funepos
f
: mu_int f -> mu_int f^\+.
Proof.
Lemma
integrable_funeneg
f
: mu_int f -> mu_int f^\-.
Proof.
Lemma
integral_funeneg_lt_pinfty
f
: mu_int f ->
\int[mu]_(
x
in D)
f^\- x < +oo.
Proof.
Lemma
integral_funepos_lt_pinfty
f
: mu_int f ->
\int[mu]_(
x
in D)
f^\+ x < +oo.
Proof.
Lemma
integrable_neg_fin_num
f
:
mu_int f -> \int[mu]_(
x
in D)
f^\- x \is a fin_num.
Proof.
Lemma
integrable_pos_fin_num
f
:
mu_int f -> \int[mu]_(
x
in D)
f^\+ x \is a fin_num.
Proof.
End integrable_theory.
Notation
"mu .-integrable"
:= (
integrable mu)
: type_scope.
Arguments eq_integrable {d T R mu D} mD f.
#[deprecated(
since="mathcomp-analysis 0.6.4", note="use `integrableZl` instead")
]
Notation
integrablerM
:= integrableZl (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.4", note="use `integrableZr` instead")
]
Notation
integrableMr
:= integrableZr (
only parsing).
Section
sequence_measure
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variable
m_
: {measure set T -> \bar R}^nat.
Let
m
:= mseries m_ O.
Lemma
integral_measure_series
(
D
: set T) (
mD
: measurable D) (
f
: T -> \bar R)
:
(
forall
n,
integrable (
m_ n)
D f)
->
measurable_fun D f ->
\sum_(
n
<oo)
`|\int[m_ n]_(
x
in D)
f^\- x | < +oo%E ->
\sum_(
n
<oo)
`|\int[m_ n]_(
x
in D)
f^\+ x | < +oo%E ->
\int[m]_(
x
in D)
f x = \sum_(
n
<oo)
\int[m_ n]_(
x
in D)
f x.
Proof.
End sequence_measure.
Section
integrable_lemmas
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType)
(
mu
: {measure set T -> \bar R}).
Lemma
ge0_integral_bigcup
(
F
: (
set _)
^nat) (
f
: T -> \bar R)
:
(
forall
k,
measurable (
F k))
->
let
D
:= \bigcup_k F k in
mu.
-integrable D f ->
(
forall
x,
D x -> 0 <= f x)
->
trivIset setT F ->
\int[mu]_(
x
in D)
f x = \sum_(
i
<oo)
\int[mu]_(
x
in F i)
f x.
Proof.
Lemma
integrableS
(
E
D
: set T) (
f
: T -> \bar R)
:
measurable E -> measurable D -> D `<=` E ->
mu.
-integrable E f -> mu.
-integrable D f.
Proof.
Lemma
integrable_mkcond
D
f
: measurable D ->
mu.
-integrable D f <-> mu.
-integrable setT (
f \_ D).
Proof.
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).
Proof.
Section
integrable_ae
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variables (
mu
: {measure set T -> \bar R}) (
D
: set T) (
mD
: measurable D).
Variable
f
: T -> \bar R.
Hypotheses
fint
: mu.
-integrable D f.
Lemma
integrable_ae
: {ae mu, forall
x,
D x -> f x \is a fin_num}.
Proof.
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
Proof.
Lemma
integralZl
r
:
\int[mu]_(
x
in D) (
r%:E * f x)
= r%:E * \int[mu]_(
x
in D)
f x.
Proof.
End linearity.
#[deprecated(
since="mathcomp-analysis 0.6.4", note="use `integralZl` instead")
]
Notation
integralM
:= integralZl (
only parsing).
Section
linearity
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variables (
mu
: {measure set T -> \bar R}) (
D
: set T) (
mD
: measurable D).
Variables
f1
f2
: T -> R.
Let
g1
:= EFin \o f1.
Let
g2
:= EFin \o f2.
Hypothesis
if1
: mu.
-integrable D g1.
Hypothesis
if2
: mu.
-integrable D g2.
Let
mf1
: measurable_fun D g1
Proof.
Let
mf2
: measurable_fun D g2
Proof.
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.
Proof.
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.
Proof.
Lemma
le_abse_integral
d
(
T
: measurableType d) (
R
: realType)
(
mu
: {measure set T -> \bar R}) (
D
: set T) (
f
: T -> \bar R)
(
mD
: measurable D)
: measurable_fun D f ->
(
`| \int[mu]_(
x
in D) (
f x)
| <= \int[mu]_(
x
in D)
`|f x|)
%E.
Proof.
Lemma
abse_integralP
d
(
T
: measurableType d) (
R
: realType)
(
mu
: {measure set T -> \bar R}) (
D
: set T) (
f
: T -> \bar R)
:
measurable D -> measurable_fun D f ->
(
`| \int[mu]_(
x
in D)
f x | < +oo <-> \int[mu]_(
x
in D)
`|f x| < +oo)
%E.
Proof.
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).
Proof.
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).
Proof.
by rewrite -integral_setI_indic// setIid. Qed.
End integral_indic.
Section
ae_eq_integral
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType)
(
mu
: {measure set T -> \bar R}).
Local Notation
ae_eq
:= (
ae_eq mu).
Let
ae_eq_integral_abs_bounded
(
D
: set T) (
mD
: measurable D) (
f
: T -> \bar R)
M
: measurable_fun D f -> (
forall
x,
D x -> `|f x| <= M%:E)
->
ae_eq D f (
cst 0)
-> \int[mu]_(
x
in D)
`|f x|%E = 0.
Proof.
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).
Proof.
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.
Proof.
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).
Proof.
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.
Proof.
Lemma
ge0_negligible_integral
(
D
N
: set T) (
f
: T -> \bar R)
:
measurable N -> measurable D -> measurable_fun D f ->
(
forall
x,
D x -> 0 <= f x)
->
mu N = 0 -> \int[mu]_(
x
in D)
f x = \int[mu]_(
x
in D `\` N)
f x.
Proof.
Lemma
ge0_ae_eq_integral
(
D
: set T) (
f
g
: T -> \bar R)
:
measurable D -> measurable_fun D f -> measurable_fun D g ->
(
forall
x,
D x -> 0 <= f x)
-> (
forall
x,
D x -> 0 <= g x)
->
ae_eq D f g -> \int[mu]_(
x
in D) (
f x)
= \int[mu]_(
x
in D) (
g x).
Proof.
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.
Proof.
End ae_eq_integral.
Arguments ae_eq_integral {d T R mu D} g.
Local Open Scope ereal_scope.
Lemma
integral_cst
d
(
T
: measurableType d) (
R
: realType)
(
mu
: {measure set T -> \bar R}) (
D
: set T)
: d.
-measurable D ->
forall
r,
\int[mu]_(
x
in D) (
cst r)
x = r * mu D.
Proof.
Add Search Blacklist "integral_cstr" "integral_csty" "integral_cstNy".
Lemma
le_integral_comp_abse
d
(
T
: measurableType d) (
R
: realType)
(
mu
: {measure set T -> \bar R}) (
D
: set T) (
mD
: measurable D)
(
g
: T -> \bar R)
a
(
f
: \bar R -> \bar R) (
mf
: measurable_fun setT f)
(
f0
: forall
r,
0 <= r -> 0 <= f r)
(
f_nd
: {in `[0, +oo[%classic &, {homo f :
x
y
/ x <= y}})
:
measurable_fun D g -> (
0 < a)
%R ->
(
f a%:E)
* mu (
D `&` [set
x
| (
`|g x| >= a%:E)
%E])
<= \int[mu]_(
x
in D)
f `|g x|.
Proof.
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.
Proof.
move=> [N [mN N0 subN]] mf B mB mD.
apply: (
measurability (
ErealGenOInfty.measurableE R))
=> // _ [_ [x ->] <-].
rewrite [X in measurable X](
_ : _ = D `&` ~` N `&` (
f @^-1` `]x%:E, +oo[)
`|` (
D `&` N `&` g @^-1` `]x%:E, +oo[))
; last first.
apply/seteqP; split=> [y /= [Dy gyxoo]|y /= [[[Dy Ny] fyxoo]|]].
- have [->|fgy] := eqVneq (
f y) (
g y).
have [yN|yN] := boolP (
y \in N).
by right; split => //; rewrite inE in yN.
by left; split => //; rewrite notin_set in yN.
by right; split => //; split => //; apply: subN => /= /(
_ Dy)
; exact/eqP.
- split => //; have [<-//|fgy] := eqVneq (
f y) (
g y).
by exfalso; apply/Ny/subN => /= /(
_ Dy)
; exact/eqP.
- by move=> [[]].
apply: measurableU.
- rewrite setIAC; apply: measurableI; last exact/measurableC.
exact/mf/emeasurable_itv.
- by apply: cmu; exists N; split => //; rewrite setIAC; apply: subIset; right.
Qed.
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
Proof.
Let
mf2
: measurable_fun D f2
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
Lemma
integral_fune_fin_num
(
f
: T -> \bar R)
:
mu.
-integrable D f -> \int[mu]_(
x
in D)
f x \is a fin_num.
Proof.
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.
Proof.
Lemma
summable_integral_dirac
(
a
: nat -> \bar R)
: summable setT a ->
\sum_(
n
<oo)
`|\int[\d_ n]_x a x| < +oo.
Proof.
Lemma
integral_count
(
a
: nat -> \bar R)
: summable setT a ->
\int[counting]_t (
a t)
= \sum_(
k
<oo) (
a k).
Proof.
Lemma
ge0_integral_count
(
a
: nat -> \bar R)
: (
forall
k,
0 <= a k)
->
\int[counting]_t (
a t)
= \sum_(
k
<oo) (
a k).
Proof.
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).
Proof.
Lemma
integrable_summable
(
F
: (
set T)
^nat) (
g
: T -> \bar R)
:
trivIset setT F -> (
forall
k,
measurable (
F k))
->
mu.
-integrable (
\bigcup_k F k)
g ->
summable [set: nat] (
fun
i
=> \int[mu]_(
x
in F i)
g x).
Proof.
Lemma
integral_bigcup
(
F
: (
set _)
^nat) (
g
: T -> \bar R)
:
trivIset setT F -> (
forall
k,
measurable (
F k))
->
mu.
-integrable (
\bigcup_k F k)
g ->
(
\int[mu]_(
x
in \bigcup_i F i)
g x = \sum_(
i
<oo)
\int[mu]_(
x
in F i)
g x)
%E.
Proof.
End subadditive_countable.
Section
dominated_convergence_lemma
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variables (
mu
: {measure set T -> \bar R}) (
D
: set T) (
mD
: measurable D).
Variables (
f_
: (
T -> \bar R)
^nat) (
f
: T -> \bar R) (
g
: T -> \bar R).
Hypothesis
mf_
: forall
n,
measurable_fun D (
f_ n).
Hypothesis
f_f
: forall
x,
D x -> f_ ^~ x --> f x.
Hypothesis
fing
: forall
x,
D x -> g x \is a fin_num.
Hypothesis
ig
: mu.
-integrable D g.
Hypothesis
absfg
: forall
n
x,
D x -> `|f_ n x| <= g x.
Let
g0
x
: D x -> 0 <= g x.
Proof.
Let
mf
: measurable_fun D f.
Proof.
Local Lemma
dominated_integrable
: mu.
-integrable D f.
Proof.
Let
g_
n
x
:= `|f_ n x - f x|.
Let
cvg_g_
x
: D x -> g_ ^~ x --> 0.
Proof.
Let
gg_
n
x
: D x -> 0 <= 2%:E * g x - g_ n x.
Proof.
Let
mgg
n
: measurable_fun D (
fun
x
=> 2%:E * g x - g_ n x).
Proof.
Let
gg_ge0
n
x
: D x -> 0 <= 2%:E * g x - g_ n x.
Proof.
by move=> Dx; rewrite gg_. Qed.
Local Lemma
dominated_cvg0
: [sequence \int[mu]_(
x
in D)
g_ n x]_n --> 0.
Proof.
Local Lemma
dominated_cvg
:
(
fun
n
=> \int[mu]_(
x
in D)
f_ n x)
--> \int[mu]_(
x
in D)
f x.
Proof.
End dominated_convergence_lemma.
Arguments dominated_integrable {d T R mu D} _ f_ f g.
Section
dominated_convergence_theorem
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variables (
mu
: {measure set T -> \bar R}) (
D
: set T) (
mD
: measurable D).
Variables (
f_
: (
T -> \bar R)
^nat) (
f
: T -> \bar R) (
g
: T -> \bar R).
Hypothesis
mf_
: forall
n,
measurable_fun D (
f_ n).
Hypothesis
mf
: measurable_fun D f.
Hypothesis
f_f
: {ae mu, forall
x,
D x -> f_ ^~ x --> f x}.
Hypothesis
ig
: mu.
-integrable D g.
Hypothesis
f_g
: {ae mu, forall
x
n,
D x -> `|f_ n x| <= g x}.
Let
g_
n
x
:= `|f_ n x - f x|.
Theorem
dominated_convergence
: [/\ mu.
-integrable D f,
[sequence \int[mu]_(
x
in D) (
g_ n x)
]_n --> 0 &
[sequence \int[mu]_(
x
in D) (
f_ n x)
]_n --> \int[mu]_(
x
in D) (
f x)
].
Proof.
End dominated_convergence_theorem.
Section
ae_ge0_le_integral
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variable
mu
: {measure set T -> \bar R}.
Variables (
D
: set T) (
mD
: measurable D) (
f1
f2
: T -> \bar R).
Hypothesis
f10
: forall
x,
D x -> 0 <= f1 x.
Hypothesis
mf1
: measurable_fun D f1.
Hypothesis
f20
: forall
x,
D x -> 0 <= f2 x.
Hypothesis
mf2
: measurable_fun D f2.
Lemma
ae_ge0_le_integral
: {ae mu, forall
x,
D x -> f1 x <= f2 x} ->
\int[mu]_(
x
in D)
f1 x <= \int[mu]_(
x
in D)
f2 x.
Proof.
End ae_ge0_le_integral.
Section
integral_bounded
.
Context
d
{T : measurableType d} {R : realType}.
Variable
mu
: {measure set T -> \bar R}.
Local Open Scope ereal_scope.
Lemma
integral_le_bound
(
D
: set T) (
f
: T -> \bar R) (
M
: \bar R)
:
measurable D -> measurable_fun D f -> 0 <= M ->
{ae mu, forall
x,
D x -> `|f x| <= M} ->
\int[mu]_(
x
in D)
`|f x| <= M * mu D.
Proof.
End integral_bounded.
Arguments integral_le_bound {d T R mu D f} M.
Section
integral_ae_eq
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType) (
mu
: {measure set T -> \bar R}).
Let
integral_measure_lt
(
D
: set T) (
mD
: measurable D) (
g
f
: T -> \bar R)
:
mu.
-integrable D f -> mu.
-integrable D g ->
(
forall
E,
E `<=` D -> measurable E ->
\int[mu]_(
x
in E)
f x = \int[mu]_(
x
in E)
g x)
->
mu (
D `&` [set
x
| g x < f x])
= 0.
Proof.
Lemma
integral_ae_eq
(
D
: set T) (
mD
: measurable D) (
g
f
: T -> \bar R)
:
mu.
-integrable D f -> measurable_fun D g ->
(
forall
E,
E `<=` D -> measurable E ->
\int[mu]_(
x
in E)
f x = \int[mu]_(
x
in E)
g x)
->
ae_eq mu D f g.
Proof.
End integral_ae_eq.
Product measure
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).
Proof.
Lemma
measurable_ysection
A
y
: measurable A -> measurable (
ysection A y).
Proof.
End measurable_section.
Section
ndseq_closed_B
.
Context
d1
d2
(
T1
: measurableType d1) (
T2
: measurableType d2) (
R
: realType).
Implicit Types A : set (
T1 * T2).
Section
xsection
.
Variables (
pt2
: T2) (
m2
: T1 -> {measure set T2 -> \bar R}).
Let
phi
A
x
:= m2 x (
xsection A x).
Let
B
:= [set
A
| measurable A /\ measurable_fun setT (
phi A)
].
Lemma
xsection_ndseq_closed
: ndseq_closed B.
Proof.
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.
Proof.
End ysection.
End ndseq_closed_B.
Section
measurable_prod_subset
.
Context
d1
d2
(
T1
: measurableType d1) (
T2
: measurableType d2) (
R
: realType).
Implicit Types A : set (
T1 * T2).
Section
xsection
.
Variable (
m2
: {measure set T2 -> \bar R}) (
D
: set T2) (
mD
: measurable D).
Let
m2D
:= mrestr m2 mD.
HB.instance Definition _ := Measure.on m2D.
Let
phi
A
:= m2D \o xsection A.
Let
B
:= [set
A
| measurable A /\ measurable_fun setT (
phi A)
].
Lemma
measurable_prod_subset_xsection
(
m2D_bounded
: exists
M,
forall
X,
measurable X -> (
m2D X < M%:E)
%E)
:
measurable `<=` B.
Proof.
End xsection.
Section
ysection
.
Variable (
m1
: {measure set T1 -> \bar R}) (
D
: set T1) (
mD
: measurable D).
Let
m1D
:= mrestr m1 mD.
HB.instance Definition _ := Measure.on m1D.
Let
psi
A
:= m1D \o ysection A.
Let
B
:= [set
A
| measurable A /\ measurable_fun setT (
psi A)
].
Lemma
measurable_prod_subset_ysection
(
m1_bounded
: exists
M,
forall
X,
measurable X -> (
m1D X < M%:E)
%E)
:
measurable `<=` B.
Proof.
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).
Proof.
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).
Proof.
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.
Proof.
Let
pm1_ge0
A
: 0 <= (
m1 \x m2)
A.
Proof.
by apply: integral_ge0 => // *; exact/measure_ge0/measurable_xsection.
Qed.
Let
pm1_sigma_additive
: semi_sigma_additive (
m1 \x m2).
Proof.
HB.instance Definition _ := isMeasure.Build _ _ _ (
m1 \x m2)
pm10 pm1_ge0 pm1_sigma_additive.
End product_measure1.
Section
product_measure1E
.
Local Open Scope ereal_scope.
Context
d1
d2
(
T1
: measurableType d1) (
T2
: measurableType d2) (
R
: realType).
Variable
m1
: {measure set T1 -> \bar R}.
Variable
m2
: {sigma_finite_measure set T2 -> \bar R}.
Implicit Types A : set (
T1 * T2).
Lemma
product_measure1E
(
A1
: set T1) (
A2
: set T2)
:
measurable A1 -> measurable A2 -> (
m1 \x m2) (
A1 `*` A2)
= m1 A1 * m2 A2.
Proof.
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})
:
(
forall
A1
A2,
measurable A1 -> measurable A2 ->
m' (
A1 `*` A2)
= m1 A1 * m2 A2)
->
forall
X
: set (
T1 * T2)
, measurable X -> (
m1 \x m2)
X = m' X.
Proof.
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.
Proof.
Let
pm2_ge0
A
: 0 <= (
m1 \x^ m2)
A.
Proof.
by apply: integral_ge0 => // *; exact/measure_ge0/measurable_ysection.
Qed.
Let
pm2_sigma_additive
: semi_sigma_additive (
m1 \x^ m2).
Proof.
HB.instance Definition _ := isMeasure.Build _ _ _ (
m1 \x^ m2)
pm20 pm2_ge0 pm2_sigma_additive.
End product_measure2.
Section
product_measure2E
.
Local Open Scope ereal_scope.
Context
d1
d2
(
T1
: measurableType d1) (
T2
: measurableType d2) (
R
: realType).
Variable
m1
: {sigma_finite_measure set T1 -> \bar R}.
Variable
m2
: {measure set T2 -> \bar R}.
Lemma
product_measure2E
(
A1
: set T1) (
A2
: set T2)
(
mA1
: measurable A1) (
mA2
: measurable A2)
:
(
m1 \x^ m2) (
A1 `*` A2)
= m1 A1 * m2 A2.
Proof.
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).
Proof.
Let
sfun_dense_L1_pos
(
f
: T -> \bar R)
:
mu.
-integrable E f -> (
forall
x,
E x -> 0 <= f x)
->
exists
g_
: {sfun T >-> R}^nat,
[/\ forall
n,
mu.
-integrable E (
EFin \o g_ n)
,
forall
x,
E x -> EFin \o g_^~ x @ \oo --> f x &
(
fun
n
=> \int[mu]_(
z
in E)
`|f z - (
g_ n z)
%:E|)
--> 0].
Proof.
Lemma
approximation_sfun_integrable
(
f
: T -> \bar R)
:
mu.
-integrable E f ->
exists
g_
: {sfun T >-> R}^nat,
[/\ forall
n,
mu.
-integrable E (
EFin \o g_ n)
,
forall
x,
E x -> EFin \o g_^~ x @ \oo --> f x &
(
fun
n
=> \int[mu]_(
z
in E)
`|f z - (
g_ n z)
%:E|)
--> 0].
Proof.
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.
Proof.
Lemma
continuous_compact_integrable
(
f
: R -> R^o) (
A
: set R^o)
:
compact A -> {within A, continuous f} -> mu.
-integrable A (
EFin \o f).
Proof.
Lemma
approximation_continuous_integrable
(
E
: set R) (
f
: R -> R^o)
:
measurable E -> mu E < +oo -> mu.
-integrable E (
EFin \o f)
->
exists
g_
: (
rT -> rT)
^nat,
[/\ forall
n,
continuous (
g_ n)
,
forall
n,
mu.
-integrable E (
EFin \o g_ n)
&
(
fun
n
=> \int[mu]_(
z
in E)
`|(
f z - g_ n z)
%:E|)
--> 0].
Proof.
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.
Proof.
Lemma
indic_fubini_tonelli_G_ge0
x
: 0 <= G x.
Proof.
Lemma
indic_fubini_tonelli_FE
: F = m2 \o xsection A.
Proof.
Lemma
indic_fubini_tonelli_GE
: G = m1 \o ysection A.
Proof.
Lemma
indic_measurable_fun_fubini_tonelli_F
: measurable_fun setT F.
Proof.
Lemma
indic_measurable_fun_fubini_tonelli_G
: measurable_fun setT G.
Proof.
Lemma
indic_fubini_tonelli1
: \int[m1 \x m2]_z (
f z)
%:E = \int[m1]_x F x.
Proof.
Lemma
indic_fubini_tonelli2
: \int[m1 \x^ m2]_z (
f z)
%:E = \int[m2]_y G y.
Proof.
Lemma
indic_fubini_tonelli
: \int[m1]_x F x = \int[m2]_y G y.
Proof.
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).
Proof.
Lemma
sfun_measurable_fun_fubini_tonelli_F
: measurable_fun setT F.
Proof.
Lemma
sfun_fubini_tonelli_GE
: G = fun
y
=>
\sum_(
k
\in range f)
k%:E * m1 (
ysection (
f @^-1` [set k])
y).
Proof.
Lemma
sfun_measurable_fun_fubini_tonelli_G
: measurable_fun setT G.
Proof.
Let
EFinf
x
: (
f x)
%:E =
\sum_(
k
\in range f)
k%:E * (
\1_(
f @^-1` [set k])
x)
%:E.
Proof.
Lemma
sfun_fubini_tonelli1
: \int[m1 \x m2]_z (
f z)
%:E = \int[m1]_x F x.
Proof.
Lemma
sfun_fubini_tonelli2
: \int[m1 \x^ m2]_z (
f z)
%:E = \int[m2]_y G y.
Proof.
Lemma
sfun_fubini_tonelli
:
\int[m1 \x m2]_z (
f z)
%:E = \int[m1 \x^ m2]_z (
f z)
%:E.
Proof.
End sfun_fubini_tonelli.
Section
fubini_tonelli
.
Variable
f
: T1 * T2 -> \bar R.
Hypothesis
mf
: measurable_fun setT f.
Hypothesis
f0
: forall
x,
0 <= f x.
Let
T
:= [the measurableType _ of T1 * T2 : Type].
Let
F
:= fubini_F m2 f.
Let
G
:= fubini_G m1 f.
Let
F_
(
g
: {nnsfun T >-> R}^nat)
n
x
:= \int[m2]_y (
g n (
x, y))
%:E.
Let
G_
(
g
: {nnsfun T >-> R}^nat)
n
y
:= \int[m1]_x (
g n (
x, y))
%:E.
Lemma
measurable_fun_fubini_tonelli_F
: measurable_fun setT F.
Proof.
Lemma
measurable_fun_fubini_tonelli_G
: measurable_fun setT G.
Proof.
Lemma
fubini_tonelli1
: \int[m1 \x m2]_z f z = \int[m1]_x F x.
Proof.
Lemma
fubini_tonelli2
: \int[m1 \x m2]_z f z = \int[m2]_y G y.
Proof.
Lemma
fubini_tonelli
:
\int[m1]_x \int[m2]_y f (
x, y)
= \int[m2]_y \int[m1]_x f (
x, y).
Proof.
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
Proof.
Lemma
fubini1a
:
(
m1 \x m2).
-integrable setT f <-> \int[m1]_x \int[m2]_y `|f (
x, y)
| < +oo.
Proof.
Lemma
fubini1b
:
(
m1 \x m2).
-integrable setT f <-> \int[m2]_y \int[m1]_x `|f (
x, y)
| < +oo.
Proof.
Let
measurable_fun1
: measurable_fun setT (
fun
x
=> \int[m2]_y `|f (
x, y)
|).
Proof.
Let
measurable_fun2
: measurable_fun setT (
fun
y
=> \int[m1]_x `|f (
x, y)
|).
Proof.
Lemma
ae_integrable1
:
{ae m1, forall
x,
m2.
-integrable setT (
fun
y
=> f (
x, y))
}.
Proof.
Lemma
ae_integrable2
:
{ae m2, forall
y,
m1.
-integrable setT (
fun
x
=> f (
x, y))
}.
Proof.
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
Proof.
Let
measurable_Fplus
: measurable_fun setT Fplus.
Proof.
Let
measurable_Fminus
: measurable_fun setT Fminus.
Proof.
Lemma
measurable_fubini_F
: measurable_fun setT F.
Proof.
Let
integrable_Fplus
: m1.
-integrable setT Fplus.
Proof.
Let
integrable_Fminus
: m1.
-integrable setT Fminus.
Proof.
Lemma
integrable_fubini_F
: m1.
-integrable setT F.
Proof.
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
Proof.
Let
measurable_Gplus
: measurable_fun setT Gplus.
Proof.
Let
measurable_Gminus
: measurable_fun setT Gminus.
Proof.
Lemma
measurable_fubini_G
: measurable_fun setT G.
Proof.
Let
integrable_Gplus
: m2.
-integrable setT Gplus.
Proof.
Let
integrable_Gminus
: m2.
-integrable setT Gminus.
Proof.
Lemma
fubini1
: \int[m1]_x F x = \int[m1 \x m2]_z f z.
Proof.
Lemma
fubini2
: \int[m2]_x G x = \int[m1 \x m2]_z f z.
Proof.
Theorem
Fubini
:
\int[m1]_x \int[m2]_y f (
x, y)
= \int[m2]_y \int[m1]_x f (
x, y).
Proof.
End fubini.
Section
sfinite_fubini
.
Local Open Scope ereal_scope.
Context
d
d'
(
X
: measurableType d) (
Y
: measurableType d') (
R
: realType).
Variables (
m1
: {sfinite_measure set X -> \bar R}).
Variables (
m2
: {sfinite_measure set Y -> \bar R}).
Variables (
f
: X * Y -> \bar R) (
f0
: forall
xy,
0 <= f xy).
Hypothesis
mf
: measurable_fun setT f.
Lemma
sfinite_Fubini
:
\int[m1]_x \int[m2]_y f (
x, y)
= \int[m2]_y \int[m1]_x f (
x, y).
Proof.
End sfinite_fubini.
Arguments sfinite_Fubini {d d' X Y R} m1 m2 f.
Section
lebesgue_differentiation_continuous
.
Context (
rT
: realType).
Let
mu
:= [the measure _ _ of @lebesgue_measure rT].
Let
R
:= [the measurableType _ of measurableTypeR rT].
Let
ballE
(
x
: R) (
r
: {posnum rT})
:
ball x r%:num = `](
x - r%:num)
, (
x + r%:num)
[%classic :> set rT.
Proof.
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).
Proof.
End lebesgue_differentiation_continuous.
Section
locally_integrable
.
Context {R : realType}.
Implicit Types (
D : set R) (
f g : R -> R).
Local Open Scope ereal_scope.
Local Notation
mu
:= lebesgue_measure.
Definition
locally_integrable
D
f
:= [/\ measurable_fun D f, open D &
forall
K,
K `<=` D -> compact K -> \int[mu]_(
x
in K)
`|f x|%:E < +oo].
Lemma
integrable_locally
D
f
: open D ->
mu.
-integrable D (
EFin \o f)
-> locally_integrable D f.
Proof.
Lemma
locally_integrableN
D
f
:
locally_integrable D f -> locally_integrable D (
\- f)
%R.
Proof.
Lemma
locally_integrableD
D
f
g
:
locally_integrable D f -> locally_integrable D g ->
locally_integrable D (
f \+ g)
%R.
Proof.
Lemma
locally_integrableB
D
f
g
:
locally_integrable D f -> locally_integrable D g ->
locally_integrable D (
f \- g)
%R.
Proof.
End locally_integrable.
Section
iavg
.
Context {R : realType}.
Implicit Types (
D A : set R) (
f g : R -> R).
Local Open Scope ereal_scope.
Local Notation
mu
:= lebesgue_measure.
Definition
iavg
f
A
:= (
fine (
mu A))
^-1%:E * \int[mu]_(
y
in A)
`| (
f y)
%:E |.
Lemma
iavg0
f
: iavg f set0 = 0.
Proof.
Lemma
iavg_ge0
f
A
: 0 <= iavg f A.
Proof.
Lemma
iavg_restrict
f
D
A
: measurable D -> measurable A ->
iavg (
f \_ D)
A = ((
fine (
mu A))
^-1)
%:E * \int[mu]_(
y
in D `&` A)
`|f y|%:E.
Proof.
Lemma
iavgD
f
g
A
: measurable A -> mu A < +oo ->
measurable_fun A f -> measurable_fun A g ->
iavg (
f \+ g)
%R A <= iavg f A + iavg g A.
Proof.
End iavg.
Section
hardy_littlewood
.
Context {R : realType}.
Notation
mu
:= (
@lebesgue_measure R).
Implicit Types (
D : set R) (
f : R -> R).
Local Open Scope ereal_scope.
Definition
HL_maximal
f
(
x
: R)
: \bar R :=
ereal_sup [set iavg f (
ball x r)
|
r
in `]0, +oo[%classic%R].
Local Notation
HL
:= HL_maximal.
Lemma
HL_maximal_ge0
f
D
: locally_integrable D f ->
forall
x,
0 <= HL (
f \_ D)
x.
Proof.
Lemma
HL_maximalT_ge0
f
: locally_integrable setT f -> forall
x,
0 <= HL f x.
Proof.
by move=> + x => /HL_maximal_ge0 /(
_ x)
; rewrite patch_setT. Qed.
Let
locally_integrable_ltbally
(
f
: R -> R) (
x
r
: R)
:
locally_integrable setT f -> \int[mu]_(
y
in ball x r)
`|(
f y)
%:E| < +oo.
Proof.
Lemma
lower_semicontinuous_HL_maximal
f
:
locally_integrable setT f -> lower_semicontinuous (
HL f).
Proof.
Lemma
measurable_HL_maximal
f
:
locally_integrable setT f -> measurable_fun setT (
HL f).
Proof.
Let
norm1
D
f
:= \int[mu]_(
y
in D)
`|(
f y)
%:E|.
Lemma
maximal_inequality
f
c
:
locally_integrable setT f -> (
0 < c)
%R ->
mu [set
x
| HL f x > c%:E] <= (
3%:R / c)
%:E * norm1 setT f.
Proof.
End hardy_littlewood.