# Documentation

Mathlib.MeasureTheory.Function.UniformIntegrable

# 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 establishes 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 formulate the martingale convergence theorem.

## Main definitions #

• MeasureTheory.UnifIntegrable: uniform integrability in the measure theory sense. In particular, a sequence of functions f is uniformly integrable if for all ε > 0, there exists some δ > 0 such that for all sets s of smaller measure than δ, the Lp-norm of f i restricted s is smaller than ε for all i.
• MeasureTheory.UniformIntegrable: uniform integrability in the probability theory sense. In particular, a sequence of measurable functions f is uniformly integrable in the probability theory sense if it is uniformly integrable in the measure theory sense and has uniformly bounded Lp-norm.

# Main results #

• MeasureTheory.unifIntegrable_finite: a finite sequence of Lp functions is uniformly integrable.
• MeasureTheory.tendsto_Lp_of_tendsto_ae: a sequence of Lp functions which is uniformly integrable converges in Lp if they converge almost everywhere.
• MeasureTheory.tendstoInMeasure_iff_tendsto_Lp: Vitali convergence theorem: a sequence of Lp functions converges in Lp if and only if it is uniformly integrable and converges in measure.

## Tags #

uniform integrable, uniformly absolutely continuous integral, Vitali convergence theorem

def MeasureTheory.UnifIntegrable {α : Type u_1} {β : Type u_2} {ι : Type u_3} :
{x : } → (ιαβ) →

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 integrability is also known as uniformly absolutely continuous integrals.

Instances For
def MeasureTheory.UniformIntegrable {α : Type u_1} {β : Type u_2} {ι : Type u_3} :
{x : } → (ιαβ) →

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.

Instances For
theorem MeasureTheory.UniformIntegrable.aeStronglyMeasurable {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {f : ιαβ} {p : ENNReal} (hf : ) (i : ι) :
theorem MeasureTheory.UniformIntegrable.unifIntegrable {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {f : ιαβ} {p : ENNReal} (hf : ) :
theorem MeasureTheory.UniformIntegrable.memℒp {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {f : ιαβ} {p : ENNReal} (hf : ) (i : ι) :

### UnifIntegrable#

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

theorem MeasureTheory.UnifIntegrable.add {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {f : ιαβ} {g : ιαβ} {p : ENNReal} (hf : ) (hg : ) (hp : 1 p) (hf_meas : ∀ (i : ι), ) (hg_meas : ∀ (i : ι), ) :
theorem MeasureTheory.UnifIntegrable.neg {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {f : ιαβ} {p : ENNReal} (hf : ) :
theorem MeasureTheory.UnifIntegrable.sub {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {f : ιαβ} {g : ιαβ} {p : ENNReal} (hf : ) (hg : ) (hp : 1 p) (hf_meas : ∀ (i : ι), ) (hg_meas : ∀ (i : ι), ) :
theorem MeasureTheory.UnifIntegrable.ae_eq {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {f : ιαβ} {g : ιαβ} {p : ENNReal} (hf : ) (hfg : ∀ (n : ι), f n =ᶠ[] g n) :
theorem MeasureTheory.unifIntegrable_zero_meas {α : Type u_1} {β : Type u_2} {ι : Type u_3} [] {p : ENNReal} {f : ιαβ} :
theorem MeasureTheory.unifIntegrable_congr_ae {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {p : ENNReal} {f : ιαβ} {g : ιαβ} (hfg : ∀ (n : ι), f n =ᶠ[] g n) :
theorem MeasureTheory.tendsto_indicator_ge {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
Filter.Tendsto (fun M => Set.indicator {x | M f x‖₊} f x) Filter.atTop (nhds 0)
theorem MeasureTheory.Memℒp.integral_indicator_norm_ge_le {α : Type u_1} {β : Type u_2} {m : } (μ : ) {f : αβ} (hf : ) (hmeas : ) {ε : } (hε : 0 < ε) :
M, ∫⁻ (x : α), Set.indicator {x | M f x‖₊} f x‖₊μ

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

theorem MeasureTheory.Memℒp.integral_indicator_norm_ge_nonneg_le_of_meas {α : Type u_1} {β : Type u_2} {m : } (μ : ) {f : αβ} (hf : ) (hmeas : ) {ε : } (hε : 0 < ε) :
M, 0 M ∫⁻ (x : α), Set.indicator {x | M f x‖₊} f x‖₊μ

This lemma is superceded by MeasureTheory.Memℒp.integral_indicator_norm_ge_nonneg_le which does not require measurability.

theorem MeasureTheory.Memℒp.integral_indicator_norm_ge_nonneg_le {α : Type u_1} {β : Type u_2} {m : } (μ : ) {f : αβ} (hf : ) {ε : } (hε : 0 < ε) :
M, 0 M ∫⁻ (x : α), Set.indicator {x | M f x‖₊} f x‖₊μ
theorem MeasureTheory.Memℒp.snormEssSup_indicator_norm_ge_eq_zero {α : Type u_1} {β : Type u_2} {m : } (μ : ) {f : αβ} (hf : ) (hmeas : ) :
M, MeasureTheory.snormEssSup (Set.indicator {x | M f x‖₊} f) μ = 0
theorem MeasureTheory.Memℒp.snorm_indicator_norm_ge_le {α : Type u_1} {β : Type u_2} {m : } (μ : ) {p : ENNReal} {f : αβ} (hf : ) (hmeas : ) {ε : } (hε : 0 < ε) :
M, MeasureTheory.snorm (Set.indicator {x | M f x‖₊} f) p μ
theorem MeasureTheory.Memℒp.snorm_indicator_norm_ge_pos_le {α : Type u_1} {β : Type u_2} {m : } (μ : ) {p : ENNReal} {f : αβ} (hf : ) (hmeas : ) {ε : } (hε : 0 < ε) :
M, 0 < M MeasureTheory.snorm (Set.indicator {x | M f x‖₊} f) p μ

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

theorem MeasureTheory.snorm_indicator_le_of_bound {α : Type u_1} {β : Type u_2} {m : } (μ : ) {p : ENNReal} {f : αβ} (hp_top : p ) {ε : } (hε : 0 < ε) {M : } (hf : ∀ (x : α), f x < M) :
δ , ∀ (s : Set α), μ s MeasureTheory.snorm () p μ
theorem MeasureTheory.Memℒp.snorm_indicator_le' {α : Type u_1} {β : Type u_2} {m : } (μ : ) {p : ENNReal} {f : αβ} (hp_one : 1 p) (hp_top : p ) (hf : ) (hmeas : ) {ε : } (hε : 0 < ε) :
δ , ∀ (s : Set α), μ s MeasureTheory.snorm () p μ

Auxiliary lemma for MeasureTheory.Memℒp.snorm_indicator_le.

theorem MeasureTheory.Memℒp.snorm_indicator_le_of_meas {α : Type u_1} {β : Type u_2} {m : } (μ : ) {p : ENNReal} {f : αβ} (hp_one : 1 p) (hp_top : p ) (hf : ) (hmeas : ) {ε : } (hε : 0 < ε) :
δ , ∀ (s : Set α), μ s MeasureTheory.snorm () p μ

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

theorem MeasureTheory.Memℒp.snorm_indicator_le {α : Type u_1} {β : Type u_2} {m : } (μ : ) {p : ENNReal} {f : αβ} (hp_one : 1 p) (hp_top : p ) (hf : ) {ε : } (hε : 0 < ε) :
δ , ∀ (s : Set α), μ s MeasureTheory.snorm () p μ
theorem MeasureTheory.unifIntegrable_const {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } (μ : ) {p : ENNReal} {g : αβ} (hp : 1 p) (hp_ne_top : p ) (hg : ) :

A constant function is uniformly integrable.

theorem MeasureTheory.unifIntegrable_subsingleton {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } (μ : ) {p : ENNReal} [] (hp_one : 1 p) (hp_top : p ) {f : ιαβ} (hf : ∀ (i : ι), MeasureTheory.Memℒp (f i) p) :

A single function is uniformly integrable.

theorem MeasureTheory.unifIntegrable_fin {α : Type u_1} {β : Type u_2} {m : } (μ : ) {p : ENNReal} (hp_one : 1 p) (hp_top : p ) {n : } {f : Fin nαβ} (hf : ∀ (i : Fin n), MeasureTheory.Memℒp (f i) p) :

This lemma is less general than MeasureTheory.unifIntegrable_finite which applies to all sequences indexed by a finite type.

theorem MeasureTheory.unifIntegrable_finite {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } (μ : ) {p : ENNReal} [] (hp_one : 1 p) (hp_top : p ) {f : ιαβ} (hf : ∀ (i : ι), MeasureTheory.Memℒp (f i) p) :

A finite sequence of Lp functions is uniformly integrable.

theorem MeasureTheory.snorm_sub_le_of_dist_bdd {α : Type u_1} {β : Type u_2} {m : } (μ : ) {p : ENNReal} (hp' : p ) {s : Set α} (hs : ) {f : αβ} {g : αβ} {c : } (hc : 0 c) (hf : ∀ (x : α), x sdist (f x) (g x) c) :
MeasureTheory.snorm (Set.indicator s (f - g)) p μ * μ s ^ ()
theorem MeasureTheory.tendsto_Lp_of_tendsto_ae_of_meas {α : Type u_1} {β : Type u_2} {m : } (μ : ) {p : ENNReal} (hp : 1 p) (hp' : p ) {f : αβ} {g : αβ} (hf : ∀ (n : ), ) (hg : ) (hg' : ) (hui : ) (hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) :
Filter.Tendsto (fun n => MeasureTheory.snorm (f n - g) p μ) Filter.atTop (nhds 0)

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

theorem MeasureTheory.tendsto_Lp_of_tendsto_ae {α : Type u_1} {β : Type u_2} {m : } (μ : ) {p : ENNReal} (hp : 1 p) (hp' : p ) {f : αβ} {g : αβ} (hf : ∀ (n : ), ) (hg : ) (hui : ) (hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) :
Filter.Tendsto (fun n => MeasureTheory.snorm (f n - g) p μ) Filter.atTop (nhds 0)

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

theorem MeasureTheory.unifIntegrable_of_tendsto_Lp_zero {α : Type u_1} {β : Type u_2} {m : } (μ : ) {p : ENNReal} {f : αβ} (hp : 1 p) (hp' : p ) (hf : ∀ (n : ), MeasureTheory.Memℒp (f n) p) (hf_tendsto : Filter.Tendsto (fun n => MeasureTheory.snorm (f n) p μ) Filter.atTop (nhds 0)) :
theorem MeasureTheory.unifIntegrable_of_tendsto_Lp {α : Type u_1} {β : Type u_2} {m : } (μ : ) {p : ENNReal} {f : αβ} {g : αβ} (hp : 1 p) (hp' : p ) (hf : ∀ (n : ), MeasureTheory.Memℒp (f n) p) (hg : ) (hfg : Filter.Tendsto (fun n => MeasureTheory.snorm (f n - g) p μ) Filter.atTop (nhds 0)) :

Convergence in Lp implies uniform integrability.

theorem MeasureTheory.tendsto_Lp_of_tendstoInMeasure {α : Type u_1} {β : Type u_2} {m : } (μ : ) {p : ENNReal} {f : αβ} {g : αβ} (hp : 1 p) (hp' : p ) (hf : ∀ (n : ), ) (hg : ) (hui : ) (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) :
Filter.Tendsto (fun n => MeasureTheory.snorm (f n - g) p μ) Filter.atTop (nhds 0)

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 MeasureTheory.tendstoInMeasure_iff_tendsto_Lp {α : Type u_1} {β : Type u_2} {m : } (μ : ) {p : ENNReal} {f : αβ} {g : αβ} (hp : 1 p) (hp' : p ) (hf : ∀ (n : ), MeasureTheory.Memℒp (f n) p) (hg : ) :
MeasureTheory.TendstoInMeasure μ f Filter.atTop g Filter.Tendsto (fun n => MeasureTheory.snorm (f n - g) p μ) Filter.atTop (nhds 0)

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 MeasureTheory.unifIntegrable_of' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } (μ : ) {p : ENNReal} (hp : 1 p) (hp' : p ) {f : ιαβ} (hf : ∀ (i : ι), ) (h : ∀ (ε : ), 0 < εC, 0 < C ∀ (i : ι), MeasureTheory.snorm (Set.indicator {x | C f i x‖₊} (f i)) p μ ) :

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

theorem MeasureTheory.unifIntegrable_of {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } (μ : ) {p : ENNReal} (hp : 1 p) (hp' : p ) {f : ιαβ} (hf : ∀ (i : ι), ) (h : ∀ (ε : ), 0 < εC, ∀ (i : ι), MeasureTheory.snorm (Set.indicator {x | C f i x‖₊} (f i)) p μ ) :

UniformIntegrable

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 develop some API for UniformIntegrable and prove that UniformIntegrable is equivalent to this definition of uniform integrability.

theorem MeasureTheory.uniformIntegrable_zero_meas {α : Type u_1} {β : Type u_2} {ι : Type u_3} {p : ENNReal} {f : ιαβ} [] :
theorem MeasureTheory.UniformIntegrable.ae_eq {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {p : ENNReal} {f : ιαβ} {g : ιαβ} (hf : ) (hfg : ∀ (n : ι), f n =ᶠ[] g n) :
theorem MeasureTheory.uniformIntegrable_congr_ae {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {p : ENNReal} {f : ιαβ} {g : ιαβ} (hfg : ∀ (n : ι), f n =ᶠ[] g n) :
theorem MeasureTheory.uniformIntegrable_finite {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {p : ENNReal} {f : ιαβ} [] (hp_one : 1 p) (hp_top : p ) (hf : ∀ (i : ι), MeasureTheory.Memℒp (f i) p) :

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

theorem MeasureTheory.uniformIntegrable_subsingleton {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {p : ENNReal} {f : ιαβ} [] (hp_one : 1 p) (hp_top : p ) (hf : ∀ (i : ι), MeasureTheory.Memℒp (f i) p) :

A single function is uniformly integrable in the probability sense.

theorem MeasureTheory.uniformIntegrable_const {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {p : ENNReal} {g : αβ} (hp : 1 p) (hp_ne_top : p ) (hg : ) :

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

theorem MeasureTheory.uniformIntegrable_of' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {p : ENNReal} {f : ιαβ} (hp : 1 p) (hp' : p ) (hf : ∀ (i : ι), ) (h : ∀ (ε : ), 0 < εC, ∀ (i : ι), MeasureTheory.snorm (Set.indicator {x | C f i x‖₊} (f i)) p μ ) :

This lemma is superceded by uniformIntegrable_of which only requires AEStronglyMeasurable.

theorem MeasureTheory.uniformIntegrable_of {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {p : ENNReal} {f : ιαβ} (hp : 1 p) (hp' : p ) (hf : ∀ (i : ι), ) (h : ∀ (ε : ), 0 < εC, ∀ (i : ι), MeasureTheory.snorm (Set.indicator {x | C f i x‖₊} (f i)) p μ ) :

A sequence 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 MeasureTheory.UniformIntegrable.spec' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {p : ENNReal} {f : ιαβ} (hp : p 0) (hp' : p ) (hf : ∀ (i : ι), ) (hfu : ) {ε : } (hε : 0 < ε) :
C, ∀ (i : ι), MeasureTheory.snorm (Set.indicator {x | C f i x‖₊} (f i)) p μ

This lemma is superceded by UniformIntegrable.spec which does not require measurability.

theorem MeasureTheory.UniformIntegrable.spec {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {p : ENNReal} {f : ιαβ} (hp : p 0) (hp' : p ) (hfu : ) {ε : } (hε : 0 < ε) :
C, ∀ (i : ι), MeasureTheory.snorm (Set.indicator {x | C f i x‖₊} (f i)) p μ
theorem MeasureTheory.uniformIntegrable_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } {μ : } {p : ENNReal} {f : ιαβ} (hp : 1 p) (hp' : p ) :
(∀ (i : ι), ) ∀ (ε : ), 0 < εC, ∀ (i : ι), MeasureTheory.snorm (Set.indicator {x | C f i x‖₊} (f i)) p μ

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

theorem MeasureTheory.uniformIntegrable_average {α : Type u_1} {m : } {μ : } {p : ENNReal} (hp : 1 p) {f : α} (hf : ) :
MeasureTheory.UniformIntegrable (fun n => (Finset.sum () fun i => f i) / n) p μ

The averaging of a uniformly integrable sequence is also uniformly integrable.