From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp Require Import finmap fingroup perm rat.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop.
Require Import reals ereal signed topology numfun normedtype.
From HB Require Import structures.
Require Import sequences esum measure real_interval realfun exp.
Require Export lebesgue_stieltjes_measure.
# Lebesgue Measure
This file contains a formalization of the Lebesgue measure using the
Measure Extension theorem from measure.v, further develops the theory of
of measurable functions, and prove properties of the Lebesgue measure
such as Vitali's covering lemma (infinite case), i.e., given a Vitali
cover $V$ of $A$, there exists a countable subcollection $D \subseteq V$
of pairwise disjoint closed balls such that
$\lambda(A \setminus \bigcup_k D_k) = 0$.
Main references:
- Daniel Li, Intégration et applications, 2016
- Achim Klenke, Probability Theory 2nd edition, 2014
```
lebesgue_measure == the Lebesgue measure
ps_infty == inductive definition of the powerset
{0, {-oo}, {+oo}, {-oo,+oo}}
emeasurable G == sigma-algebra over \bar R built out of the
measurables G of a sigma-algebra over R
elebesgue_measure == the Lebesgue measure extended to \bar R
```
The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens provide proofs
of equivalence between the sigma-algebra generated by list of intervals
and the sigma-algebras generated by open rays, closed rays, and open
intervals.
The modules ErealGenOInfty, ErealGenCInfty, ErealGenInftyO provide proofs
of equivalence between emeasurable and the sigma-algebras generated open
rays and closed rays.
```
vitali_cover A B V == V is a Vitali cover of A, here B is a
collection of non-empty closed balls
```
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.
Module
LebesgueMeasure
.
Section
hlength
.
Context {R : realType}.
Local Open Scope ereal_scope.
Implicit Types i j : interval R.
Definition
hlength
(
A
: set (
ocitv_type R))
: \bar R :=
let
i
:= Rhull A in i.
2 - i.
1.
Lemma
hlength0
: hlength (
set0 : set R)
= 0.
Proof.
Lemma
hlength_singleton
(
r
: R)
: hlength `[r, r] = 0.
Proof.
Lemma
hlength_setT
: hlength setT = +oo%E :> \bar R.
Proof.
by rewrite /hlength RhullT. Qed.
Lemma
hlength_itv
i
: hlength [set` i] = if i.
2 > i.
1 then i.
2 - i.
1 else 0.
Proof.
Lemma
hlength_finite_fin_num
i
: neitv i -> hlength [set` i] < +oo ->
((
i.
1 : \bar R)
\is a fin_num)
/\ ((
i.
2 : \bar R)
\is a fin_num).
Proof.
Lemma
finite_hlength_itv
i
: neitv i -> hlength [set` i] < +oo ->
hlength [set` i] = (
fine i.
2)
%:E - (
fine i.
1)
%:E.
Proof.
Lemma
hlength_infty_bnd
b
r
:
hlength [set` Interval -oo%O (
BSide b r)
] = +oo :> \bar R.
Proof.
Lemma
hlength_bnd_infty
b
r
:
hlength [set` Interval (
BSide b r)
+oo%O] = +oo :> \bar R.
Proof.
Lemma
infinite_hlength_itv
i
: hlength [set` i] = +oo ->
(
exists
s
r,
i = Interval -oo%O (
BSide s r)
\/ i = Interval (
BSide s r)
+oo%O)
\/ i = `]-oo, +oo[.
Proof.
rewrite hlength_itv; case: i => -[ba a|[]] [bb b|[]] //= => [|_|_|].
- by case: ifPn.
- by left; exists ba, a; right.
- by left; exists bb, b; left.
- by right.
Qed.
Lemma
hlength_itv_ge0
i
: 0 <= hlength [set` i].
Proof.
Lemma
hlength_Rhull
(
A
: set R)
: hlength [set` Rhull A] = hlength A.
Proof.
Lemma
le_hlength_itv
i
j
: {subset i <= j} -> hlength [set` i] <= hlength [set` j].
Proof.
Lemma
le_hlength
: {homo hlength :
A
B
/ (
A `<=` B)
>-> A <= B}.
Proof.
Lemma
hlength_ge0
I
: (
0 <= hlength I)
%E.
Proof.
End hlength.
#[local] Hint Extern 0 (
0%:E <= hlength _)
=> solve[apply: hlength_ge0] : core.
Section
hlength_extension
.
Context {R : realType}.
Notation
hlength
:= (
@hlength R).
Lemma
hlength_semi_additive
: semi_additive hlength.
Proof.
move=> /= I n /(
_ _)
/cid2-/all_sig[b]/all_and2[_]/(
_ _)
/esym-/funext {I}->.
move=> Itriv [[/= a1 a2] _] /esym /[dup] + ->.
rewrite hlength_itv ?lte_fin/= -EFinB.
case: ifPn => a12; last first.
pose I
i
:= `](
b i).
1, (
b i).
2]%classic.
rewrite set_itv_ge//= -(
bigcup_mkord _ I)
/I => /bigcup0P I0.
by under eq_bigr => i _ do rewrite I0//= hlength0; rewrite big1.
set A := `]a1, a2]%classic.
rewrite -bigcup_pred; set P := xpredT; rewrite (
eq_bigl P)
//.
move: P => P; have [p] := ubnP #|P|; elim: p => // p IHp in P a2 a12 A *.
rewrite ltnS => cP /esym AE.
have : A a2 by rewrite /A /= in_itv/= lexx andbT.
rewrite AE/= => -[i /= Pi] a2bi.
case: (
boolP ((
b i).
1 < (
b i).
2))
=> bi; last by rewrite itv_ge in a2bi.
have {}a2bi : a2 = (
b i).
2.
apply/eqP; rewrite eq_le (
itvP a2bi)
/=.
suff: A (
b i).
2 by move=> /itvP->.
by rewrite AE; exists i=> //=; rewrite in_itv/= lexx andbT.
rewrite {a2}a2bi in a12 A AE *.
rewrite (
bigD1 i)
//= hlength_itv ?lte_fin/= bi !EFinD -addeA.
congr (
_ + _)
%E; apply/eqP; rewrite addeC -sube_eq// 1?adde_defC//.
rewrite ?EFinN oppeK addeC; apply/eqP.
case: (
eqVneq a1 (
b i).
1)
=> a1bi.
rewrite {a1}a1bi in a12 A AE {IHp} *; rewrite subee ?big1// => j.
move=> /andP[Pj Nji]; rewrite hlength_itv ?lte_fin/=; case: ifPn => bj//.
exfalso; have /trivIsetP/(
_ j i I I Nji)
:= Itriv.
pose m := ((
b j).
1 + (
b j).
2)
/ 2%:R.
have mbj : `](
b j).
1, (
b j).
2]%classic m.
by rewrite /= !in_itv/= ?(
midf_lt, midf_le)
//= ltW.
rewrite -subset0 => /(
_ m)
; apply; split=> //.
by suff: A m by []; rewrite AE; exists j => //.
have a1b2 j : P j -> (
b j).
1 < (
b j).
2 -> a1 <= (
b j).
2.
move=> Pj bj; suff /itvP-> : A (
b j).
2 by [].
by rewrite AE; exists j => //=; rewrite ?in_itv/= bj//=.
have a1b j : P j -> (
b j).
1 < (
b j).
2 -> a1 <= (
b j).
1.
move=> Pj bj; case: ltP=> // bj1a.
suff : A a1 by rewrite /A/= in_itv/= ltxx.
by rewrite AE; exists j; rewrite //= in_itv/= bj1a//= a1b2.
have bbi2 j : P j -> (
b j).
1 < (
b j).
2 -> (
b j).
2 <= (
b i).
2.
move=> Pj bj; suff /itvP-> : A (
b j).
2 by [].
by rewrite AE; exists j => //=; rewrite ?in_itv/= bj//=.
apply/IHp.
- by rewrite lt_neqAle a1bi/= a1b.
- rewrite (
leq_trans _ cP)
// -(
cardID (
pred1 i)
P).
rewrite [X in (
_ < X + _)
%N](
@eq_card _ _ (
pred1 i))
; last first.
by move=> j; rewrite !inE andbC; case: eqVneq => // ->.
rewrite ?card1 ?ltnS// subset_leq_card//.
by apply/fintype.
subsetP => j; rewrite -topredE/= !inE andbC.
apply/seteqP; split=> /= [x [j/= /andP[Pj Nji]]|x/= xabi].
case: (
boolP ((
b j).
1 < (
b j).
2))
=> bj; last by rewrite itv_ge.
apply: subitvP; rewrite subitvE ?bnd_simp a1b//= leNgt.
have /trivIsetP/(
_ j i I I Nji)
:= Itriv.
rewrite -subset0 => /(
_ (
b j).
2)
; apply: contra_notN => /= bi1j2.
by rewrite !in_itv/= bj !lexx bi1j2 bbi2.
have: A x.
rewrite /A/= in_itv/= (
itvP xabi)
/= ltW//.
by rewrite (
le_lt_trans _ bi)
?(
itvP xabi).
rewrite AE => -[j /= Pj xbj].
exists j => //=.
apply/andP; split=> //; apply: contraTneq xbj => ->.
by rewrite in_itv/= le_gtF// (
itvP xabi).
Qed.
HB.instance Definition _ := isContent.Build _ _ R
hlength hlength_ge0 hlength_semi_additive.
Hint Extern 0 ((
_ .-ocitv).
-measurable _)
=> solve [apply: is_ocitv] : core.
Lemma
hlength_sigma_sub_additive
:
sigma_sub_additive (
hlength : set (
ocitv_type R)
-> _).
Proof.
HB.instance Definition _ := Content_SubSigmaAdditive_isMeasure.Build _ _ _
hlength hlength_sigma_sub_additive.
Lemma
hlength_sigma_finite
: sigma_finite setT (
hlength : set (
ocitv_type R)
-> _).
Proof.
Definition
lebesgue_measure
:= measure_extension [the measure _ _ of hlength].
HB.instance Definition _ := Measure.on lebesgue_measure.
Let
sigmaT_finite_lebesgue_measure
: sigma_finite setT lebesgue_measure.
Proof.
exact/measure_extension_sigma_finite/hlength_sigma_finite. Qed.
HB.instance Definition _ := @isSigmaFinite.
Build _ _ _
lebesgue_measure sigmaT_finite_lebesgue_measure.
End hlength_extension.
End LebesgueMeasure.
Definition
lebesgue_measure
{R : realType} :
set [the measurableType _.
-sigma of
salgebraType R.
-ocitv.
-measurable] -> \bar R :=
[the measure _ _ of lebesgue_stieltjes_measure [the cumulative _ of idfun]].
HB.instance Definition _ (
R
: realType)
:= Measure.on (
@lebesgue_measure R).
HB.instance Definition _ (
R
: realType)
:=
SigmaFiniteContent.on (
@lebesgue_measure R).
Section
ps_infty
.
Context {T : Type}.
Local Open Scope ereal_scope.
Inductive
ps_infty
: set \bar T -> Prop :=
|
ps_infty0
: ps_infty set0
|
ps_ninfty
: ps_infty [set -oo]
|
ps_pinfty
: ps_infty [set +oo]
|
ps_inftys
: ps_infty [set -oo; +oo].
Lemma
ps_inftyP
(
A
: set \bar T)
: ps_infty A <-> A `<=` [set -oo; +oo].
Proof.
split => [[]//|Aoo].
by have [] := subset_set2 Aoo; move=> ->; constructor.
Qed.
Lemma
setCU_Efin
(
A
: set T) (
B
: set \bar T)
: ps_infty B ->
~` (
EFin @` A)
`&` ~` B = (
EFin @` ~` A)
`|` (
[set -oo%E; +oo%E] `&` ~` B).
Proof.
End ps_infty.
Section
salgebra_ereal
.
Variables (
R
: realType) (
G
: set (
set R)).
Let
measurableR
: set (
set R)
:= G.
-sigma.
-measurable.
Definition
emeasurable
: set (
set \bar R)
:=
[set EFin @` A `|` B |
A
in measurableR &
B
in ps_infty].
Lemma
emeasurable0
: emeasurable set0.
Proof.
Lemma
emeasurableC
(
X
: set \bar R)
: emeasurable X -> emeasurable (
~` X).
Proof.
Lemma
bigcupT_emeasurable
(
F
: (
set \bar R)
^nat)
:
(
forall
i,
emeasurable (
F i))
-> emeasurable (
\bigcup_i (
F i)).
Proof.
Definition
ereal_isMeasurable
:
isMeasurable default_measure_display (
\bar R)
:=
isMeasurable.Build _ _ (
Pointed.class _)
emeasurable0 emeasurableC bigcupT_emeasurable.
End salgebra_ereal.
Section
puncture_ereal_itv
.
Variable
R
: realDomainType.
Implicit Types (
y : R) (
b : bool).
Local Open Scope ereal_scope.
Lemma
punct_eitv_bndy
b
y
: [set` Interval (
BSide b y%:E)
+oo%O] =
EFin @` [set` Interval (
BSide b y)
+oo%O] `|` [set +oo].
Proof.
rewrite predeqE => x; split; rewrite /= in_itv andbT.
- move: x => [x| |] yxb; [|by right|by case: b yxb].
by left; exists x => //; rewrite in_itv /= andbT; case: b yxb.
- move=> [[r]|->].
+ by rewrite in_itv /= andbT => yxb <-; case: b yxb.
+ by case: b => /=; rewrite ?(
ltry, leey).
Qed.
Lemma
punct_eitv_Nybnd
b
y
: [set` Interval -oo%O (
BSide b y%:E)
] =
[set -oo%E] `|` EFin @` [set
x
| x \in Interval -oo%O (
BSide b y)
].
Proof.
rewrite predeqE => x; split; rewrite /= in_itv.
- move: x => [x| |] yxb; [|by case: b yxb|by left].
by right; exists x => //; rewrite in_itv /= andbT; case: b yxb.
- move=> [->|[r]].
+ by case: b => /=; rewrite ?(
ltNyr, leNye).
+ by rewrite in_itv /= => yxb <-; case: b yxb.
Qed.
Lemma
punct_eitv_setTR
: range (
@EFin R)
`|` [set +oo] = [set~ -oo].
Proof.
rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //.
by move=> [x| |] //= _; [left; exists x|right].
Qed.
Lemma
punct_eitv_setTL
: range (
@EFin R)
`|` [set -oo] = [set~ +oo].
Proof.
rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //.
by move=> [x| |] //= _; [left; exists x|right].
Qed.
End puncture_ereal_itv.
Section
salgebra_R_ssets
.
Variable
R
: realType.
Definition
measurableTypeR
:= salgebraType (
R.
-ocitv.
-measurable).
Definition
measurableR
: set (
set R)
:=
(
R.
-ocitv.
-measurable).
-sigma.
-measurable.
HB.instance Definition R_isMeasurable :
isMeasurable default_measure_display R :=
@isMeasurable.
Build _ measurableTypeR (
Pointed.class R)
measurableR
measurable0 (
@measurableC _ _) (
@bigcupT_measurable _ _).
Lemma
measurable_set1
(
r
: R)
: measurable [set r].
Proof.
#[local] Hint Resolve measurable_set1 : core.
Lemma
measurable_itv
(
i
: interval R)
: measurable [set` i].
Proof.
have moc (
a
b
: R)
: measurable `]a, b].
by apply: sub_sigma_algebra; apply: is_ocitv.
have mopoo (
x
: R)
: measurable `]x, +oo[.
by rewrite itv_bnd_infty_bigcup; exact: bigcup_measurable.
have mnooc (
x
: R)
: measurable `]-oo, x].
by rewrite -setCitvr; exact/measurableC.
have ooE (
a
b
: R)
: `]a, b[%classic = `]a, b] `\ b.
case: (
boolP (
a < b))
=> ab; last by rewrite !set_itv_ge ?set0D.
by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx andbF.
have moo (
a
b
: R)
: measurable `]a, b[.
by rewrite ooE; exact: measurableD.
have mcc (
a
b
: R)
: measurable `[a, b].
case: (
boolP (
a <= b))
=> ab; last by rewrite set_itv_ge.
by rewrite -setU1itv//; apply/measurableU.
have mco (
a
b
: R)
: measurable `[a, b[.
case: (
boolP (
a < b))
=> ab; last by rewrite set_itv_ge.
by rewrite -setU1itv//; apply/measurableU.
have oooE (
b
: R)
: `]-oo, b[%classic = `]-oo, b] `\ b.
by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx.
case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge.
- by rewrite -setU1itv//; exact/measurableU.
- by rewrite oooE; exact/measurableD.
- by rewrite set_itv_infty_infty.
Qed.
HB.instance Definition _ :=
(
ereal_isMeasurable (
R.
-ocitv.
-measurable)).
Lemma
measurable_image_EFin
(
A
: set R)
: measurableR A -> measurable (
EFin @` A).
Proof.
by move=> mA; exists A => //; exists set0; [constructor|rewrite setU0].
Qed.
Lemma
emeasurable_set1
(
x
: \bar R)
: measurable [set x].
Proof.
#[local] Hint Resolve emeasurable_set1 : core.
Lemma
__deprecated__itv_cpinfty_pinfty
: `[+oo%E, +oo[%classic = [set +oo%E] :> set (
\bar R).
Proof.
#[deprecated(
since="mathcomp-analysis 0.6.0", note="renamed `itv_cyy`")
]
Notation
itv_cpinfty_pinfty
:= __deprecated__itv_cpinfty_pinfty (
only parsing).
Lemma
__deprecated__itv_opinfty_pinfty
: `]+oo%E, +oo[%classic = set0 :> set (
\bar R).
Proof.
#[deprecated(
since="mathcomp-analysis 0.6.0", note="renamed `itv_oyy`")
]
Notation
itv_opinfty_pinfty
:= __deprecated__itv_opinfty_pinfty (
only parsing).
Lemma
__deprecated__itv_cninfty_pinfty
: `[-oo%E, +oo[%classic = setT :> set (
\bar R).
Proof.
#[deprecated(
since="mathcomp-analysis 0.6.0", note="renamed `itv_cNyy`")
]
Notation
itv_cninfty_pinfty
:= __deprecated__itv_cninfty_pinfty (
only parsing).
Lemma
__deprecated__itv_oninfty_pinfty
:
`]-oo%E, +oo[%classic = ~` [set -oo]%E :> set (
\bar R).
Proof.
#[deprecated(
since="mathcomp-analysis 0.6.0", note="renamed `itv_oNyy`")
]
Notation
itv_oninfty_pinfty
:= __deprecated__itv_oninfty_pinfty (
only parsing).
Let
emeasurable_itv_bndy
b
(
y
: \bar R)
:
measurable [set` Interval (
BSide b y)
+oo%O].
Proof.
Let
emeasurable_itv_Nybnd
b
(
y
: \bar R)
:
measurable [set` Interval -oo%O (
BSide b y)
].
Proof.
by rewrite -setCitvr; exact/measurableC/emeasurable_itv_bndy. Qed.
Lemma
emeasurable_itv
(
i
: interval (
\bar R))
:
measurable (
[set` i]%classic : set \bar R).
Proof.
Definition
elebesgue_measure
: set \bar R -> \bar R :=
fun
S
=> lebesgue_measure (
fine @` (
S `\` [set -oo; +oo]%E)).
Lemma
elebesgue_measure0
: elebesgue_measure set0 = 0%E.
Proof.
Lemma
measurable_image_fine
(
X
: set \bar R)
: measurable X ->
measurable [set fine x |
x
in X `\` [set -oo; +oo]%E].
Proof.
case => Y mY [X' [ | <-{X} | <-{X} | <-{X} ]].
- rewrite setU0 => <-{X}.
rewrite [X in measurable X](
_ : _ = Y)
// predeqE => r; split.
by move=> [x [[x' Yx' <-{x}/= _ <-//]]].
by move=> Yr; exists r%:E; split => [|[]//]; exists r.
- rewrite [X in measurable X](
_ : _ = Y)
// predeqE => r; split.
move=> [x [[[x' Yx' <- _ <-//]|]]].
by move=> <-; rewrite not_orP => -[]/(
_ erefl).
by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r.
- rewrite [X in measurable X](
_ : _ = Y)
// predeqE => r; split.
move=> [x [[[x' Yx' <-{x} _ <-//]|]]].
by move=> ->; rewrite not_orP => -[_]/(
_ erefl).
by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r.
- rewrite [X in measurable X](
_ : _ = Y)
// predeqE => r; split.
by rewrite setDUl setDv setU0 => -[_ [[x' Yx' <-]] _ <-].
by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r.
Qed.
Lemma
elebesgue_measure_ge0
X
: (
0 <= elebesgue_measure X)
%E.
Proof.
exact/measure_ge0. Qed.
Lemma
semi_sigma_additive_elebesgue_measure
:
semi_sigma_additive elebesgue_measure.
Proof.
move=> /= F mF tF mUF; rewrite /elebesgue_measure.
rewrite [X in lebesgue_measure X](
_ : _ =
\bigcup_n (
fine @` (
F n `\` [set -oo; +oo]%E)))
; last first.
rewrite predeqE => r; split.
by move=> [x [[n _ Fnx xoo <-]]]; exists n => //; exists x.
by move=> [n _ [x [Fnx xoo <-{r}]]]; exists x => //; split => //; exists n.
apply: (
@measure_semi_sigma_additive _ _ _ [the measure _ _ of (
@lebesgue_measure R)
]
(
fun
n
=> fine @` (
F n `\` [set -oo; +oo]%E))).
- move=> n; have := mF n.
move=> [X mX [X' mX']] XX'Fn.
apply: measurable_image_fine.
rewrite -XX'Fn.
apply: measurableU; first exact: measurable_image_EFin.
by case: mX' => //; exact: measurableU.
- move=> i j _ _ [x [[a [Fia aoo ax] [b [Fjb boo] bx]]]].
move: tF => /(
_ i j Logic.I Logic.I)
; apply.
suff ab : a = b by exists a; split => //; rewrite ab.
move: a b {Fia Fjb} aoo boo ax bx.
move=> [a| |] [b| |] /=.
+ by move=> _ _ -> ->.
+ by move=> _; rewrite not_orP => -[_]/(
_ erefl).
+ by move=> _; rewrite not_orP => -[]/(
_ erefl).
+ by rewrite not_orP => -[_]/(
_ erefl).
+ by rewrite not_orP => -[_]/(
_ erefl).
+ by rewrite not_orP => -[_]/(
_ erefl).
+ by rewrite not_orP => -[]/(
_ erefl).
+ by rewrite not_orP => -[]/(
_ erefl).
+ by rewrite not_orP => -[]/(
_ erefl).
- move: mUF.
rewrite {1}/measurable /emeasurable /= => -[X mX [Y []]] {Y}.
- rewrite setU0 => h.
rewrite [X in measurable X](
_ : _ = X)
// predeqE => r; split => [|Xr].
move=> -[n _ [x [Fnx xoo <-{r}]]].
have : (
\bigcup_n F n)
x by exists n.
by rewrite -h => -[x' Xx' <-].
have [n _ Fnr] : (
\bigcup_n F n)
r%:E by rewrite -h; exists r.
by exists n => //; exists r%:E => //; split => //; case.
- move=> h.
rewrite [X in measurable X](
_ : _ = X)
// predeqE => r; split => [|Xr].
move=> -[n _ [x [Fnx xoo <-]]].
have : (
\bigcup_n F n)
x by exists n.
by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[].
have [n _ Fnr] : (
\bigcup_n F n)
r%:E by rewrite -h; left; exists r.
by exists n => //; exists r%:E => //; split => //; case.
-
move=> h.
rewrite [X in measurable X](
_ : _ = X)
// predeqE => r; split => [|Xr].
move=> -[n _ [x [Fnx xoo <-]]].
have : (
\bigcup_n F n)
x by exists n.
by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[].
have [n _ Fnr] : (
\bigcup_n F n)
r%:E by rewrite -h; left; exists r.
by exists n => //; exists r%:E => //; split => //; case.
- move=> h.
rewrite [X in measurable X](
_ : _ = X)
// predeqE => r; split => [|Xr].
move=> -[n _ [x [Fnx xoo <-]]].
have : (
\bigcup_n F n)
x by exists n.
by rewrite -h => -[[x' Xx' <-//]|].
have [n _ Fnr] : (
\bigcup_n F n)
r%:E by rewrite -h; left; exists r.
by exists n => //; exists r%:E => //; split => //; case.
Qed.
HB.instance Definition _ := isMeasure.Build _ _ _ elebesgue_measure
elebesgue_measure0 elebesgue_measure_ge0
semi_sigma_additive_elebesgue_measure.
End salgebra_R_ssets.
#[global]
Hint Extern 0 (
measurable [set _])
=> solve [apply: measurable_set1|
apply: emeasurable_set1] : core.
#[global]
Hint Extern 0 (
measurable [set` _] )
=> exact: measurable_itv : core.
#[deprecated(
since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")
]
Notation
emeasurable_itv_bnd_pinfty
:= emeasurable_itv (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")
]
Notation
emeasurable_itv_ninfty_bnd
:= emeasurable_itv (
only parsing).
Lemma
measurable_fine
(
R
: realType) (
D
: set (
\bar R))
: measurable D ->
measurable_fun D fine.
Proof.
#[global] Hint Extern 0 (
measurable_fun _ fine)
=>
solve [exact: measurable_fine] : core.
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_fine` instead")
]
Notation
measurable_fun_fine
:= measurable_fine (
only parsing).
Section
lebesgue_measure_itv
.
Variable
R
: realType.
Let
lebesgue_measure_itvoc
(
a
b
: R)
:
(
lebesgue_measure (
`]a, b] : set R)
=
wlength [the cumulative _ of idfun] `]a, b])
%classic.
Proof.
Let
lebesgue_measure_itvoo_subr1
(
a
: R)
:
lebesgue_measure (
`]a - 1, a[%classic : set R)
= 1%E.
Proof.
Lemma
lebesgue_measure_set1
(
a
: R)
: lebesgue_measure [set a] = 0%E.
Proof.
Let
lebesgue_measure_itvoo
(
a
b
: R)
:
(
lebesgue_measure (
`]a, b[ : set R)
=
wlength [the cumulative _ of idfun] `]a, b[)
%classic.
Proof.
Let
lebesgue_measure_itvcc
(
a
b
: R)
:
(
lebesgue_measure (
`[a, b] : set R)
=
wlength [the cumulative _ of idfun] `[a, b])
%classic.
Proof.
Let
lebesgue_measure_itvco
(
a
b
: R)
:
(
lebesgue_measure (
`[a, b[ : set R)
=
wlength [the cumulative _ of idfun] `[a, b[)
%classic.
Proof.
Let
lebesgue_measure_itv_bnd
(
x
y
: bool) (
a
b
: R)
:
lebesgue_measure (
[set` Interval (
BSide x a) (
BSide y b)
] : set R)
=
wlength [the cumulative _ of idfun] [set` Interval (
BSide x a) (
BSide y b)
].
Proof.
Let
limnatR
: lim (
fun
k
=> (
k%:R)
%:E : \bar R)
= +oo%E.
Proof.
by apply/cvg_lim => //; apply/cvgenyP. Qed.
Let
lebesgue_measure_itv_bnd_infty
x
(
a
: R)
:
lebesgue_measure (
[set` Interval (
BSide x a)
+oo%O] : set R)
= +oo%E.
Proof.
Let
lebesgue_measure_itv_infty_bnd
y
(
b
: R)
:
lebesgue_measure (
[set` Interval -oo%O (
BSide y b)
] : set R)
= +oo%E.
Proof.
Let
lebesgue_measure_itv_infty_infty
:
lebesgue_measure (
[set` Interval -oo%O +oo%O] : set R)
= +oo%E.
Proof.
Lemma
lebesgue_measure_itv
(
i
: interval R)
:
lebesgue_measure (
[set` i] : set R)
= (
if i.
1 < i.
2 then i.
2 - i.
1 else 0)
%E.
Proof.
End lebesgue_measure_itv.
Section
measurable_ball
.
Variable
R
: realType.
Lemma
measurable_ball
(
x
: R)
e
: measurable (
ball x e).
Proof.
Lemma
lebesgue_measure_ball
(
x
r
: R)
: (
0 <= r)
%R ->
lebesgue_measure (
ball x r)
= (
r *+ 2)
%:E.
Proof.
Lemma
measurable_closed_ball
(
x
: R)
r
: measurable (
closed_ball x r).
Proof.
Lemma
lebesgue_measure_closed_ball
(
x
r
: R)
: 0 <= r ->
lebesgue_measure (
closed_ball x r)
= (
r *+ 2)
%:E.
Proof.
End measurable_ball.
Lemma
lebesgue_measure_rat
(
R
: realType)
:
lebesgue_measure (
range ratr : set R)
= 0%E.
Proof.
Section
measurable_fun_measurable
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Variables (
D
: set T) (
f
: T -> \bar R).
Hypotheses (
mD
: measurable D) (
mf
: measurable_fun D f).
Implicit Types y : \bar R.
Lemma
emeasurable_fun_c_infty
y
: measurable (
D `&` [set
x
| y <= f x]).
Proof.
by rewrite -preimage_itv_c_infty; exact/mf/emeasurable_itv. Qed.
Lemma
emeasurable_fun_o_infty
y
: measurable (
D `&` [set
x
| y < f x]).
Proof.
by rewrite -preimage_itv_o_infty; exact/mf/emeasurable_itv. Qed.
Lemma
emeasurable_fun_infty_o
y
: measurable (
D `&` [set
x
| f x < y]).
Proof.
by rewrite -preimage_itv_infty_o; exact/mf/emeasurable_itv. Qed.
Lemma
emeasurable_fun_infty_c
y
: measurable (
D `&` [set
x
| f x <= y]).
Proof.
by rewrite -preimage_itv_infty_c; exact/mf/emeasurable_itv. Qed.
Lemma
emeasurable_fin_num
: measurable (
D `&` [set
x
| f x \is a fin_num]).
Proof.
Lemma
emeasurable_neq
y
: measurable (
D `&` [set
x
| f x != y]).
Proof.
rewrite (
_ : [set
x
| f x != y] = f @^-1` (
setT `\ y)).
exact/mf/measurableD.
rewrite predeqE => t; split; last by rewrite /preimage /= => -[_ /eqP].
by rewrite /= => ft0; rewrite /preimage /=; split => //; exact/eqP.
Qed.
End measurable_fun_measurable.
Module
RGenOInfty
.
Section
rgenoinfty
.
Variable
R
: realType.
Implicit Types x y z : R.
Definition
G
:= [set
A
| exists
x,
A = `]x, +oo[%classic].
Lemma
measurable_itv_bnd_infty
b
x
:
G.
-sigma.
-measurable [set` Interval (
BSide b x)
+oo%O].
Proof.
Lemma
measurable_itv_bounded
a
b
x
: a != +oo%O ->
G.
-sigma.
-measurable [set` Interval a (
BSide b x)
].
Proof.
Lemma
measurableE
: (
@ocitv R).
-sigma.
-measurable = G.
-sigma.
-measurable.
Proof.
End rgenoinfty.
End RGenOInfty.
Module
RGenInftyO
.
Section
rgeninftyo
.
Variable
R
: realType.
Implicit Types x y z : R.
Definition
G
:= [set
A
| exists
x,
A = `]-oo, x[%classic].
Lemma
measurable_itv_bnd_infty
b
x
:
G.
-sigma.
-measurable [set` Interval -oo%O (
BSide b x)
].
Proof.
Lemma
measurable_itv_bounded
a
b
x
: a != -oo%O ->
G.
-sigma.
-measurable [set` Interval (
BSide b x)
a].
Proof.
Lemma
measurableE
: (
@ocitv R).
-sigma.
-measurable = G.
-sigma.
-measurable.
Proof.
End rgeninftyo.
End RGenInftyO.
Module
RGenCInfty
.
Section
rgencinfty
.
Variable
R
: realType.
Implicit Types x y z : R.
Definition
G
: set (
set R)
:= [set
A
| exists
x,
A = `[x, +oo[%classic].
Lemma
measurable_itv_bnd_infty
b
x
:
G.
-sigma.
-measurable [set` Interval (
BSide b x)
+oo%O].
Proof.
Lemma
measurable_itv_bounded
a
b
y
: a != +oo%O ->
G.
-sigma.
-measurable [set` Interval a (
BSide b y)
].
Proof.
Lemma
measurableE
: (
@ocitv R).
-sigma.
-measurable = G.
-sigma.
-measurable.
Proof.
End rgencinfty.
End RGenCInfty.
Module
RGenOpens
.
Section
rgenopens
.
Variable
R
: realType.
Implicit Types x y z : R.
Definition
G
:= [set
A
| exists
x
y,
A = `]x, y[%classic].
Local Lemma
measurable_itvoo
x
y
: G.
-sigma.
-measurable `]x, y[%classic.
Proof.
Local Lemma
measurable_itv_o_infty
x
: G.
-sigma.
-measurable `]x, +oo[%classic.
Proof.
Lemma
measurable_itv_bnd_infty
b
x
:
G.
-sigma.
-measurable [set` Interval (
BSide b x)
+oo%O].
Proof.
Lemma
measurable_itv_infty_bnd
b
x
:
G.
-sigma.
-measurable [set` Interval -oo%O (
BSide b x)
].
Proof.
Lemma
measurable_itv_bounded
a
x
b
y
:
G.
-sigma.
-measurable [set` Interval (
BSide a x) (
BSide b y)
].
Proof.
Lemma
measurableE
: (
@ocitv R).
-sigma.
-measurable = G.
-sigma.
-measurable.
Proof.
End rgenopens.
End RGenOpens.
Section
erealwithrays
.
Variable
R
: realType.
Implicit Types (
x y z : \bar R) (
r s : R).
Local Open Scope ereal_scope.
Lemma
EFin_itv_bnd_infty
b
r
: EFin @` [set` Interval (
BSide b r)
+oo%O] =
[set` Interval (
BSide b r%:E)
+oo%O] `\ +oo.
Proof.
Lemma
EFin_itv
r
: [set
s
| r%:E < s%:E] = `]r, +oo[%classic.
Proof.
Lemma
preimage_EFin_setT
: @EFin R @^-1` [set
x
| x \in `]-oo%E, +oo[] = setT.
Proof.
Lemma
eitv_bnd_infty
b
r
: `[r%:E, +oo[%classic =
\bigcap_k [set` Interval (
BSide b (
r - k.
+1%:R^-1)
%:E)
+oo%O] :> set _.
Proof.
Lemma
eitv_infty_bnd
b
r
: `]-oo, r%:E]%classic =
\bigcap_k [set` Interval -oo%O (
BSide b (
r%:E + k.
+1%:R^-1%:E))
] :> set _.
Proof.
Lemma
eset1Ny
:
[set -oo] = \bigcap_k `]-oo, (
-k%:R%:E)
[%classic :> set (
\bar R).
Proof.
Lemma
eset1y
: [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (
\bar R).
Proof.
End erealwithrays.
Module
ErealGenOInfty
.
Section
erealgenoinfty
.
Variable
R
: realType.
Implicit Types (
x y z : \bar R) (
r s : R).
Local Open Scope ereal_scope.
Definition
G
:= [set
A
: set \bar R | exists
r,
A = `]r%:E, +oo[%classic].
Lemma
measurable_set1Ny
: G.
-sigma.
-measurable [set -oo].
Proof.
Lemma
measurable_set1y
: G.
-sigma.
-measurable [set +oo].
Proof.
Lemma
measurableE
: emeasurable (
@ocitv R)
= G.
-sigma.
-measurable.
Proof.
End erealgenoinfty.
End ErealGenOInfty.
Module
ErealGenCInfty
.
Section
erealgencinfty
.
Variable
R
: realType.
Implicit Types (
x y z : \bar R) (
r s : R).
Local Open Scope ereal_scope.
Definition
G
:= [set
A
: set \bar R | exists
r,
A = `[r%:E, +oo[%classic].
Lemma
measurable_set1Ny
: G.
-sigma.
-measurable [set -oo].
Proof.
Lemma
measurable_set1y
: G.
-sigma.
-measurable [set +oo].
Proof.
Lemma
measurableE
: emeasurable (
@ocitv R)
= G.
-sigma.
-measurable.
Proof.
End erealgencinfty.
End ErealGenCInfty.
Module
ErealGenInftyO
.
Section
erealgeninftyo
.
Variable
R
: realType.
Definition
G
:= [set
A
: set \bar R | exists
r,
A = `]-oo, r%:E[%classic].
Lemma
measurableE
: emeasurable (
@ocitv R)
= G.
-sigma.
-measurable.
Proof.
End erealgeninftyo.
End ErealGenInftyO.
Section
trace
.
Variable (
T
: Type).
Implicit Types (
G : set (
set T)) (
A D : set T).
Definition
strace
G
D
:= [set x `&` D |
x
in G].
Lemma
stracexx
G
D
: G D -> strace G D D.
Proof.
by rewrite /strace /=; exists D => //; rewrite setIid. Qed.
Lemma
sigma_algebra_strace
G
D
:
sigma_algebra setT G -> sigma_algebra D (
strace G D).
Proof.
move=> [G0 GC GU]; split; first by exists set0 => //; rewrite set0I.
- move=> S [A mA ADS]; have mCA := GC _ mA.
have : strace G D (
D `&` ~` A).
by rewrite setIC; exists (
setT `\` A)
=> //; rewrite setTD.
rewrite -setDE => trDA.
have DADS : D `\` A = D `\` S by rewrite -ADS !setDE setCI setIUr setICr setU0.
by rewrite DADS in trDA.
- move=> S mS; have /choice[M GM] : forall
n,
exists
A,
G A /\ S n = A `&` D.
by move=> n; have [A mA ADSn] := mS n; exists A.
exists (
\bigcup_i (
M i))
; first by apply GU => i; exact: (
GM i).
1.
by rewrite setI_bigcupl; apply eq_bigcupr => i _; rewrite (
GM i).
2.
Qed.
End trace.
Lemma
strace_measurable
d
(
T
: measurableType d) (
A
: set T)
: measurable A ->
strace measurable A `<=` measurable.
Proof.
Lemma
is_interval_measurable
(
R
: realType) (
I
: set R)
:
is_interval I -> measurable I.
Proof.
Section
coutinuous_measurable
.
Variable
R
: realType.
Lemma
open_measurable
(
A
: set R)
: open A -> measurable A.
Proof.
Lemma
open_measurable_subspace
(
D
: set R) (
U
: set (
subspace D))
:
measurable D -> open U -> measurable (
D `&` U).
Proof.
Lemma
closed_measurable
(
A
: set R)
: closed A -> measurable A.
Proof.
by move/closed_openC/open_measurable/measurableC; rewrite setCK. Qed.
Lemma
compact_measurable
(
A
: set R)
: compact A -> measurable A.
Proof.
Lemma
subspace_continuous_measurable_fun
(
D
: set R) (
f
: subspace D -> R)
:
measurable D -> continuous f -> measurable_fun D f.
Proof.
Corollary
open_continuous_measurable_fun
(
D
: set R) (
f
: R -> R)
:
open D -> {in D, continuous f} -> measurable_fun D f.
Proof.
Lemma
continuous_measurable_fun
(
f
: R -> R)
:
continuous f -> measurable_fun setT f.
Proof.
End coutinuous_measurable.
Lemma
lower_semicontinuous_measurable
{R : realType} (
f
: R -> \bar R)
:
lower_semicontinuous f -> measurable_fun setT f.
Proof.
Section
standard_measurable_fun
.
Variable
R
: realType.
Implicit Types D : set R.
Lemma
measurable_oppr
D
: measurable_fun D (
-%R).
Proof.
Lemma
measurable_normr
D
: measurable_fun D (
@normr _ R).
Proof.
Lemma
measurable_mulrl
D
(
k
: R)
: measurable_fun D (
*%R k).
Proof.
Lemma
measurable_mulrr
D
(
k
: R)
: measurable_fun D (
fun
x
=> x * k).
Proof.
Lemma
measurable_exprn
D
n
: measurable_fun D (
fun
x
=> x ^+ n).
Proof.
End standard_measurable_fun.
#[global] Hint Extern 0 (
measurable_fun _ (
-%R))
=>
solve [exact: measurable_oppr] : core.
#[global] Hint Extern 0 (
measurable_fun _ normr)
=>
solve [exact: measurable_normr] : core.
#[global] Hint Extern 0 (
measurable_fun _ (
*%R _))
=>
solve [exact: measurable_mulrl] : core.
#[global] Hint Extern 0 (
measurable_fun _ (
fun
x
=> x ^+ _))
=>
solve [exact: measurable_exprn] : core.
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_exprn` instead")
]
Notation
measurable_fun_sqr
:= measurable_exprn (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_oppr` instead")
]
Notation
measurable_fun_opp
:= measurable_oppr (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_oppr` instead")
]
Notation
measurable_funN
:= measurable_oppr (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_normr` instead")
]
Notation
measurable_fun_normr
:= measurable_normr (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_exprn` instead")
]
Notation
measurable_fun_exprn
:= measurable_exprn (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_mulrl` instead")
]
Notation
measurable_funrM
:= measurable_mulrl (
only parsing).
Section
measurable_fun_realType
.
Context
d
(
T
: measurableType d) (
R
: realType).
Implicit Types (
D : set T) (
f g : T -> R).
Lemma
measurable_funD
D
f
g
:
measurable_fun D f -> measurable_fun D g -> measurable_fun D (
f \+ g).
Proof.
Lemma
measurable_funB
D
f
g
: measurable_fun D f ->
measurable_fun D g -> measurable_fun D (
f \- g).
Proof.
Lemma
measurable_funM
D
f
g
:
measurable_fun D f -> measurable_fun D g -> measurable_fun D (
f \* g).
Proof.
Lemma
measurable_fun_ltr
D
f
g
: measurable_fun D f -> measurable_fun D g ->
measurable_fun D (
fun
x
=> f x < g x).
Proof.
Lemma
measurable_maxr
D
f
g
:
measurable_fun D f -> measurable_fun D g -> measurable_fun D (
f \max g).
Proof.
Lemma
measurable_minr
D
f
g
:
measurable_fun D f -> measurable_fun D g -> measurable_fun D (
f \min g).
Proof.
Lemma
measurable_fun_sups
D
(
h
: (
T -> R)
^nat)
n
:
(
forall
t,
D t -> has_ubound (
range (
h ^~ t)))
->
(
forall
m,
measurable_fun D (
h m))
->
measurable_fun D (
fun
x
=> sups (
h ^~ x)
n).
Proof.
Lemma
measurable_fun_infs
D
(
h
: (
T -> R)
^nat)
n
:
(
forall
t,
D t -> has_lbound (
range (
h ^~ t)))
->
(
forall
n,
measurable_fun D (
h n))
->
measurable_fun D (
fun
x
=> infs (
h ^~ x)
n).
Proof.
Lemma
measurable_fun_limn_sup
D
(
h
: (
T -> R)
^nat)
:
(
forall
t,
D t -> has_ubound (
range (
h ^~ t)))
->
(
forall
t,
D t -> has_lbound (
range (
h ^~ t)))
->
(
forall
n,
measurable_fun D (
h n))
->
measurable_fun D (
fun
x
=> limn_sup (
h ^~ x)).
Proof.
Lemma
measurable_fun_cvg
D
(
h
: (
T -> R)
^nat)
f
:
(
forall
m,
measurable_fun D (
h m))
-> (
forall
x,
D x -> h ^~ x --> f x)
->
measurable_fun D f.
Proof.
move=> mf_ f_f; have fE x : D x -> f x = limn_sup (
h ^~ x).
move=> Dx; have /cvg_lim <-// := @cvg_sups _ (
h ^~ x) (
f x) (
f_f _ Dx).
exact: Rhausdorff.
apply: (
@eq_measurable_fun _ _ _ _ D (
fun
x
=> limn_sup (
h ^~ x))).
by move=> x; rewrite inE => Dx; rewrite -fE.
apply: (
@measurable_fun_limn_sup _ h)
=> // t Dt.
- apply/bounded_fun_has_ubound/(
@cvg_seq_bounded _ [normedModType R of R^o]).
by apply/cvg_ex; eexists; exact: f_f.
- apply/bounded_fun_has_lbound/(
@cvg_seq_bounded _ [normedModType R of R^o]).
by apply/cvg_ex; eexists; exact: f_f.
Qed.
End measurable_fun_realType.
#[deprecated(
since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_sup`")
]
Notation
measurable_fun_lim_sup
:= measurable_fun_limn_sup (
only parsing).
Lemma
measurable_ln
(
R
: realType)
: measurable_fun [set~ (
0:R)
] (
@ln R).
Proof.
#[global] Hint Extern 0 (
measurable_fun _ (
@ln _))
=>
solve [apply: measurable_ln] : core.
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_ln` instead")
]
Notation
measurable_fun_ln
:= measurable_ln (
only parsing).
Lemma
measurable_expR
(
R
: realType)
: measurable_fun [set: R] expR.
Proof.
#[global] Hint Extern 0 (
measurable_fun _ expR)
=>
solve [apply: measurable_expR] : core.
Lemma
measurable_powR
(
R
: realType)
p
:
measurable_fun [set: R] (
@powR R ^~ p).
Proof.
#[global] Hint Extern 0 (
measurable_fun _ (
@powR _ ^~ _))
=>
solve [apply: measurable_powR] : core.
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_powR` instead")
]
Notation
measurable_fun_power_pos
:= measurable_powR (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.4", note="use `measurable_powR` instead")
]
Notation
measurable_power_pos
:= measurable_powR (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_maxr` instead")
]
Notation
measurable_fun_max
:= measurable_maxr (
only parsing).
Section
standard_emeasurable_fun
.
Variable
R
: realType.
Lemma
measurable_EFin
(
D
: set R)
: measurable_fun D EFin.
Proof.
Lemma
measurable_abse
(
D
: set (
\bar R))
: measurable_fun D abse.
Proof.
Lemma
measurable_oppe
(
D
: set (
\bar R))
:
measurable_fun D (
-%E : \bar R -> \bar R).
Proof.
End standard_emeasurable_fun.
#[global] Hint Extern 0 (
measurable_fun _ abse)
=>
solve [exact: measurable_abse] : core.
#[global] Hint Extern 0 (
measurable_fun _ EFin)
=>
solve [exact: measurable_EFin] : core.
#[global] Hint Extern 0 (
measurable_fun _ (
-%E))
=>
solve [exact: measurable_oppe] : core.
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_oppe` instead")
]
Notation
emeasurable_fun_minus
:= measurable_oppe (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_abse` instead")
]
Notation
measurable_fun_abse
:= measurable_abse (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_EFin` instead")
]
Notation
measurable_fun_EFin
:= measurable_EFin (
only parsing).
Lemma
EFin_measurable_fun
d
(
T
: measurableType d) (
R
: realType) (
D
: set T)
(
g
: T -> R)
:
measurable_fun D (
EFin \o g)
<-> measurable_fun D g.
Proof.
Lemma
measurable_er_map
d
(
T
: measurableType d) (
R
: realType) (
f
: R -> R)
: measurable_fun setT f -> measurable_fun [set: \bar R] (
er_map f).
Proof.
#[deprecated(
since="mathcomp-analysis 0.6.3", note="renamed `measurable_er_map`")
]
Notation
measurable_fun_er_map
:= measurable_er_map (
only parsing).
Section
emeasurable_fun
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType).
Implicit Types (
D : set T).
Lemma
measurable_fun_einfs
D
(
f
: (
T -> \bar R)
^nat)
:
(
forall
n,
measurable_fun D (
f n))
->
forall
n,
measurable_fun D (
fun
x
=> einfs (
f ^~ x)
n).
Proof.
Lemma
measurable_fun_esups
D
(
f
: (
T -> \bar R)
^nat)
:
(
forall
n,
measurable_fun D (
f n))
->
forall
n,
measurable_fun D (
fun
x
=> esups (
f ^~ x)
n).
Proof.
Lemma
measurable_maxe
D
(
f
g
: T -> \bar R)
:
measurable_fun D f -> measurable_fun D g ->
measurable_fun D (
fun
x
=> maxe (
f x) (
g x)).
Proof.
Lemma
measurable_funepos
D
(
f
: T -> \bar R)
:
measurable_fun D f -> measurable_fun D f^\+.
Proof.
Lemma
measurable_funeneg
D
(
f
: T -> \bar R)
:
measurable_fun D f -> measurable_fun D f^\-.
Proof.
Lemma
measurable_mine
D
(
f
g
: T -> \bar R)
:
measurable_fun D f -> measurable_fun D g ->
measurable_fun D (
fun
x
=> mine (
f x) (
g x)).
Proof.
Lemma
measurable_fun_limn_esup
D
(
f
: (
T -> \bar R)
^nat)
:
(
forall
n,
measurable_fun D (
f n))
->
measurable_fun D (
fun
x
=> limn_esup (
f ^~ x)).
Proof.
Lemma
emeasurable_fun_cvg
D
(
f_
: (
T -> \bar R)
^nat) (
f
: T -> \bar R)
:
(
forall
m,
measurable_fun D (
f_ m))
->
(
forall
x,
D x -> f_ ^~ x --> f x)
-> measurable_fun D f.
Proof.
End emeasurable_fun.
Arguments emeasurable_fun_cvg {d T R D} f_.
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurableT_comp` instead")
]
Notation
emeasurable_funN
:= measurableT_comp (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_maxe` instead")
]
Notation
emeasurable_fun_max
:= measurable_maxe (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_mine` instead")
]
Notation
emeasurable_fun_min
:= measurable_mine (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_funepos` instead")
]
Notation
emeasurable_fun_funepos
:= measurable_funepos (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.3", note="use `measurable_funeneg` instead")
]
Notation
emeasurable_fun_funeneg
:= measurable_funeneg (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_esup`")
]
Notation
measurable_fun_lim_esup
:= measurable_fun_limn_esup (
only parsing).
Section
lebesgue_regularity
.
Context {R : realType}.
Let
mu
:= [the measure _ _ of @lebesgue_measure R].
Local Open Scope ereal_scope.
Lemma
lebesgue_regularity_outer
(
D
: set R) (
eps
: R)
:
measurable D -> mu D < +oo -> (
0 < eps)
%R ->
exists
U
: set R, [/\ open U , D `<=` U & mu (
U `\` D)
< eps%:E].
Proof.
Lemma
lebesgue_nearly_bounded
(
D
: set R) (
eps
: R)
:
measurable D -> mu D < +oo -> (
0 < eps)
%R ->
exists
ab
: R * R, mu (
D `\` [set` `[ab.
1,ab.
2]])
< eps%:E.
Proof.
Lemma
lebesgue_regularity_inner
(
D
: set R) (
eps
: R)
:
measurable D -> mu D < +oo -> (
0 < eps)
%R ->
exists
V
: set R, [/\ compact V , V `<=` D & mu (
D `\` V)
< eps%:E].
Proof.
Let
lebesgue_regularity_innerE_bounded
(
A
: set R)
: measurable A ->
mu A < +oo ->
mu A = ereal_sup [set mu K |
K
in [set
K
| compact K /\ K `<=` A]].
Proof.
Lemma
lebesgue_regularity_inner_sup
(
D
: set R)
: measurable D ->
mu D = ereal_sup [set mu K |
K
in [set
K
| compact K /\ K `<=` D]].
Proof.
End lebesgue_regularity.
Section
egorov
.
Context
d
{R : realType} {T : measurableType d}.
Context (
mu
: {measure set T -> \bar R}).
Local Open Scope ereal_scope.
Lemma
pointwise_almost_uniform
(
f_
: (
T -> R)
^nat) (
g
: T -> R) (
A
: set T) (
eps
: R)
:
(
forall
n,
measurable_fun A (
f_ n))
-> measurable_fun A g ->
measurable A -> mu A < +oo -> (
forall
x,
A x -> f_ ^~ x --> g x)
->
(
0 < eps)
%R -> exists
B,
[/\ measurable B, mu B < eps%:E &
{uniform A `\` B, f_ --> g}].
Proof.
Lemma
ae_pointwise_almost_uniform
(
f_
: (
T -> R)
^nat) (
g
: T -> R) (
A
: set T) (
eps
: R)
:
(
forall
n,
measurable_fun A (
f_ n))
-> measurable_fun A g ->
measurable A -> mu A < +oo -> {ae mu, (
forall
x,
A x -> f_ ^~ x --> g x)
} ->
(
0 < eps)
%R -> exists
B,
[/\ measurable B, mu B < eps%:E &
{uniform A `\` B, (
fun
n
=> (
f_ n : T -> R))
--> g}].
Proof.
End egorov.
Definition
vitali_cover
{R : realType} (
E
: set R)
I
(
B
: I -> set R) (
D
: set I)
:=
(
forall
i,
is_ball (
B i))
/\
forall
x,
E x -> forall
e
: R, 0 < e -> exists
i,
[/\ D i, B i x & (
radius (
B i))
%:num < e].
Section
vitali_theorem
.
Context {R : realType} (
A
: set R) (
B
: nat -> set R).
Hypothesis
B0
: forall
i,
(
0 < (
radius (
B i))
%:num)
%R.
Notation
mu
:= (
@lebesgue_measure R).
Local Open Scope ereal_scope.
Lemma
vitali_theorem
(
V
: set nat)
: vitali_cover A B V ->
exists
D,
[/\ countable D, D `<=` V, trivIset D (
closure \o B)
&
mu (
A `\` \bigcup_(
k
in D)
closure (
B k))
= 0].
Proof.
End vitali_theorem.