Convergence in measure #
We define convergence in measure which is one of the many notions of convergence in probability.
A sequence of functions f is said to converge in measure to some function g
if for all ε > 0, the measure of the set {x | ε ≤ dist (f i x) (g x)} tends to 0 as i
converges along some given filter l.
Convergence in measure is most notably used in the formulation of the weak law of large numbers and is also useful in theorems such as the Vitali convergence theorem. This file provides some basic lemmas for working with convergence in measure and establishes some relations between convergence in measure and other notions of convergence.
Main definitions #
MeasureTheory.TendstoInMeasure (μ : Measure α) (f : ι → α → E) (g : α → E):fconverges inμ-measure tog.
Main results #
MeasureTheory.tendstoInMeasure_of_tendsto_ae: convergence almost everywhere in a finite measure space implies convergence in measure.MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae: iffis a sequence of functions which converges in measure tog, thenfhas a subsequence which convergence almost everywhere tog.MeasureTheory.exists_seq_tendstoInMeasure_atTop_iff: for a sequence of functionsf, convergence in measure is equivalent to the fact that every subsequence has another subsequence that converges almost surely.MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm: convergence in Lp implies convergence in measure.
def
MeasureTheory.TendstoInMeasure
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
[Dist E]
{x✝ : MeasurableSpace α}
(μ : Measure α)
(f : ι → α → E)
(l : Filter ι)
(g : α → E)
:
A sequence of functions f is said to converge in measure to some function g if for all
ε > 0, the measure of the set {x | ε ≤ dist (f i x) (g x)} tends to 0 as i converges along
some given filter l.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.tendstoInMeasure_iff_norm
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[SeminormedAddCommGroup E]
{l : Filter ι}
{f : ι → α → E}
{g : α → E}
:
Iff (TendstoInMeasure μ f l g)
(∀ (ε : Real),
LT.lt 0 ε →
Filter.Tendsto
(fun (i : ι) => DFunLike.coe μ (setOf fun (x : α) => LE.le ε (Norm.norm (HSub.hSub (f i x) (g x))))) l (nhds 0))
theorem
MeasureTheory.tendstoInMeasure_iff_tendsto_toNNReal
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[Dist E]
[IsFiniteMeasure μ]
{f : ι → α → E}
{l : Filter ι}
{g : α → E}
:
Iff (TendstoInMeasure μ f l g)
(∀ (ε : Real),
LT.lt 0 ε →
Filter.Tendsto (fun (i : ι) => (DFunLike.coe μ (setOf fun (x : α) => LE.le ε (Dist.dist (f i x) (g x)))).toNNReal)
l (nhds 0))
theorem
MeasureTheory.TendstoInMeasure.mono
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[Dist E]
{f : ι → α → E}
{g : α → E}
{u v : Filter ι}
(huv : LE.le v u)
(hg : TendstoInMeasure μ f u g)
:
TendstoInMeasure μ f v g
theorem
MeasureTheory.TendstoInMeasure.comp
{α : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[Dist E]
{f : ι → α → E}
{g : α → E}
{u : Filter ι}
{v : Filter κ}
{ns : κ → ι}
(hg : TendstoInMeasure μ f u g)
(hns : Filter.Tendsto ns v u)
:
TendstoInMeasure μ (Function.comp f ns) v g
theorem
MeasureTheory.TendstoInMeasure.congr'
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[Dist E]
{l : Filter ι}
{f f' : ι → α → E}
{g g' : α → E}
(h_left : Filter.Eventually (fun (i : ι) => (ae μ).EventuallyEq (f i) (f' i)) l)
(h_right : (ae μ).EventuallyEq g g')
(h_tendsto : TendstoInMeasure μ f l g)
:
TendstoInMeasure μ f' l g'
theorem
MeasureTheory.TendstoInMeasure.congr
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[Dist E]
{l : Filter ι}
{f f' : ι → α → E}
{g g' : α → E}
(h_left : ∀ (i : ι), (ae μ).EventuallyEq (f i) (f' i))
(h_right : (ae μ).EventuallyEq g g')
(h_tendsto : TendstoInMeasure μ f l g)
:
TendstoInMeasure μ f' l g'
theorem
MeasureTheory.TendstoInMeasure.congr_left
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[Dist E]
{l : Filter ι}
{f f' : ι → α → E}
{g : α → E}
(h : ∀ (i : ι), (ae μ).EventuallyEq (f i) (f' i))
(h_tendsto : TendstoInMeasure μ f l g)
:
TendstoInMeasure μ f' l g
theorem
MeasureTheory.TendstoInMeasure.congr_right
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[Dist E]
{l : Filter ι}
{f : ι → α → E}
{g g' : α → E}
(h : (ae μ).EventuallyEq g g')
(h_tendsto : TendstoInMeasure μ f l g)
:
TendstoInMeasure μ f l g'
theorem
MeasureTheory.tendstoInMeasure_of_tendsto_ae_of_stronglyMeasurable
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MetricSpace E]
{f : Nat → α → E}
{g : α → E}
[IsFiniteMeasure μ]
(hf : ∀ (n : Nat), StronglyMeasurable (f n))
(hg : StronglyMeasurable g)
(hfg : Filter.Eventually (fun (x : α) => Filter.Tendsto (fun (n : Nat) => f n x) Filter.atTop (nhds (g x))) (ae μ))
:
TendstoInMeasure μ f Filter.atTop g
Auxiliary lemma for tendstoInMeasure_of_tendsto_ae.
theorem
MeasureTheory.tendstoInMeasure_of_tendsto_ae
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MetricSpace E]
{f : Nat → α → E}
{g : α → E}
[IsFiniteMeasure μ]
(hf : ∀ (n : Nat), AEStronglyMeasurable (f n) μ)
(hfg : Filter.Eventually (fun (x : α) => Filter.Tendsto (fun (n : Nat) => f n x) Filter.atTop (nhds (g x))) (ae μ))
:
TendstoInMeasure μ f Filter.atTop g
Convergence a.e. implies convergence in measure in a finite measure space.
theorem
MeasureTheory.ExistsSeqTendstoAe.exists_nat_measure_lt_two_inv
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MetricSpace E]
{f : Nat → α → E}
{g : α → E}
(hfg : TendstoInMeasure μ f Filter.atTop g)
(n : Nat)
:
noncomputable def
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MetricSpace E]
{f : Nat → α → E}
{g : α → E}
(hfg : TendstoInMeasure μ f Filter.atTop g)
(n : Nat)
:
Given a sequence of functions f which converges in measure to g,
seqTendstoAeSeqAux is a sequence such that
∀ m ≥ seqTendstoAeSeqAux n, μ {x | 2⁻¹ ^ n ≤ dist (f m x) (g x)} ≤ 2⁻¹ ^ n.
Equations
Instances For
noncomputable def
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MetricSpace E]
{f : Nat → α → E}
{g : α → E}
(hfg : TendstoInMeasure μ f Filter.atTop g)
:
Transformation of seqTendstoAeSeqAux to makes sure it is strictly monotone.
Equations
- One or more equations did not get rendered due to their size.
- Eq (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg 0) (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux hfg 0)
Instances For
theorem
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_succ
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MetricSpace E]
{f : Nat → α → E}
{g : α → E}
(hfg : TendstoInMeasure μ f Filter.atTop g)
{n : Nat}
:
Eq (seqTendstoAeSeq hfg (HAdd.hAdd n 1))
(Max.max (seqTendstoAeSeqAux hfg (HAdd.hAdd n 1)) (HAdd.hAdd (seqTendstoAeSeq hfg n) 1))
theorem
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_spec
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MetricSpace E]
{f : Nat → α → E}
{g : α → E}
(hfg : TendstoInMeasure μ f Filter.atTop g)
(n k : Nat)
(hn : LE.le (seqTendstoAeSeq hfg n) k)
:
theorem
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_strictMono
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MetricSpace E]
{f : Nat → α → E}
{g : α → E}
(hfg : TendstoInMeasure μ f Filter.atTop g)
:
StrictMono (seqTendstoAeSeq hfg)
theorem
MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MetricSpace E]
{f : Nat → α → E}
{g : α → E}
(hfg : TendstoInMeasure μ f Filter.atTop g)
:
Exists fun (ns : Nat → Nat) =>
And (StrictMono ns)
(Filter.Eventually (fun (x : α) => Filter.Tendsto (fun (i : Nat) => f (ns i) x) Filter.atTop (nhds (g x))) (ae μ))
If f is a sequence of functions which converges in measure to g, then there exists a
subsequence of f which converges a.e. to g.
theorem
MeasureTheory.TendstoInMeasure.exists_seq_tendstoInMeasure_atTop
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MetricSpace E]
{u : Filter ι}
[u.NeBot]
[u.IsCountablyGenerated]
{f : ι → α → E}
{g : α → E}
(hfg : TendstoInMeasure μ f u g)
:
Exists fun (ns : Nat → ι) =>
And (Filter.Tendsto ns Filter.atTop u) (TendstoInMeasure μ (fun (n : Nat) => f (ns n)) Filter.atTop g)
theorem
MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae'
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MetricSpace E]
{u : Filter ι}
[u.NeBot]
[u.IsCountablyGenerated]
{f : ι → α → E}
{g : α → E}
(hfg : TendstoInMeasure μ f u g)
:
Exists fun (ns : Nat → ι) =>
And (Filter.Tendsto ns Filter.atTop u)
(Filter.Eventually (fun (x : α) => Filter.Tendsto (fun (i : Nat) => f (ns i) x) Filter.atTop (nhds (g x))) (ae μ))
theorem
MeasureTheory.exists_seq_tendstoInMeasure_atTop_iff
{α : Type u_1}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MetricSpace E]
[IsFiniteMeasure μ]
{f : Nat → α → E}
(hf : ∀ (n : Nat), AEStronglyMeasurable (f n) μ)
{g : α → E}
:
Iff (TendstoInMeasure μ f Filter.atTop g)
(∀ (ns : Nat → Nat),
StrictMono ns →
Exists fun (ns' : Nat → Nat) =>
And (StrictMono ns')
(Filter.Eventually
(fun (ω : α) => Filter.Tendsto (fun (i : Nat) => f (ns (ns' i)) ω) Filter.atTop (nhds (g ω))) (ae μ)))
TendstoInMeasure is equivalent to every subsequence having another subsequence
which converges almost surely.
theorem
MeasureTheory.tendstoInMeasure_ae_unique
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MetricSpace E]
{g h : α → E}
{f : ι → α → E}
{u : Filter ι}
[u.NeBot]
[u.IsCountablyGenerated]
(hg : TendstoInMeasure μ f u g)
(hh : TendstoInMeasure μ f u h)
:
(ae μ).EventuallyEq g h
The limit in measure is ae unique.
theorem
MeasureTheory.TendstoInMeasure.aemeasurable
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MeasurableSpace E]
[NormedAddCommGroup E]
[BorelSpace E]
{u : Filter ι}
[u.NeBot]
[u.IsCountablyGenerated]
{f : ι → α → E}
{g : α → E}
(hf : ∀ (n : ι), AEMeasurable (f n) μ)
(h_tendsto : TendstoInMeasure μ f u g)
:
AEMeasurable g μ
theorem
MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{p : ENNReal}
{f : ι → α → E}
{g : α → E}
(hp_ne_zero : Ne p 0)
(hp_ne_top : Ne p Top.top)
(hf : ∀ (n : ι), StronglyMeasurable (f n))
(hg : StronglyMeasurable g)
{l : Filter ι}
(hfg : Filter.Tendsto (fun (n : ι) => eLpNorm (HSub.hSub (f n) g) p μ) l (nhds 0))
:
TendstoInMeasure μ f l g
This lemma is superseded by MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm where we
allow p = ∞ and only require AEStronglyMeasurable.
theorem
MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{p : ENNReal}
{f : ι → α → E}
{g : α → E}
(hp_ne_zero : Ne p 0)
(hp_ne_top : Ne p Top.top)
(hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ)
(hg : AEStronglyMeasurable g μ)
{l : Filter ι}
(hfg : Filter.Tendsto (fun (n : ι) => eLpNorm (HSub.hSub (f n) g) p μ) l (nhds 0))
:
TendstoInMeasure μ f l g
This lemma is superseded by MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm where we
allow p = ∞.
theorem
MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_top
{α : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
{f : ι → α → E}
{g : α → E}
{l : Filter ι}
(hfg : Filter.Tendsto (fun (n : ι) => eLpNorm (HSub.hSub (f n) g) Top.top μ) l (nhds 0))
:
TendstoInMeasure μ f l g
See also MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm which work for general
Lp-convergence for all p ≠ 0.
theorem
MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{p : ENNReal}
{f : ι → α → E}
{g : α → E}
{l : Filter ι}
(hp_ne_zero : Ne p 0)
(hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ)
(hg : AEStronglyMeasurable g μ)
(hfg : Filter.Tendsto (fun (n : ι) => eLpNorm (HSub.hSub (f n) g) p μ) l (nhds 0))
:
TendstoInMeasure μ f l g
Convergence in Lp implies convergence in measure.
theorem
MeasureTheory.tendstoInMeasure_of_tendsto_Lp
{α : Type u_1}
{ι : Type u_2}
{E : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{p : ENNReal}
[hp : Fact (LE.le 1 p)]
{f : ι → Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x}
{g : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x}
{l : Filter ι}
(hfg : Filter.Tendsto f l (nhds g))
:
TendstoInMeasure μ (fun (n : ι) => (f n).val.cast) l g.val.cast
Convergence in Lp implies convergence in measure.