mathlib documentation

measure_theory.function.convergence_in_measure

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 #

Main results #

def measure_theory.tendsto_in_measure {α : Type u_1} {ι : Type u_2} {E : Type u_3} [has_dist E] {m : measurable_space α} (μ : measure_theory.measure α) (f : ι → α → E) (l : filter ι) (g : α → 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
theorem measure_theory.tendsto_in_measure_iff_norm {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [seminormed_add_comm_group E] {l : filter ι} {f : ι → α → E} {g : α → E} :
measure_theory.tendsto_in_measure μ f l g ∀ (ε : ), 0 < εfilter.tendsto (λ (i : ι), μ {x : α | ε f i x - g x}) l (nhds 0)
@[protected]
theorem measure_theory.tendsto_in_measure.congr' {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [has_dist E] {l : filter ι} {f f' : ι → α → E} {g g' : α → E} (h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i) (h_right : g =ᵐ[μ] g') (h_tendsto : measure_theory.tendsto_in_measure μ f l g) :
@[protected]
theorem measure_theory.tendsto_in_measure.congr {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [has_dist E] {l : filter ι} {f f' : ι → α → E} {g g' : α → E} (h_left : ∀ (i : ι), f i =ᵐ[μ] f' i) (h_right : g =ᵐ[μ] g') (h_tendsto : measure_theory.tendsto_in_measure μ f l g) :
theorem measure_theory.tendsto_in_measure.congr_left {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [has_dist E] {l : filter ι} {f f' : ι → α → E} {g : α → E} (h : ∀ (i : ι), f i =ᵐ[μ] f' i) (h_tendsto : measure_theory.tendsto_in_measure μ f l g) :
theorem measure_theory.tendsto_in_measure.congr_right {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [has_dist E] {l : filter ι} {f : ι → α → E} {g g' : α → E} (h : g =ᵐ[μ] g') (h_tendsto : measure_theory.tendsto_in_measure μ f l g) :
theorem measure_theory.tendsto_in_measure_of_tendsto_ae_of_strongly_measurable {α : Type u_1} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [metric_space E] {f : α → E} {g : α → E} [measure_theory.is_finite_measure μ] (hf : ∀ (n : ), measure_theory.strongly_measurable (f n)) (hg : measure_theory.strongly_measurable g) (hfg : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ), f n x) filter.at_top (nhds (g x))) :

Auxiliary lemma for tendsto_in_measure_of_tendsto_ae.

theorem measure_theory.tendsto_in_measure_of_tendsto_ae {α : Type u_1} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [metric_space E] {f : α → E} {g : α → E} [measure_theory.is_finite_measure μ] (hf : ∀ (n : ), measure_theory.ae_strongly_measurable (f n) μ) (hfg : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ), f n x) filter.at_top (nhds (g x))) :

Convergence a.e. implies convergence in measure in a finite measure space.

theorem measure_theory.exists_seq_tendsto_ae.exists_nat_measure_lt_two_inv {α : Type u_1} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [metric_space E] {f : α → E} {g : α → E} (hfg : measure_theory.tendsto_in_measure μ f filter.at_top g) (n : ) :
∃ (N : ), ∀ (m_1 : ), m_1 Nμ {x : α | 2⁻¹ ^ n has_dist.dist (f m_1 x) (g x)} 2⁻¹ ^ n
noncomputable def measure_theory.exists_seq_tendsto_ae.seq_tendsto_ae_seq_aux {α : Type u_1} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [metric_space E] {f : α → E} {g : α → E} (hfg : measure_theory.tendsto_in_measure μ f filter.at_top g) (n : ) :

Given a sequence of functions f which converges in measure to g, seq_tendsto_ae_seq_aux is a sequence such that ∀ m ≥ seq_tendsto_ae_seq_aux n, μ {x | 2⁻¹ ^ n ≤ dist (f m x) (g x)} ≤ 2⁻¹ ^ n.

Equations
theorem measure_theory.exists_seq_tendsto_ae.seq_tendsto_ae_seq_spec {α : Type u_1} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [metric_space E] {f : α → E} {g : α → E} (hfg : measure_theory.tendsto_in_measure μ f filter.at_top g) (n k : ) (hn : measure_theory.exists_seq_tendsto_ae.seq_tendsto_ae_seq hfg n k) :
μ {x : α | 2⁻¹ ^ n has_dist.dist (f k x) (g x)} 2⁻¹ ^ n
theorem measure_theory.tendsto_in_measure.exists_seq_tendsto_ae {α : Type u_1} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [metric_space E] {f : α → E} {g : α → E} (hfg : measure_theory.tendsto_in_measure μ f filter.at_top g) :
∃ (ns : ), strict_mono ns ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (i : ), f (ns i) x) filter.at_top (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 measure_theory.tendsto_in_measure.exists_seq_tendsto_in_measure_at_top {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [metric_space E] {u : filter ι} [u.ne_bot] [u.is_countably_generated] {f : ι → α → E} {g : α → E} (hfg : measure_theory.tendsto_in_measure μ f u g) :
∃ (ns : → ι), measure_theory.tendsto_in_measure μ (λ (n : ), f (ns n)) filter.at_top g
theorem measure_theory.tendsto_in_measure.exists_seq_tendsto_ae' {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [metric_space E] {u : filter ι} [u.ne_bot] [u.is_countably_generated] {f : ι → α → E} {g : α → E} (hfg : measure_theory.tendsto_in_measure μ f u g) :
∃ (ns : → ι), ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (i : ), f (ns i) x) filter.at_top (nhds (g x))
theorem measure_theory.tendsto_in_measure.ae_measurable {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [measurable_space E] [normed_add_comm_group E] [borel_space E] {u : filter ι} [u.ne_bot] [u.is_countably_generated] {f : ι → α → E} {g : α → E} (hf : ∀ (n : ι), ae_measurable (f n) μ) (h_tendsto : measure_theory.tendsto_in_measure μ f u g) :
theorem measure_theory.tendsto_in_measure_of_tendsto_snorm_of_strongly_measurable {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group E] {p : ennreal} {f : ι → α → E} {g : α → E} (hp_ne_zero : p 0) (hp_ne_top : p ) (hf : ∀ (n : ι), measure_theory.strongly_measurable (f n)) (hg : measure_theory.strongly_measurable g) {l : filter ι} (hfg : filter.tendsto (λ (n : ι), measure_theory.snorm (f n - g) p μ) l (nhds 0)) :

This lemma is superceded by measure_theory.tendsto_in_measure_of_tendsto_snorm where we allow p = ∞ and only require ae_strongly_measurable.

theorem measure_theory.tendsto_in_measure_of_tendsto_snorm_of_ne_top {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group E] {p : ennreal} {f : ι → α → E} {g : α → E} (hp_ne_zero : p 0) (hp_ne_top : p ) (hf : ∀ (n : ι), measure_theory.ae_strongly_measurable (f n) μ) (hg : measure_theory.ae_strongly_measurable g μ) {l : filter ι} (hfg : filter.tendsto (λ (n : ι), measure_theory.snorm (f n - g) p μ) l (nhds 0)) :

This lemma is superceded by measure_theory.tendsto_in_measure_of_tendsto_snorm where we allow p = ∞.

theorem measure_theory.tendsto_in_measure_of_tendsto_snorm_top {α : Type u_1} {ι : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_3} [normed_add_comm_group E] {f : ι → α → E} {g : α → E} {l : filter ι} (hfg : filter.tendsto (λ (n : ι), measure_theory.snorm (f n - g) μ) l (nhds 0)) :

See also measure_theory.tendsto_in_measure_of_tendsto_snorm which work for general Lp-convergence for all p ≠ 0.

theorem measure_theory.tendsto_in_measure_of_tendsto_snorm {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group E] {p : ennreal} {f : ι → α → E} {g : α → E} {l : filter ι} (hp_ne_zero : p 0) (hf : ∀ (n : ι), measure_theory.ae_strongly_measurable (f n) μ) (hg : measure_theory.ae_strongly_measurable g μ) (hfg : filter.tendsto (λ (n : ι), measure_theory.snorm (f n - g) p μ) l (nhds 0)) :

Convergence in Lp implies convergence in measure.

theorem measure_theory.tendsto_in_measure_of_tendsto_Lp {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group E] {p : ennreal} [hp : fact (1 p)] {f : ι → (measure_theory.Lp E p μ)} {g : (measure_theory.Lp E p μ)} {l : filter ι} (hfg : filter.tendsto f l (nhds g)) :
measure_theory.tendsto_in_measure μ (λ (n : ι), (f n)) l g

Convergence in Lp implies convergence in measure.