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 L¹, 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 L¹ (i.e. eLpNorm (f n - g) 1 μ → 0), then the L¹-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 L¹ and g, f n are all in L¹, 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)) :

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

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

L¹ convergence f n → g implies convergence of the L¹ 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 L¹. 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 L¹ and f n → g in measure (with g ∈ L¹), then f n → g in L¹. 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 L¹.
  2. f n → g in L¹ (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, L¹ convergence, and convergence of L¹ 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 L¹, and convergence ‖f n‖₁ → ‖g‖₁ are equivalent.

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