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 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.MeasureTheory.UniformIntegrable: 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 #
MeasureTheory.unifIntegrable_finite: a finite sequence of Lp functions is uniformly integrable.MeasureTheory.tendsto_Lp_finite_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_finite: 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}
[NormedAddCommGroup β]
:
{x : MeasurableSpace α} → (ι → α → β) → ENNReal → MeasureTheory.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 integrability is also known as uniformly absolutely continuous integrals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MeasureTheory.UniformIntegrable
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[NormedAddCommGroup β]
:
{x : MeasurableSpace α} → (ι → α → β) → ENNReal → MeasureTheory.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
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.UniformIntegrable.aeStronglyMeasurable
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{p : ENNReal}
(hf : MeasureTheory.UniformIntegrable f p μ)
(i : ι)
:
theorem
MeasureTheory.UniformIntegrable.unifIntegrable
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{p : ENNReal}
(hf : MeasureTheory.UniformIntegrable f p μ)
:
theorem
MeasureTheory.UniformIntegrable.memℒp
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{p : ENNReal}
(hf : MeasureTheory.UniformIntegrable f p μ)
(i : ι)
:
MeasureTheory.Memℒp (f i) p μ
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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{g : ι → α → β}
{p : ENNReal}
(hf : MeasureTheory.UnifIntegrable f p μ)
(hg : MeasureTheory.UnifIntegrable g p μ)
(hp : 1 ≤ p)
(hf_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ)
(hg_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (g i) μ)
:
MeasureTheory.UnifIntegrable (f + g) p μ
theorem
MeasureTheory.UnifIntegrable.neg
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{p : ENNReal}
(hf : MeasureTheory.UnifIntegrable f p μ)
:
MeasureTheory.UnifIntegrable (-f) p μ
theorem
MeasureTheory.UnifIntegrable.sub
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{g : ι → α → β}
{p : ENNReal}
(hf : MeasureTheory.UnifIntegrable f p μ)
(hg : MeasureTheory.UnifIntegrable g p μ)
(hp : 1 ≤ p)
(hf_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ)
(hg_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (g i) μ)
:
MeasureTheory.UnifIntegrable (f - g) p μ
theorem
MeasureTheory.UnifIntegrable.ae_eq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{g : ι → α → β}
{p : ENNReal}
(hf : MeasureTheory.UnifIntegrable f p μ)
(hfg : ∀ (n : ι), f n =ᵐ[μ] g n)
:
theorem
MeasureTheory.UnifIntegrable.indicator
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{p : ENNReal}
(hf : MeasureTheory.UnifIntegrable f p μ)
(E : Set α)
:
MeasureTheory.UnifIntegrable (fun (i : ι) => E.indicator (f i)) p μ
Uniform integrability is preserved by restriction of the functions to a set.
theorem
MeasureTheory.UnifIntegrable.restrict
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{p : ENNReal}
(hf : MeasureTheory.UnifIntegrable f p μ)
(E : Set α)
:
MeasureTheory.UnifIntegrable f p (μ.restrict E)
Uniform integrability is preserved by restriction of the measure to a set.
theorem
MeasureTheory.unifIntegrable_zero_meas
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[NormedAddCommGroup β]
[MeasurableSpace α]
{p : ENNReal}
{f : ι → α → β}
:
theorem
MeasureTheory.unifIntegrable_congr_ae
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : ι → α → β}
{g : ι → α → β}
(hfg : ∀ (n : ι), f n =ᵐ[μ] g n)
:
theorem
MeasureTheory.tendsto_indicator_ge
{α : Type u_1}
{β : Type u_2}
[NormedAddCommGroup β]
(f : α → β)
(x : α)
:
theorem
MeasureTheory.Memℒp.integral_indicator_norm_ge_le
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.Memℒp f 1 μ)
(hmeas : MeasureTheory.StronglyMeasurable f)
{ε : ℝ}
(hε : 0 < ε)
:
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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.Memℒp f 1 μ)
(hmeas : MeasureTheory.StronglyMeasurable f)
{ε : ℝ}
(hε : 0 < ε)
:
This lemma is superseded 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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.Memℒp f 1 μ)
{ε : ℝ}
(hε : 0 < ε)
:
theorem
MeasureTheory.Memℒp.eLpNormEssSup_indicator_norm_ge_eq_zero
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.Memℒp f ⊤ μ)
(hmeas : MeasureTheory.StronglyMeasurable f)
:
@[deprecated MeasureTheory.Memℒp.eLpNormEssSup_indicator_norm_ge_eq_zero]
theorem
MeasureTheory.Memℒp.snormEssSup_indicator_norm_ge_eq_zero
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.Memℒp f ⊤ μ)
(hmeas : MeasureTheory.StronglyMeasurable f)
:
Alias of MeasureTheory.Memℒp.eLpNormEssSup_indicator_norm_ge_eq_zero.
theorem
MeasureTheory.Memℒp.eLpNorm_indicator_norm_ge_le
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : α → β}
(hf : MeasureTheory.Memℒp f p μ)
(hmeas : MeasureTheory.StronglyMeasurable f)
{ε : ℝ}
(hε : 0 < ε)
:
∃ (M : ℝ), MeasureTheory.eLpNorm ({x : α | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
@[deprecated MeasureTheory.Memℒp.eLpNorm_indicator_norm_ge_le]
theorem
MeasureTheory.Memℒp.snorm_indicator_norm_ge_le
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : α → β}
(hf : MeasureTheory.Memℒp f p μ)
(hmeas : MeasureTheory.StronglyMeasurable f)
{ε : ℝ}
(hε : 0 < ε)
:
∃ (M : ℝ), MeasureTheory.eLpNorm ({x : α | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
theorem
MeasureTheory.Memℒp.eLpNorm_indicator_norm_ge_pos_le
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : α → β}
(hf : MeasureTheory.Memℒp f p μ)
(hmeas : MeasureTheory.StronglyMeasurable f)
{ε : ℝ}
(hε : 0 < ε)
:
∃ (M : ℝ), 0 < M ∧ MeasureTheory.eLpNorm ({x : α | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
This lemma implies that a single function is uniformly integrable (in the probability sense).
@[deprecated MeasureTheory.Memℒp.eLpNorm_indicator_norm_ge_pos_le]
theorem
MeasureTheory.Memℒp.snorm_indicator_norm_ge_pos_le
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : α → β}
(hf : MeasureTheory.Memℒp f p μ)
(hmeas : MeasureTheory.StronglyMeasurable f)
{ε : ℝ}
(hε : 0 < ε)
:
∃ (M : ℝ), 0 < M ∧ MeasureTheory.eLpNorm ({x : α | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
Alias of MeasureTheory.Memℒp.eLpNorm_indicator_norm_ge_pos_le.
This lemma implies that a single function is uniformly integrable (in the probability sense).
theorem
MeasureTheory.eLpNorm_indicator_le_of_bound
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : α → β}
(hp_top : p ≠ ⊤)
{ε : ℝ}
(hε : 0 < ε)
{M : ℝ}
(hf : ∀ (x : α), ‖f x‖ < M)
:
∃ (δ : ℝ) (_ : 0 < δ),
∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
@[deprecated MeasureTheory.eLpNorm_indicator_le_of_bound]
theorem
MeasureTheory.snorm_indicator_le_of_bound
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : α → β}
(hp_top : p ≠ ⊤)
{ε : ℝ}
(hε : 0 < ε)
{M : ℝ}
(hf : ∀ (x : α), ‖f x‖ < M)
:
∃ (δ : ℝ) (_ : 0 < δ),
∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
theorem
MeasureTheory.Memℒp.eLpNorm_indicator_le'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : α → β}
(hp_one : 1 ≤ p)
(hp_top : p ≠ ⊤)
(hf : MeasureTheory.Memℒp f p μ)
(hmeas : MeasureTheory.StronglyMeasurable f)
{ε : ℝ}
(hε : 0 < ε)
:
∃ (δ : ℝ) (_ : 0 < δ),
∀ (s : Set α),
MeasurableSet s → μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
Auxiliary lemma for MeasureTheory.Memℒp.eLpNorm_indicator_le.
@[deprecated MeasureTheory.Memℒp.eLpNorm_indicator_le']
theorem
MeasureTheory.Memℒp.snorm_indicator_le'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : α → β}
(hp_one : 1 ≤ p)
(hp_top : p ≠ ⊤)
(hf : MeasureTheory.Memℒp f p μ)
(hmeas : MeasureTheory.StronglyMeasurable f)
{ε : ℝ}
(hε : 0 < ε)
:
∃ (δ : ℝ) (_ : 0 < δ),
∀ (s : Set α),
MeasurableSet s → μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
Alias of MeasureTheory.Memℒp.eLpNorm_indicator_le'.
Auxiliary lemma for MeasureTheory.Memℒp.eLpNorm_indicator_le.
theorem
MeasureTheory.Memℒp.eLpNorm_indicator_le_of_meas
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : α → β}
(hp_one : 1 ≤ p)
(hp_top : p ≠ ⊤)
(hf : MeasureTheory.Memℒp f p μ)
(hmeas : MeasureTheory.StronglyMeasurable f)
{ε : ℝ}
(hε : 0 < ε)
:
∃ (δ : ℝ) (_ : 0 < δ),
∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
This lemma is superseded by MeasureTheory.Memℒp.eLpNorm_indicator_le which does not require
measurability on f.
@[deprecated MeasureTheory.Memℒp.eLpNorm_indicator_le_of_meas]
theorem
MeasureTheory.Memℒp.snorm_indicator_le_of_meas
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : α → β}
(hp_one : 1 ≤ p)
(hp_top : p ≠ ⊤)
(hf : MeasureTheory.Memℒp f p μ)
(hmeas : MeasureTheory.StronglyMeasurable f)
{ε : ℝ}
(hε : 0 < ε)
:
∃ (δ : ℝ) (_ : 0 < δ),
∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Alias of MeasureTheory.Memℒp.eLpNorm_indicator_le_of_meas.
This lemma is superseded by MeasureTheory.Memℒp.eLpNorm_indicator_le which does not require
measurability on f.
theorem
MeasureTheory.Memℒp.eLpNorm_indicator_le
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : α → β}
(hp_one : 1 ≤ p)
(hp_top : p ≠ ⊤)
(hf : MeasureTheory.Memℒp f p μ)
{ε : ℝ}
(hε : 0 < ε)
:
∃ (δ : ℝ) (_ : 0 < δ),
∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
@[deprecated MeasureTheory.Memℒp.eLpNorm_indicator_le]
theorem
MeasureTheory.Memℒp.snorm_indicator_le
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : α → β}
(hp_one : 1 ≤ p)
(hp_top : p ≠ ⊤)
(hf : MeasureTheory.Memℒp f p μ)
{ε : ℝ}
(hε : 0 < ε)
:
∃ (δ : ℝ) (_ : 0 < δ),
∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Alias of MeasureTheory.Memℒp.eLpNorm_indicator_le.
theorem
MeasureTheory.unifIntegrable_const
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{g : α → β}
(hp : 1 ≤ p)
(hp_ne_top : p ≠ ⊤)
(hg : MeasureTheory.Memℒp g p μ)
:
MeasureTheory.UnifIntegrable (fun (x : ι) => g) p μ
A constant function is uniformly integrable.
theorem
MeasureTheory.unifIntegrable_subsingleton
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
[Subsingleton ι]
(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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
[Finite ι]
(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.eLpNorm_sub_le_of_dist_bdd
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup β]
(μ : MeasureTheory.Measure α)
{p : ENNReal}
(hp' : p ≠ ⊤)
{s : Set α}
(hs : MeasurableSet s)
{f : α → β}
{g : α → β}
{c : ℝ}
(hc : 0 ≤ c)
(hf : ∀ x ∈ s, dist (f x) (g x) ≤ c)
:
MeasureTheory.eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)
@[deprecated MeasureTheory.eLpNorm_sub_le_of_dist_bdd]
theorem
MeasureTheory.snorm_sub_le_of_dist_bdd
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup β]
(μ : MeasureTheory.Measure α)
{p : ENNReal}
(hp' : p ≠ ⊤)
{s : Set α}
(hs : MeasurableSet s)
{f : α → β}
{g : α → β}
{c : ℝ}
(hc : 0 ≤ c)
(hf : ∀ x ∈ s, dist (f x) (g x) ≤ c)
:
MeasureTheory.eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)
Alias of MeasureTheory.eLpNorm_sub_le_of_dist_bdd.
theorem
MeasureTheory.tendsto_Lp_finite_of_tendsto_ae_of_meas
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
[MeasureTheory.IsFiniteMeasure μ]
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
{f : ℕ → α → β}
{g : α → β}
(hf : ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (f n))
(hg : MeasureTheory.StronglyMeasurable g)
(hg' : MeasureTheory.Memℒp g p μ)
(hui : MeasureTheory.UnifIntegrable f p μ)
(hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x)))
:
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (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_finite_of_tendsto_ae
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
[MeasureTheory.IsFiniteMeasure μ]
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
{f : ℕ → α → β}
{g : α → β}
(hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ)
(hg : MeasureTheory.Memℒp g p μ)
(hui : MeasureTheory.UnifIntegrable f p μ)
(hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x)))
:
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : ℕ → α → β}
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
(hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ)
(hf_tendsto : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n) p μ) Filter.atTop (nhds 0))
:
theorem
MeasureTheory.unifIntegrable_of_tendsto_Lp
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : ℕ → α → β}
{g : α → β}
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
(hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ)
(hg : MeasureTheory.Memℒp g p μ)
(hfg : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0))
:
Convergence in Lp implies uniform integrability.
theorem
MeasureTheory.tendsto_Lp_finite_of_tendstoInMeasure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : ℕ → α → β}
{g : α → β}
[MeasureTheory.IsFiniteMeasure μ]
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
(hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ)
(hg : MeasureTheory.Memℒp g p μ)
(hui : MeasureTheory.UnifIntegrable f p μ)
(hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g)
:
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (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_finite
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : ℕ → α → β}
{g : α → β}
[MeasureTheory.IsFiniteMeasure μ]
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
(hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ)
(hg : MeasureTheory.Memℒp g p μ)
:
MeasureTheory.TendstoInMeasure μ f Filter.atTop g ∧ MeasureTheory.UnifIntegrable f p μ ↔ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
{f : ι → α → β}
(hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i))
(h : ∀ (ε : ℝ),
0 < ε →
∃ (C : NNReal),
0 < C ∧ ∀ (i : ι), MeasureTheory.eLpNorm ({x : α | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε)
:
This lemma is superseded 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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
{f : ι → α → β}
(hf : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ)
(h : ∀ (ε : ℝ),
0 < ε →
∃ (C : NNReal), ∀ (i : ι), MeasureTheory.eLpNorm ({x : α | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε)
:
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}
[NormedAddCommGroup β]
{p : ENNReal}
{f : ι → α → β}
[MeasurableSpace α]
:
theorem
MeasureTheory.UniformIntegrable.ae_eq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : ι → α → β}
{g : ι → α → β}
(hf : MeasureTheory.UniformIntegrable f p μ)
(hfg : ∀ (n : ι), f n =ᵐ[μ] g n)
:
theorem
MeasureTheory.uniformIntegrable_congr_ae
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : ι → α → β}
{g : ι → α → β}
(hfg : ∀ (n : ι), f n =ᵐ[μ] g n)
:
theorem
MeasureTheory.uniformIntegrable_finite
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : ι → α → β}
[Finite ι]
(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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : ι → α → β}
[Subsingleton ι]
(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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{g : α → β}
(hp : 1 ≤ p)
(hp_ne_top : p ≠ ⊤)
(hg : MeasureTheory.Memℒp g p μ)
:
MeasureTheory.UniformIntegrable (fun (x : ι) => g) p μ
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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : ι → α → β}
[MeasureTheory.IsFiniteMeasure μ]
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
(hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i))
(h : ∀ (ε : ℝ),
0 < ε →
∃ (C : NNReal), ∀ (i : ι), MeasureTheory.eLpNorm ({x : α | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε)
:
This lemma is superseded by uniformIntegrable_of which only requires
AEStronglyMeasurable.
theorem
MeasureTheory.uniformIntegrable_of
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : ι → α → β}
[MeasureTheory.IsFiniteMeasure μ]
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
(hf : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ)
(h : ∀ (ε : ℝ),
0 < ε →
∃ (C : NNReal), ∀ (i : ι), MeasureTheory.eLpNorm ({x : α | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε)
:
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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : ι → α → β}
(hp : p ≠ 0)
(hp' : p ≠ ⊤)
(hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i))
(hfu : MeasureTheory.UniformIntegrable f p μ)
{ε : ℝ}
(hε : 0 < ε)
:
∃ (C : NNReal), ∀ (i : ι), MeasureTheory.eLpNorm ({x : α | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
This lemma is superseded by UniformIntegrable.spec which does not require measurability.
theorem
MeasureTheory.UniformIntegrable.spec
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : ι → α → β}
(hp : p ≠ 0)
(hp' : p ≠ ⊤)
(hfu : MeasureTheory.UniformIntegrable f p μ)
{ε : ℝ}
(hε : 0 < ε)
:
∃ (C : NNReal), ∀ (i : ι), MeasureTheory.eLpNorm ({x : α | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
theorem
MeasureTheory.uniformIntegrable_iff
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{f : ι → α → β}
[MeasureTheory.IsFiniteMeasure μ]
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
:
MeasureTheory.UniformIntegrable f p μ ↔ (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) ∧ ∀ (ε : ℝ),
0 < ε →
∃ (C : NNReal), ∀ (i : ι), MeasureTheory.eLpNorm ({x : α | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
The definition of uniform integrable in mathlib is equivalent to the definition commonly found in literature.
theorem
MeasureTheory.uniformIntegrable_average
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(hp : 1 ≤ p)
{f : ℕ → α → E}
(hf : MeasureTheory.UniformIntegrable f p μ)
:
MeasureTheory.UniformIntegrable (fun (n : ℕ) => (↑n)⁻¹ • ∑ i ∈ Finset.range n, f i) p μ
The averaging of a uniformly integrable sequence is also uniformly integrable.
theorem
MeasureTheory.uniformIntegrable_average_real
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ENNReal}
(hp : 1 ≤ p)
{f : ℕ → α → ℝ}
(hf : MeasureTheory.UniformIntegrable f p μ)
:
MeasureTheory.UniformIntegrable (fun (n : ℕ) => (∑ i ∈ Finset.range n, f i) / ↑n) p μ
The averaging of a uniformly integrable real-valued sequence is also uniformly integrable.