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 #

Main results #

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 α} → (ιαβ)ENNRealMeasureTheory.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 α} → (ιαβ)ENNRealMeasureTheory.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 : ι) :

      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) μ) :
      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 μ) :
      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) μ) :
      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 : α) :
      Filter.Tendsto (fun (M : ) => {x : α | M f x‖₊}.indicator f x) Filter.atTop (nhds 0)
      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 < ε) :
      ∃ (M : ), ∫⁻ (x : α), {x : α | M f x‖₊}.indicator f x‖₊μ ENNReal.ofReal ε

      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 < ε) :
      ∃ (M : ), 0 M ∫⁻ (x : α), {x : α | M f x‖₊}.indicator f x‖₊μ ENNReal.ofReal ε

      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 < ε) :
      ∃ (M : ), 0 M ∫⁻ (x : α), {x : α | M f x‖₊}.indicator f x‖₊μ ENNReal.ofReal ε
      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) :
      ∃ (M : ), MeasureTheory.eLpNormEssSup ({x : α | M f x‖₊}.indicator f) μ = 0
      @[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) :
      ∃ (M : ), MeasureTheory.eLpNormEssSup ({x : α | M f x‖₊}.indicator f) μ = 0

      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 ε

      Alias of MeasureTheory.Memℒp.eLpNorm_indicator_norm_ge_le.

      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 ε

      Alias of MeasureTheory.eLpNorm_indicator_le_of_bound.

      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 : xs, 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 : xs, 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 ε) :

      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} [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)⁻¹ iFinset.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 : ) => (∑ iFinset.range n, f i) / n) p μ

      The averaging of a uniformly integrable real-valued sequence is also uniformly integrable.