Uniform tightness #
This file contains the definitions for uniform tightness for a family of Lp functions. It is used as a hypothesis to the version of Vitali's convergence theorem for Lp spaces that works also for spaces of infinite measure. This version of Vitali's theorem is also proved later in the file.
Main definitions #
MeasureTheory.UnifTight: A sequence of functionsfis uniformly tight inL^pif for allε > 0, there exists some measurable setswith finite measure such that the Lp-norm off irestricted tosᶜis smaller thanεfor alli.
Main results #
MeasureTheory.unifTight_finite: a finite sequence of Lp functions is uniformly tight.MeasureTheory.tendsto_Lp_of_tendsto_ae: a sequence of Lp functions which is uniformly integrable and uniformly tight converges in Lp if it converges 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, uniformly tight and converges in measure.
Tags #
uniform integrable, uniformly tight, Vitali convergence theorem
def
MeasureTheory.UnifTight
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[NormedAddCommGroup β]
:
{x : MeasurableSpace α} → (ι → α → β) → ENNReal → MeasureTheory.Measure α → Prop
A sequence of functions f is uniformly tight in L^p if for all ε > 0, there
exists some measurable set s with finite measure such that the Lp-norm of
f i restricted to sᶜ is smaller than ε for all i.
Equations
Instances For
theorem
MeasureTheory.unifTight_iff_ennreal
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[NormedAddCommGroup β]
:
∀ {x : MeasurableSpace α} (f : ι → α → β) (p : ENNReal) (μ : MeasureTheory.Measure α),
MeasureTheory.UnifTight f p μ ↔ ∀ ⦃ε : ENNReal⦄, 0 < ε → ∃ (s : Set α), μ s ≠ ⊤ ∧ ∀ (i : ι), MeasureTheory.snorm (sᶜ.indicator (f i)) p μ ≤ ε
theorem
MeasureTheory.unifTight_iff_real
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[NormedAddCommGroup β]
:
∀ {x : MeasurableSpace α} (f : ι → α → β) (p : ENNReal) (μ : MeasureTheory.Measure α),
MeasureTheory.UnifTight f p μ ↔ ∀ ⦃ε : ℝ⦄,
0 < ε → ∃ (s : Set α), μ s ≠ ⊤ ∧ ∀ (i : ι), MeasureTheory.snorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ε
theorem
MeasureTheory.UnifTight.eventually_cofinite_indicator
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{p : ENNReal}
(hf : MeasureTheory.UnifTight f p μ)
{ε : ENNReal}
(hε : ε ≠ 0)
:
∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), MeasureTheory.snorm (s.indicator (f i)) p μ ≤ ε
theorem
MeasureTheory.UnifTight.exists_measurableSet_indicator
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{p : ENNReal}
(hf : MeasureTheory.UnifTight f p μ)
{ε : ENNReal}
(hε : ε ≠ 0)
:
∃ (s : Set α), MeasurableSet s ∧ μ s < ⊤ ∧ ∀ (i : ι), MeasureTheory.snorm (sᶜ.indicator (f i)) p μ ≤ ε
theorem
MeasureTheory.UnifTight.add
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{g : ι → α → β}
{p : ENNReal}
(hf : MeasureTheory.UnifTight f p μ)
(hg : MeasureTheory.UnifTight g p μ)
(hf_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ)
(hg_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (g i) μ)
:
MeasureTheory.UnifTight (f + g) p μ
theorem
MeasureTheory.UnifTight.neg
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{p : ENNReal}
(hf : MeasureTheory.UnifTight f p μ)
:
MeasureTheory.UnifTight (-f) p μ
theorem
MeasureTheory.UnifTight.sub
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{g : ι → α → β}
{p : ENNReal}
(hf : MeasureTheory.UnifTight f p μ)
(hg : MeasureTheory.UnifTight g p μ)
(hf_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ)
(hg_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (g i) μ)
:
MeasureTheory.UnifTight (f - g) p μ
theorem
MeasureTheory.UnifTight.aeeq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{g : ι → α → β}
{p : ENNReal}
(hf : MeasureTheory.UnifTight f p μ)
(hfg : ∀ (n : ι), f n =ᵐ[μ] g n)
:
MeasureTheory.UnifTight g p μ
theorem
MeasureTheory.unifTight_congr_ae
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : ι → α → β}
{p : ENNReal}
{g : ι → α → β}
(hfg : ∀ (n : ι), f n =ᵐ[μ] g n)
:
MeasureTheory.UnifTight f p μ ↔ MeasureTheory.UnifTight g p μ
If two functions agree a.e., then one is tight iff the other is tight.
theorem
MeasureTheory.unifTight_const
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
{g : α → β}
(hp_ne_top : p ≠ ⊤)
(hg : MeasureTheory.Memℒp g p μ)
:
MeasureTheory.UnifTight (fun (x : ι) => g) p μ
A constant sequence is tight.
theorem
MeasureTheory.unifTight_of_subsingleton
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
[Subsingleton ι]
(hp_top : p ≠ ⊤)
{f : ι → α → β}
(hf : ∀ (i : ι), MeasureTheory.Memℒp (f i) p μ)
:
MeasureTheory.UnifTight f p μ
A single function is tight.
theorem
MeasureTheory.unifTight_finite
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{p : ENNReal}
[Finite ι]
(hp_top : p ≠ ⊤)
{f : ι → α → β}
(hf : ∀ (i : ι), MeasureTheory.Memℒp (f i) p μ)
:
MeasureTheory.UnifTight f p μ
A finite sequence of Lp functions is uniformly tight.
Both directions and an iff version of Vitali's convergence theorem on measure spaces
of not necessarily finite volume. See Thm III.6.15 of Dunford & Schwartz, Part I (1958).
theorem
MeasureTheory.tendsto_Lp_of_tendsto_ae
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup β]
{μ : MeasureTheory.Measure α}
{p : ENNReal}
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
{f : ℕ → α → β}
{g : α → β}
(haef : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ)
(hg' : MeasureTheory.Memℒp g p μ)
(hui : MeasureTheory.UnifIntegrable f p μ)
(hut : MeasureTheory.UnifTight f p μ)
(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)
Forward direction of Vitali's convergnece theorem, with a.e. instead of InMeasure convergence.
theorem
MeasureTheory.tendsto_Lp_of_tendstoInMeasure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup β]
{μ : MeasureTheory.Measure α}
{p : ENNReal}
{f : ℕ → α → β}
{g : α → β}
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
(hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ)
(hg : MeasureTheory.Memℒp g p μ)
(hui : MeasureTheory.UnifIntegrable f p μ)
(hut : MeasureTheory.UnifTight f p μ)
(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, uniformly tight 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 : MeasurableSpace α}
[NormedAddCommGroup β]
{μ : MeasureTheory.Measure α}
{p : ENNReal}
{f : ℕ → α → β}
{g : α → β}
(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 μ ∧ MeasureTheory.UnifTight f p μ ↔ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.snorm (f n - g) p μ) Filter.atTop (nhds 0)
Vitali's convergence theorem (non-finite measure version).
A sequence of functions f converges to g in Lp
if and only if it is uniformly integrable, uniformly tight and converges to g in measure.