Documentation

Mathlib.MeasureTheory.Function.UnifTight

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 #

Main results #

Tags #

uniform integrable, uniformly tight, Vitali convergence theorem

def MeasureTheory.UnifTight {α : Type u_1} {β : Type u_2} {ι : Type u_3} [NormedAddCommGroup β] :
{x : MeasurableSpace α} → (ιαβ)ENNRealMeasureTheory.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.eLpNorm (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.eLpNorm (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.eLpNorm (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.eLpNorm (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) μ) :
    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 μ) :
    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) μ) :
    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) :
    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) :

    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 μ) :

    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 μ) :

    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.eLpNorm (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.eLpNorm (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.eLpNorm (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.