Uniform integrability #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
measure_theory.unif_integrable: uniform integrability in the measure theory sense. In particular, a sequence of functionsfis uniformly integrable if for allε > 0, there exists someδ > 0such that for all setssof smaller measure thanδ, the Lp-norm off irestrictedsis smaller thanεfor alli.measure_theory.uniform_integrable: uniform integrability in the probability theory sense. In particular, a sequence of measurable functionsfis 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 #
measure_theory.unif_integrable_fintype: a finite sequence of Lp functions is uniformly integrable.measure_theory.tendsto_Lp_of_tendsto_ae: a sequence of Lp functions which is uniformly integrable converges in Lp if they converge almost everywhere.measure_theory.tendsto_in_measure_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
measure_theory.unif_integrable
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[normed_add_comm_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
- measure_theory.unif_integrable f p μ = ∀ ⦃ε : ℝ⦄, 0 < ε → (∃ (δ : ℝ) (hδ : 0 < δ), ∀ (i : ι) (s : set α), measurable_set s → ⇑μ s ≤ ennreal.of_real δ → measure_theory.snorm (s.indicator (f i)) p μ ≤ ennreal.of_real ε)
def
measure_theory.uniform_integrable
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[normed_add_comm_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
- measure_theory.uniform_integrable f p μ = ((∀ (i : ι), measure_theory.ae_strongly_measurable (f i) μ) ∧ measure_theory.unif_integrable f p μ ∧ ∃ (C : nnreal), ∀ (i : ι), measure_theory.snorm (f i) p μ ≤ ↑C)
@[protected]
theorem
measure_theory.uniform_integrable.ae_strongly_measurable
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : ι → α → β}
{p : ennreal}
(hf : measure_theory.uniform_integrable f p μ)
(i : ι) :
@[protected]
theorem
measure_theory.uniform_integrable.unif_integrable
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : ι → α → β}
{p : ennreal}
(hf : measure_theory.uniform_integrable f p μ) :
@[protected]
theorem
measure_theory.uniform_integrable.mem_ℒp
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : ι → α → β}
{p : ennreal}
(hf : measure_theory.uniform_integrable f p μ)
(i : ι) :
measure_theory.mem_ℒp (f i) p μ
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_add_comm_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) μ) :
measure_theory.unif_integrable (f + g) p μ
@[protected]
theorem
measure_theory.unif_integrable.neg
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : ι → α → β}
{p : ennreal}
(hf : measure_theory.unif_integrable f p μ) :
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_add_comm_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) μ) :
measure_theory.unif_integrable (f - g) p μ
@[protected]
theorem
measure_theory.unif_integrable.ae_eq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_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_add_comm_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_add_comm_group β]
{p : ennreal}
{f g : ι → α → β}
(hfg : ∀ (n : ι), f n =ᵐ[μ] g n) :
theorem
measure_theory.tendsto_indicator_ge
{α : Type u_1}
{β : Type u_2}
[normed_add_comm_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_add_comm_group β]
{f : α → β}
(hf : measure_theory.mem_ℒp f 1 μ)
(hmeas : measure_theory.strongly_measurable f)
{ε : ℝ}
(hε : 0 < ε) :
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_add_comm_group β]
{f : α → β}
(hf : measure_theory.mem_ℒp f 1 μ)
(hmeas : measure_theory.strongly_measurable f)
{ε : ℝ}
(hε : 0 < ε) :
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_add_comm_group β]
{f : α → β}
(hf : measure_theory.mem_ℒp f 1 μ)
{ε : ℝ}
(hε : 0 < ε) :
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_add_comm_group β]
{f : α → β}
(hf : measure_theory.mem_ℒp f ⊤ μ)
(hmeas : measure_theory.strongly_measurable f) :
theorem
measure_theory.mem_ℒp.snorm_indicator_norm_ge_le
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
(μ : measure_theory.measure α)
[normed_add_comm_group β]
{p : ennreal}
{f : α → β}
(hf : measure_theory.mem_ℒp f p μ)
(hmeas : measure_theory.strongly_measurable f)
{ε : ℝ}
(hε : 0 < ε) :
theorem
measure_theory.mem_ℒp.snorm_indicator_norm_ge_pos_le
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
(μ : measure_theory.measure α)
[normed_add_comm_group β]
{p : ennreal}
{f : α → β}
(hf : measure_theory.mem_ℒp f p μ)
(hmeas : measure_theory.strongly_measurable f)
{ε : ℝ}
(hε : 0 < ε) :
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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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 finite type.
theorem
measure_theory.unif_integrable_finite
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
(μ : measure_theory.measure α)
[normed_add_comm_group β]
{p : ennreal}
[finite ι]
(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_add_comm_group β]
{p : ennreal}
(hp' : p ≠ ⊤)
{s : set α}
(hs : measurable_set s)
{f g : α → β}
{c : ℝ}
(hc : 0 ≤ c)
(hf : ∀ (x : α), x ∈ s → has_dist.dist (f x) (g x) ≤ c) :
measure_theory.snorm (s.indicator (f - g)) p μ ≤ ennreal.of_real c * ⇑μ s ^ (1 / p.to_real)
theorem
measure_theory.tendsto_Lp_of_tendsto_ae_of_meas
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
(μ : measure_theory.measure α)
[normed_add_comm_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))) :
filter.tendsto (λ (n : ℕ), measure_theory.snorm (f n - g) p μ) filter.at_top (nhds 0)
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_add_comm_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))) :
filter.tendsto (λ (n : ℕ), measure_theory.snorm (f n - g) p μ) filter.at_top (nhds 0)
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_add_comm_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_add_comm_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_add_comm_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) :
filter.tendsto (λ (n : ℕ), measure_theory.snorm (f n - g) p μ) filter.at_top (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
measure_theory.tendsto_in_measure_iff_tendsto_Lp
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
(μ : measure_theory.measure α)
[normed_add_comm_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 μ) :
measure_theory.tendsto_in_measure μ f filter.at_top g ∧ measure_theory.unif_integrable f p μ ↔ filter.tendsto (λ (n : ℕ), measure_theory.snorm (f n - g) p μ) filter.at_top (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
measure_theory.unif_integrable_of'
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
(μ : measure_theory.measure α)
[normed_add_comm_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_add_comm_group β]
{p : ennreal}
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
{f : ι → α → β}
(hf : ∀ (i : ι), measure_theory.ae_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_add_comm_group β]
{p : ennreal}
{f : ι → α → β}
[measurable_space α] :
theorem
measure_theory.uniform_integrable.ae_eq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{p : ennreal}
{f g : ι → α → β}
(hf : measure_theory.uniform_integrable f p μ)
(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_add_comm_group β]
{p : ennreal}
{f g : ι → α → β}
(hfg : ∀ (n : ι), f n =ᵐ[μ] g n) :
theorem
measure_theory.uniform_integrable_finite
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{p : ennreal}
{f : ι → α → β}
[finite ι]
(hp_one : 1 ≤ p)
(hp_top : p ≠ ⊤)
(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_add_comm_group β]
{p : ennreal}
{f : ι → α → β}
[subsingleton ι]
(hp_one : 1 ≤ p)
(hp_top : p ≠ ⊤)
(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_add_comm_group β]
{p : ennreal}
{g : α → β}
(hp : 1 ≤ p)
(hp_ne_top : p ≠ ⊤)
(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_add_comm_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 ε)) :
This lemma is superceded by uniform_integrable_of which only requires
ae_strongly_measurable.
theorem
measure_theory.uniform_integrable_of
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{p : ennreal}
{f : ι → α → β}
[measure_theory.is_finite_measure μ]
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
(hf : ∀ (i : ι), measure_theory.ae_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_add_comm_group β]
{p : ennreal}
{f : ι → α → β}
(hp : p ≠ 0)
(hp' : p ≠ ⊤)
(hf : ∀ (i : ι), measure_theory.strongly_measurable (f i))
(hfu : measure_theory.uniform_integrable f p μ)
{ε : ℝ}
(hε : 0 < ε) :
This lemma is superceded by uniform_integrable.spec which does not require measurability.
theorem
measure_theory.uniform_integrable.spec
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{p : ennreal}
{f : ι → α → β}
(hp : p ≠ 0)
(hp' : p ≠ ⊤)
(hfu : measure_theory.uniform_integrable f p μ)
{ε : ℝ}
(hε : 0 < ε) :
theorem
measure_theory.uniform_integrable_iff
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{p : ennreal}
{f : ι → α → β}
[measure_theory.is_finite_measure μ]
(hp : 1 ≤ p)
(hp' : p ≠ ⊤) :
measure_theory.uniform_integrable f p μ ↔ (∀ (i : ι), measure_theory.ae_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.
theorem
measure_theory.uniform_integrable_average
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{p : ennreal}
(hp : 1 ≤ p)
{f : ℕ → α → ℝ}
(hf : measure_theory.uniform_integrable f p μ) :
measure_theory.uniform_integrable (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i) / ↑n) p μ
The averaging of a uniformly integrable sequence is also uniformly integrable.