mathlib documentation

measure_theory.function.uniform_integrable

Uniform integrability #

This file contains the definitions for uniform integrability (both in the measure theory sense as well as the probability theory sense). This file also contains the Vitali convergence theorem which estabishes a relation between uniform integrability, convergence in measure and Lp convergence.

Uniform integrability plays a vital role in the theory of martingales most notably is used to fomulate the martingale convergence theorem.

Main definitions #

Main results #

Tags #

uniform integrable, uniformly absolutely continuous integral, Vitali convergence theorem

def measure_theory.unif_integrable {α : Type u_1} {β : Type u_2} {ι : Type u_3} [normed_group β] {m : measurable_space α} (f : ι → α → β) (p : ennreal) (μ : measure_theory.measure α) :
Prop

Uniform integrability in the measure theory sense.

A sequence of functions f is said to be uniformly integrable if for all ε > 0, there exists some δ > 0 such that for all sets s with measure less than δ, the Lp-norm of f i restricted on s is less than ε.

Uniform integrablility is also known as uniformly absolutely continuous integrals.

Equations
def measure_theory.uniform_integrable {α : Type u_1} {β : Type u_2} {ι : Type u_3} [normed_group β] {m : measurable_space α} (f : ι → α → β) (p : ennreal) (μ : measure_theory.measure α) :
Prop

In probability theory, a family of measurable functions is uniformly integrable if it is uniformly integrable in the measure theory sense and is uniformly bounded.

Equations
theorem measure_theory.uniform_integrable.strongly_measurable {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : ι → α → β} {p : ennreal} (hf : measure_theory.uniform_integrable f p μ) (i : ι) :
theorem measure_theory.uniform_integrable.unif_integrable {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : ι → α → β} {p : ennreal} (hf : measure_theory.uniform_integrable f p μ) :
theorem measure_theory.uniform_integrable.mem_ℒp {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : ι → α → β} {p : ennreal} (hf : measure_theory.uniform_integrable f p μ) (i : ι) :

unif_integrable #

This section deals with uniform integrability in the measure theory sense.

@[protected]
theorem measure_theory.unif_integrable.add {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f g : ι → α → β} {p : ennreal} (hf : measure_theory.unif_integrable f p μ) (hg : measure_theory.unif_integrable g p μ) (hp : 1 p) (hf_meas : ∀ (i : ι), measure_theory.ae_strongly_measurable (f i) μ) (hg_meas : ∀ (i : ι), measure_theory.ae_strongly_measurable (g i) μ) :
@[protected]
theorem measure_theory.unif_integrable.neg {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : ι → α → β} {p : ennreal} (hf : measure_theory.unif_integrable f p μ) :
@[protected]
theorem measure_theory.unif_integrable.sub {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f g : ι → α → β} {p : ennreal} (hf : measure_theory.unif_integrable f p μ) (hg : measure_theory.unif_integrable g p μ) (hp : 1 p) (hf_meas : ∀ (i : ι), measure_theory.ae_strongly_measurable (f i) μ) (hg_meas : ∀ (i : ι), measure_theory.ae_strongly_measurable (g i) μ) :
@[protected]
theorem measure_theory.unif_integrable.ae_eq {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f g : ι → α → β} {p : ennreal} (hf : measure_theory.unif_integrable f p μ) (hfg : ∀ (n : ι), f n =ᵐ[μ] g n) :
theorem measure_theory.unif_integrable_zero_meas {α : Type u_1} {β : Type u_2} {ι : Type u_3} [normed_group β] [measurable_space α] {p : ennreal} {f : ι → α → β} :
theorem measure_theory.unif_integrable_congr_ae {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {p : ennreal} {f g : ι → α → β} (hfg : ∀ (n : ι), f n =ᵐ[μ] g n) :
theorem measure_theory.tendsto_indicator_ge {α : Type u_1} {β : Type u_2} [normed_group β] (f : α → β) (x : α) :
filter.tendsto (λ (M : ), {x : α | M f x∥₊}.indicator f x) filter.at_top (nhds 0)
theorem measure_theory.mem_ℒp.integral_indicator_norm_ge_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {f : α → β} (hf : measure_theory.mem_ℒp f 1 μ) (hmeas : measure_theory.strongly_measurable f) {ε : } (hε : 0 < ε) :
∃ (M : ), ∫⁻ (x : α), {x : α | M f x∥₊}.indicator f x∥₊ μ ennreal.of_real ε

This lemma is weaker than measure_theory.mem_ℒp.integral_indicator_norm_ge_nonneg_le as the latter provides 0 ≤ M and does not require the measurability of f.

theorem measure_theory.mem_ℒp.integral_indicator_norm_ge_nonneg_le_of_meas {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {f : α → β} (hf : measure_theory.mem_ℒp f 1 μ) (hmeas : measure_theory.strongly_measurable f) {ε : } (hε : 0 < ε) :
∃ (M : ), 0 M ∫⁻ (x : α), {x : α | M f x∥₊}.indicator f x∥₊ μ ennreal.of_real ε

This lemma is superceded by measure_theory.mem_ℒp.integral_indicator_norm_ge_nonneg_le which does not require measurability.

theorem measure_theory.mem_ℒp.integral_indicator_norm_ge_nonneg_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {f : α → β} (hf : measure_theory.mem_ℒp f 1 μ) {ε : } (hε : 0 < ε) :
∃ (M : ), 0 M ∫⁻ (x : α), {x : α | M f x∥₊}.indicator f x∥₊ μ ennreal.of_real ε
theorem measure_theory.mem_ℒp.snorm_ess_sup_indicator_norm_ge_eq_zero {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {f : α → β} (hf : measure_theory.mem_ℒp f μ) (hmeas : measure_theory.strongly_measurable f) :
∃ (M : ), measure_theory.snorm_ess_sup ({x : α | M f x∥₊}.indicator f) μ = 0
theorem measure_theory.mem_ℒp.snorm_indicator_norm_ge_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} {f : α → β} (hf : measure_theory.mem_ℒp f p μ) (hmeas : measure_theory.strongly_measurable f) {ε : } (hε : 0 < ε) :
∃ (M : ), measure_theory.snorm ({x : α | M f x∥₊}.indicator f) p μ ennreal.of_real ε
theorem measure_theory.mem_ℒp.snorm_indicator_norm_ge_pos_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} {f : α → β} (hf : measure_theory.mem_ℒp f p μ) (hmeas : measure_theory.strongly_measurable f) {ε : } (hε : 0 < ε) :
∃ (M : ), 0 < M measure_theory.snorm ({x : α | M f x∥₊}.indicator f) p μ ennreal.of_real ε

This lemma implies that a single function is uniformly integrable (in the probability sense).

theorem measure_theory.snorm_indicator_le_of_bound {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} {f : α → β} (hp_top : p ) {ε : } (hε : 0 < ε) {M : } (hf : ∀ (x : α), f x < M) :
∃ (δ : ) (hδ : 0 < δ), ∀ (s : set α), measurable_set sμ s ennreal.of_real δmeasure_theory.snorm (s.indicator f) p μ ennreal.of_real ε
theorem measure_theory.mem_ℒp.snorm_indicator_le' {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} {f : α → β} (hp_one : 1 p) (hp_top : p ) (hf : measure_theory.mem_ℒp f p μ) (hmeas : measure_theory.strongly_measurable f) {ε : } (hε : 0 < ε) :
∃ (δ : ) (hδ : 0 < δ), ∀ (s : set α), measurable_set sμ s ennreal.of_real δmeasure_theory.snorm (s.indicator f) p μ 2 * ennreal.of_real ε

Auxiliary lemma for measure_theory.mem_ℒp.snorm_indicator_le.

theorem measure_theory.mem_ℒp.snorm_indicator_le_of_meas {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} {f : α → β} (hp_one : 1 p) (hp_top : p ) (hf : measure_theory.mem_ℒp f p μ) (hmeas : measure_theory.strongly_measurable f) {ε : } (hε : 0 < ε) :
∃ (δ : ) (hδ : 0 < δ), ∀ (s : set α), measurable_set sμ s ennreal.of_real δmeasure_theory.snorm (s.indicator f) p μ ennreal.of_real ε

This lemma is superceded by measure_theory.mem_ℒp.snorm_indicator_le which does not require measurability on f.

theorem measure_theory.mem_ℒp.snorm_indicator_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} {f : α → β} (hp_one : 1 p) (hp_top : p ) (hf : measure_theory.mem_ℒp f p μ) {ε : } (hε : 0 < ε) :
∃ (δ : ) (hδ : 0 < δ), ∀ (s : set α), measurable_set sμ s ennreal.of_real δmeasure_theory.snorm (s.indicator f) p μ ennreal.of_real ε
theorem measure_theory.unif_integrable_const {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} {g : α → β} (hp : 1 p) (hp_ne_top : p ) (hg : measure_theory.mem_ℒp g p μ) :
measure_theory.unif_integrable (λ (n : ι), g) p μ

A constant function is uniformly integrable.

theorem measure_theory.unif_integrable_subsingleton {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} [subsingleton ι] (hp_one : 1 p) (hp_top : p ) {f : ι → α → β} (hf : ∀ (i : ι), measure_theory.mem_ℒp (f i) p μ) :

A single function is uniformly integrable.

theorem measure_theory.unif_integrable_fin {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} (hp_one : 1 p) (hp_top : p ) {n : } {f : fin nα → β} (hf : ∀ (i : fin n), measure_theory.mem_ℒp (f i) p μ) :

This lemma is less general than measure_theory.unif_integrable_fintype which applies to all sequences indexed by a fintype.

theorem measure_theory.unif_integrable_fintype {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} [fintype ι] (hp_one : 1 p) (hp_top : p ) {f : ι → α → β} (hf : ∀ (i : ι), measure_theory.mem_ℒp (f i) p μ) :

A finite sequence of Lp functions is uniformly integrable.

theorem measure_theory.snorm_sub_le_of_dist_bdd {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} (hp' : p ) {s : set α} (hs : measurable_set s) {f g : α → β} {c : } (hc : 0 c) (hf : ∀ (x : α), x shas_dist.dist (f x) (g x) c) :
theorem measure_theory.tendsto_Lp_of_tendsto_ae_of_meas {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} [measure_theory.is_finite_measure μ] (hp : 1 p) (hp' : p ) {f : α → β} {g : α → β} (hf : ∀ (n : ), measure_theory.strongly_measurable (f n)) (hg : measure_theory.strongly_measurable g) (hg' : measure_theory.mem_ℒp g p μ) (hui : measure_theory.unif_integrable f p μ) (hfg : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ), f n x) filter.at_top (nhds (g x))) :

A sequence of uniformly integrable functions which converges μ-a.e. converges in Lp.

theorem measure_theory.tendsto_Lp_of_tendsto_ae {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} [measure_theory.is_finite_measure μ] (hp : 1 p) (hp' : p ) {f : α → β} {g : α → β} (hf : ∀ (n : ), measure_theory.ae_strongly_measurable (f n) μ) (hg : measure_theory.mem_ℒp g p μ) (hui : measure_theory.unif_integrable f p μ) (hfg : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ), f n x) filter.at_top (nhds (g x))) :

A sequence of uniformly integrable functions which converges μ-a.e. converges in Lp.

theorem measure_theory.unif_integrable_of_tendsto_Lp_zero {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} {f : α → β} (hp : 1 p) (hp' : p ) (hf : ∀ (n : ), measure_theory.mem_ℒp (f n) p μ) (hf_tendsto : filter.tendsto (λ (n : ), measure_theory.snorm (f n) p μ) filter.at_top (nhds 0)) :
theorem measure_theory.unif_integrable_of_tendsto_Lp {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} {f : α → β} {g : α → β} (hp : 1 p) (hp' : p ) (hf : ∀ (n : ), measure_theory.mem_ℒp (f n) p μ) (hg : measure_theory.mem_ℒp g p μ) (hfg : filter.tendsto (λ (n : ), measure_theory.snorm (f n - g) p μ) filter.at_top (nhds 0)) :

Convergence in Lp implies uniform integrability.

theorem measure_theory.tendsto_Lp_of_tendsto_in_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} {f : α → β} {g : α → β} [measure_theory.is_finite_measure μ] (hp : 1 p) (hp' : p ) (hf : ∀ (n : ), measure_theory.ae_strongly_measurable (f n) μ) (hg : measure_theory.mem_ℒp g p μ) (hui : measure_theory.unif_integrable f p μ) (hfg : measure_theory.tendsto_in_measure μ f filter.at_top g) :

Forward direction of Vitali's convergence theorem: if f is a sequence of uniformly integrable functions that converge in measure to some function g in a finite measure space, then f converge in Lp to g.

theorem measure_theory.tendsto_in_measure_iff_tendsto_Lp {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} {f : α → β} {g : α → β} [measure_theory.is_finite_measure μ] (hp : 1 p) (hp' : p ) (hf : ∀ (n : ), measure_theory.mem_ℒp (f n) p μ) (hg : measure_theory.mem_ℒp g p μ) :

Vitali's convergence theorem: A sequence of functions f converges to g in Lp if and only if it is uniformly integrable and converges to g in measure.

theorem measure_theory.unif_integrable_of' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} (hp : 1 p) (hp' : p ) {f : ι → α → β} (hf : ∀ (i : ι), measure_theory.strongly_measurable (f i)) (h : ∀ (ε : ), 0 < ε(∃ (C : nnreal), 0 < C ∀ (i : ι), measure_theory.snorm ({x : α | C f i x∥₊}.indicator (f i)) p μ ennreal.of_real ε)) :

This lemma is superceded by unif_integrable_of which do not require C to be positive.

theorem measure_theory.unif_integrable_of {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] {p : ennreal} (hp : 1 p) (hp' : p ) {f : ι → α → β} (hf : ∀ (i : ι), measure_theory.strongly_measurable (f i)) (h : ∀ (ε : ), 0 < ε(∃ (C : nnreal), ∀ (i : ι), measure_theory.snorm ({x : α | C f i x∥₊}.indicator (f i)) p μ ennreal.of_real ε)) :

uniform_integrable

In probability theory, uniform integrability normally refers to the condition that a sequence of function (fₙ) satisfies for all ε > 0, there exists some C ≥ 0 such that ∫ x in {|fₙ| ≥ C}, fₙ x ∂μ ≤ ε for all n.

In this section, we will develope some API for uniform_integrable and prove that uniform_integrable is equivalent to this definition of uniform integrability.

theorem measure_theory.uniform_integrable_zero_meas {α : Type u_1} {β : Type u_2} {ι : Type u_3} [normed_group β] {p : ennreal} {f : ι → α → β} [measurable_space α] (hf : ∀ (i : ι), measure_theory.strongly_measurable (f i)) :
theorem measure_theory.uniform_integrable.ae_eq {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {p : ennreal} {f g : ι → α → β} (hf : measure_theory.uniform_integrable f p μ) (hg : ∀ (i : ι), measure_theory.strongly_measurable (g i)) (hfg : ∀ (n : ι), f n =ᵐ[μ] g n) :
theorem measure_theory.uniform_integrable_congr_ae {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {p : ennreal} {f g : ι → α → β} (hf : ∀ (i : ι), measure_theory.strongly_measurable (f i)) (hg : ∀ (i : ι), measure_theory.strongly_measurable (g i)) (hfg : ∀ (n : ι), f n =ᵐ[μ] g n) :
theorem measure_theory.uniform_integrable_fintype {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {p : ennreal} {f : ι → α → β} [fintype ι] (hp_one : 1 p) (hp_top : p ) (hf : ∀ (i : ι), measure_theory.strongly_measurable (f i)) (hf' : ∀ (i : ι), measure_theory.mem_ℒp (f i) p μ) :

A finite sequence of Lp functions is uniformly integrable in the probability sense.

theorem measure_theory.uniform_integrable_subsingleton {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {p : ennreal} {f : ι → α → β} [subsingleton ι] (hp_one : 1 p) (hp_top : p ) (hf : ∀ (i : ι), measure_theory.strongly_measurable (f i)) (hf' : ∀ (i : ι), measure_theory.mem_ℒp (f i) p μ) :

A single function is uniformly integrable in the probability sense.

theorem measure_theory.uniform_integrable_const {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {p : ennreal} {g : α → β} (hp : 1 p) (hp_ne_top : p ) (hgm : measure_theory.strongly_measurable g) (hg : measure_theory.mem_ℒp g p μ) :
measure_theory.uniform_integrable (λ (n : ι), g) p μ

A constant sequence of functions is uniformly integrable in the probability sense.

theorem measure_theory.uniform_integrable_of {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {p : ennreal} {f : ι → α → β} [measure_theory.is_finite_measure μ] (hp : 1 p) (hp' : p ) (hf : ∀ (i : ι), measure_theory.strongly_measurable (f i)) (h : ∀ (ε : ), 0 < ε(∃ (C : nnreal), ∀ (i : ι), measure_theory.snorm ({x : α | C f i x∥₊}.indicator (f i)) p μ ennreal.of_real ε)) :

A sequene of functions (fₙ) is uniformly integrable in the probability sense if for all ε > 0, there exists some C such that ∫ x in {|fₙ| ≥ C}, fₙ x ∂μ ≤ ε for all n.

theorem measure_theory.uniform_integrable.spec {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {p : ennreal} {f : ι → α → β} (hp : p 0) (hp' : p ) (hfu : measure_theory.uniform_integrable f p μ) {ε : } (hε : 0 < ε) :
∃ (C : nnreal), ∀ (i : ι), measure_theory.snorm ({x : α | C f i x∥₊}.indicator (f i)) p μ ennreal.of_real ε
theorem measure_theory.uniform_integrable_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {p : ennreal} {f : ι → α → β} [measure_theory.is_finite_measure μ] (hp : 1 p) (hp' : p ) :
measure_theory.uniform_integrable f p μ (∀ (i : ι), measure_theory.strongly_measurable (f i)) ∀ (ε : ), 0 < ε(∃ (C : nnreal), ∀ (i : ι), measure_theory.snorm ({x : α | C f i x∥₊}.indicator (f i)) p μ ennreal.of_real ε)

The definition of uniform integrable in mathlib is equivalent to the definition commonly found in literature.