Documentation

Atlas.TheoryOfProbability.code.UIConvergenceEquiv

theorem TheoryOfProbability3.ennreal_tendsto_zero_of_squeeze {a b : ENNReal} {c : ENNReal} (hba : ∀ (n : ), b n a n) (ha : Filter.Tendsto a Filter.atTop (nhds c)) (hc_ne_top : c ) (h : c Filter.liminf (fun (n : ) => a n - b n) Filter.atTop) :

Squeeze-style lemma in ℝ≥0∞: if b n ≤ a n, a n → c < ∞, and the liminf of a n - b n is at least c, then b n → 0.

theorem TheoryOfProbability3.scheffe_hn_tendsto_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {g : α} (hae : ∀ᵐ (x : α) μ, Filter.Tendsto (fun (n : ) => f n x) Filter.atTop (nhds (g x))) :
∀ᵐ (x : α) μ, Filter.Tendsto (fun (n : ) => f n x‖ₑ + g x‖ₑ - f n x - g x‖ₑ) Filter.atTop (nhds (g x‖ₑ + g x‖ₑ))

Pointwise (a.e.) convergence step in Scheffé's lemma: if f n → g a.e., then the auxiliary quantity ‖f n‖ₑ + ‖g‖ₑ - ‖f n - g‖ₑ converges a.e. to 2‖g‖ₑ.

theorem TheoryOfProbability3.scheffe_lintegral_eq {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {g : α} (hfm : ∀ (n : ), MeasureTheory.AEStronglyMeasurable (f n) μ) (hgm : MeasureTheory.AEStronglyMeasurable g μ) (hg : MeasureTheory.MemLp g 1 μ) {n : } (hfn : MeasureTheory.eLpNorm (f n) 1 μ < ) :
∫⁻ (x : α), f n x‖ₑ + g x‖ₑ - f n x - g x‖ₑ μ = MeasureTheory.eLpNorm (f n) 1 μ + MeasureTheory.eLpNorm g 1 μ - MeasureTheory.eLpNorm (f n - g) 1 μ

Integration identity used in the proof of Scheffé's lemma: the lintegral of the auxiliary quantity equals (eLpNorm (f n) 1 μ + eLpNorm g 1 μ) - eLpNorm (f n - g) 1 μ.

theorem TheoryOfProbability3.scheffe_lemma {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {g : α} (hfm : ∀ (n : ), MeasureTheory.AEStronglyMeasurable (f n) μ) (hgm : MeasureTheory.AEStronglyMeasurable g μ) (hg : MeasureTheory.MemLp g 1 μ) (hae : ∀ᵐ (x : α) μ, Filter.Tendsto (fun (n : ) => f n x) Filter.atTop (nhds (g x))) (hnorm : Filter.Tendsto (fun (n : ) => MeasureTheory.eLpNorm (f n) 1 μ) Filter.atTop (nhds (MeasureTheory.eLpNorm g 1 μ))) :
Filter.Tendsto (fun (n : ) => MeasureTheory.eLpNorm (f n - g) 1 μ) Filter.atTop (nhds 0)

Scheffé's lemma. If f n → g almost everywhere and ‖f n‖₁ → ‖g‖₁, then f n → g in , i.e. eLpNorm (f n - g) 1 μ → 0.

theorem TheoryOfProbability3.tendsto_eLpNorm_of_tendsto_eLpNorm_sub {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {g : α} (hfm : ∀ (n : ), MeasureTheory.AEStronglyMeasurable (f n) μ) (hgm : MeasureTheory.AEStronglyMeasurable g μ) (hg_ne_top : MeasureTheory.eLpNorm g 1 μ ) (h : Filter.Tendsto (fun (n : ) => MeasureTheory.eLpNorm (f n - g) 1 μ) Filter.atTop (nhds 0)) :

If f n → g in (i.e. eLpNorm (f n - g) 1 μ → 0), then the -norms converge: ‖f n‖₁ → ‖g‖₁.

theorem TheoryOfProbability3.eLpNorm_uniformly_bounded_of_tendsto_eLpNorm_sub {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {g : α} (hf : ∀ (n : ), MeasureTheory.MemLp (f n) 1 μ) (hg : MeasureTheory.MemLp g 1 μ) (hL1 : Filter.Tendsto (fun (n : ) => MeasureTheory.eLpNorm (f n - g) 1 μ) Filter.atTop (nhds 0)) :
∃ (C : NNReal), ∀ (i : ), MeasureTheory.eLpNorm (f i) 1 μ C

If f n → g in and g, f n are all in , then the eLpNorms of f n are uniformly bounded by some C : ℝ≥0.

theorem TheoryOfProbability3.uniformIntegrable_of_tendsto_eLpNorm_sub {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {g : α} (hf : ∀ (n : ), MeasureTheory.MemLp (f n) 1 μ) (hg : MeasureTheory.MemLp g 1 μ) (hL1 : Filter.Tendsto (fun (n : ) => MeasureTheory.eLpNorm (f n - g) 1 μ) Filter.atTop (nhds 0)) :

convergence implies uniform integrability: if f n → g in (with f n, g in ), then the family f n is uniformly integrable in .

theorem TheoryOfProbability3.L1_convergence_imp_norm_convergence {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {g : α} (hfm : ∀ (n : ), MeasureTheory.AEStronglyMeasurable (f n) μ) (hgm : MeasureTheory.AEStronglyMeasurable g μ) (hg : MeasureTheory.MemLp g 1 μ) (hL1 : Filter.Tendsto (fun (n : ) => MeasureTheory.eLpNorm (f n - g) 1 μ) Filter.atTop (nhds 0)) :

convergence f n → g implies convergence of the norms ‖f n‖₁ → ‖g‖₁. This is the (2) ⇒ (3) implication of the uniform integrability equivalence theorem.

theorem TheoryOfProbability3.norm_convergence_imp_ui {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {g : α} (hf : ∀ (n : ), MeasureTheory.MemLp (f n) 1 μ) (hg : MeasureTheory.MemLp g 1 μ) (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) (hnorm : Filter.Tendsto (fun (n : ) => MeasureTheory.eLpNorm (f n) 1 μ) Filter.atTop (nhds (MeasureTheory.eLpNorm g 1 μ))) :

If f n → g in measure and ‖f n‖₁ → ‖g‖₁, then the family f n is uniformly integrable in . This is the (3) ⇒ (1) implication of the uniform integrability equivalence theorem, proven via Scheffé's lemma and a subsequence argument.

If f n is uniformly integrable in and f n → g in measure (with g ∈ L¹), then f n → g in . This is the (1) ⇒ (2) implication of the uniform integrability equivalence theorem.

Uniform integrability equivalences. Suppose f n → g in measure on a finite measure space, with f n, g ∈ L¹. Then the following are equivalent:

  1. The family f n is uniformly integrable in .
  2. f n → g in (i.e. eLpNorm (f n - g) 1 μ → 0).
  3. ‖f n‖₁ → ‖g‖₁.

Renamed alias for ui_L1_norm_tfae: the textbook statement that uniform integrability, convergence, and convergence of norms are equivalent (assuming convergence in measure to g).

Top-level (out-of-namespace) restatement of the uniform integrability equivalences: if f n → g in measure on a finite measure space with f n, g ∈ L¹, then uniform integrability of f n, convergence f n → g in , and convergence ‖f n‖₁ → ‖g‖₁ are equivalent.

Out-of-namespace alias for TheoryOfProbability3.ui_L1_norm_tfae, stating the same uniform integrability ↔ convergence ↔ convergence of norms equivalence.