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): f converges in μ-measure to g.

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: if f is a sequence of functions which converges in measure to g, then f has a subsequence which convergence almost everywhere to g.
• MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm: convergence in Lp implies convergence in measure.

def MeasureTheory.TendstoInMeasure {α : Type u_1} {ι : Type u_2} {E : Type u_3} [Dist E] : {x : MeasurableSpace α} → MeasureTheory.Measure α → (ι → α → E) → Filter ι → (α → E) → Prop

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

• MeasureTheory.TendstoInMeasure μ f l g = ∀ (ε : ℝ), 0 < ε → Filter.Tendsto (fun (i : ι) => μ {x : α | ε ≤ dist (f i x) (g x)}) l (nhds 0)

theorem MeasureTheory.tendstoInMeasure_iff_norm {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [SeminormedAddCommGroup E] {l : Filter ι} {f : ι → α → E} {g : α → E} : MeasureTheory.TendstoInMeasure μ f l g ↔ ∀ (ε : ℝ), 0 < ε → Filter.Tendsto (fun (i : ι) => μ {x : α | ε ≤ ‖f i x - g x‖}) l (nhds 0)

theorem MeasureTheory.TendstoInMeasure.congr' {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Dist E] {l : Filter ι} {f : ι → α → E} {f' : ι → α → E} {g : α → E} {g' : α → E} (h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i) (h_right : g =ᵐ[μ] g') (h_tendsto : MeasureTheory.TendstoInMeasure μ f l g) : MeasureTheory.TendstoInMeasure μ f' l g'

theorem MeasureTheory.TendstoInMeasure.congr {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Dist E] {l : Filter ι} {f : ι → α → E} {f' : ι → α → E} {g : α → E} {g' : α → E} (h_left : ∀ (i : ι), f i =ᵐ[μ] f' i) (h_right : g =ᵐ[μ] g') (h_tendsto : MeasureTheory.TendstoInMeasure μ f l g) : MeasureTheory.TendstoInMeasure μ f' l g'

theorem MeasureTheory.TendstoInMeasure.congr_left {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Dist E] {l : Filter ι} {f : ι → α → E} {f' : ι → α → E} {g : α → E} (h : ∀ (i : ι), f i =ᵐ[μ] f' i) (h_tendsto : MeasureTheory.TendstoInMeasure μ f l g) : MeasureTheory.TendstoInMeasure μ f' l g

theorem MeasureTheory.TendstoInMeasure.congr_right {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Dist E] {l : Filter ι} {f : ι → α → E} {g : α → E} {g' : α → E} (h : g =ᵐ[μ] g') (h_tendsto : MeasureTheory.TendstoInMeasure μ f l g) : MeasureTheory.TendstoInMeasure μ f l g'

theorem MeasureTheory.tendstoInMeasure_of_tendsto_ae_of_stronglyMeasurable {α : Type u_1} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MetricSpace E] {f : ℕ → α → E} {g : α → E} [MeasureTheory.IsFiniteMeasure μ] (hf : ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (f n)) (hg : MeasureTheory.StronglyMeasurable g) (hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))) : MeasureTheory.TendstoInMeasure μ f Filter.atTop g

Auxiliary lemma for tendstoInMeasure_of_tendsto_ae.

theorem MeasureTheory.tendstoInMeasure_of_tendsto_ae {α : Type u_1} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MetricSpace E] {f : ℕ → α → E} {g : α → E} [MeasureTheory.IsFiniteMeasure μ] (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) (hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))) : MeasureTheory.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_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MetricSpace E] {f : ℕ → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) (n : ℕ) : ∃ (N : ℕ), ∀ m_1 ≥ N, μ {x : α | 2⁻¹ ^ n ≤ dist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n

noncomputable def MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux {α : Type u_1} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MetricSpace E] {f : ℕ → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) (n : ℕ) : ℕ

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

• MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux hfg n = Classical.choose ⋯

noncomputable def MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq {α : Type u_1} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MetricSpace E] {f : ℕ → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) : ℕ → ℕ

Transformation of seqTendstoAeSeqAux to makes sure it is strictly monotone.

Equations

• MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg 0 = MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux hfg 0
• MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg n.succ = max (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux hfg (n + 1)) (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg n + 1)

theorem MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_succ {α : Type u_1} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MetricSpace E] {f : ℕ → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) {n : ℕ} : MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg (n + 1) = max (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux hfg (n + 1)) (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg n + 1)

theorem MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_spec {α : Type u_1} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MetricSpace E] {f : ℕ → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) (n : ℕ) (k : ℕ) (hn : MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg n ≤ k) : μ {x : α | 2⁻¹ ^ n ≤ dist (f k x) (g x)} ≤ 2⁻¹ ^ n

theorem MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_strictMono {α : Type u_1} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MetricSpace E] {f : ℕ → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) : StrictMono (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg)

theorem MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae {α : Type u_1} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MetricSpace E] {f : ℕ → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) : ∃ (ns : ℕ → ℕ), StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (i : ℕ) => f (ns i) x) Filter.atTop (nhds (g x))

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_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MetricSpace E] {u : Filter ι} [u.NeBot] [u.IsCountablyGenerated] {f : ι → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f u g) : ∃ (ns : ℕ → ι), MeasureTheory.TendstoInMeasure μ (fun (n : ℕ) => f (ns n)) Filter.atTop g

theorem MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae' {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MetricSpace E] {u : Filter ι} [u.NeBot] [u.IsCountablyGenerated] {f : ι → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f u g) : ∃ (ns : ℕ → ι), ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (i : ℕ) => f (ns i) x) Filter.atTop (nhds (g x))

theorem MeasureTheory.TendstoInMeasure.aemeasurable {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E] {u : Filter ι} [u.NeBot] [u.IsCountablyGenerated] {f : ι → α → E} {g : α → E} (hf : ∀ (n : ι), AEMeasurable (f n) μ) (h_tendsto : MeasureTheory.TendstoInMeasure μ f u g) : AEMeasurable g μ

theorem MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {p : ENNReal} {f : ι → α → E} {g : α → E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) (hg : MeasureTheory.StronglyMeasurable g) {l : Filter ι} (hfg : Filter.Tendsto (fun (n : ι) => MeasureTheory.eLpNorm (f n - g) p μ) l (nhds 0)) : MeasureTheory.TendstoInMeasure μ f l g

This lemma is superseded by MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm where we allow p = ∞ and only require AEStronglyMeasurable.

@[deprecated MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable]

theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm_of_stronglyMeasurable {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {p : ENNReal} {f : ι → α → E} {g : α → E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) (hg : MeasureTheory.StronglyMeasurable g) {l : Filter ι} (hfg : Filter.Tendsto (fun (n : ι) => MeasureTheory.eLpNorm (f n - g) p μ) l (nhds 0)) : MeasureTheory.TendstoInMeasure μ f l g

Alias of MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable.

---

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_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {p : ENNReal} {f : ι → α → E} {g : α → E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hf : ∀ (n : ι), MeasureTheory.AEStronglyMeasurable (f n) μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) {l : Filter ι} (hfg : Filter.Tendsto (fun (n : ι) => MeasureTheory.eLpNorm (f n - g) p μ) l (nhds 0)) : MeasureTheory.TendstoInMeasure μ f l g

This lemma is superseded by MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm where we allow p = ∞.

@[deprecated MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top]

theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm_of_ne_top {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {p : ENNReal} {f : ι → α → E} {g : α → E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hf : ∀ (n : ι), MeasureTheory.AEStronglyMeasurable (f n) μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) {l : Filter ι} (hfg : Filter.Tendsto (fun (n : ι) => MeasureTheory.eLpNorm (f n - g) p μ) l (nhds 0)) : MeasureTheory.TendstoInMeasure μ f l g

Alias of MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top.

---

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 α} {μ : MeasureTheory.Measure α} {E : Type u_4} [NormedAddCommGroup E] {f : ι → α → E} {g : α → E} {l : Filter ι} (hfg : Filter.Tendsto (fun (n : ι) => MeasureTheory.eLpNorm (f n - g) ⊤ μ) l (nhds 0)) : MeasureTheory.TendstoInMeasure μ f l g

See also MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm which work for general Lp-convergence for all p ≠ 0.

@[deprecated MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_top]

theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm_top {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_4} [NormedAddCommGroup E] {f : ι → α → E} {g : α → E} {l : Filter ι} (hfg : Filter.Tendsto (fun (n : ι) => MeasureTheory.eLpNorm (f n - g) ⊤ μ) l (nhds 0)) : MeasureTheory.TendstoInMeasure μ f l g

Alias of MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_top.

---

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_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {p : ENNReal} {f : ι → α → E} {g : α → E} {l : Filter ι} (hp_ne_zero : p ≠ 0) (hf : ∀ (n : ι), MeasureTheory.AEStronglyMeasurable (f n) μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (hfg : Filter.Tendsto (fun (n : ι) => MeasureTheory.eLpNorm (f n - g) p μ) l (nhds 0)) : MeasureTheory.TendstoInMeasure μ f l g

Convergence in Lp implies convergence in measure.

@[deprecated MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm]

theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {p : ENNReal} {f : ι → α → E} {g : α → E} {l : Filter ι} (hp_ne_zero : p ≠ 0) (hf : ∀ (n : ι), MeasureTheory.AEStronglyMeasurable (f n) μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (hfg : Filter.Tendsto (fun (n : ι) => MeasureTheory.eLpNorm (f n - g) p μ) l (nhds 0)) : MeasureTheory.TendstoInMeasure μ f l g

Alias of MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm.

---

Convergence in Lp implies convergence in measure.

theorem MeasureTheory.tendstoInMeasure_of_tendsto_Lp {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {p : ENNReal} [hp : Fact (1 ≤ p)] {f : ι → ↥(MeasureTheory.Lp E p μ)} {g : ↥(MeasureTheory.Lp E p μ)} {l : Filter ι} (hfg : Filter.Tendsto f l (nhds g)) : MeasureTheory.TendstoInMeasure μ (fun (n : ι) => ↑↑(f n)) l ↑↑g

Convergence in Lp implies convergence in measure.