theorem
tendsto_integral_norm_zero_of_tendsto_eLpNorm
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{f : ℕ → Ω → ℝ}
{g : Ω → ℝ}
(hint : ∀ (n : ℕ), MeasureTheory.Integrable (f n - g) μ)
(h : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) 1 μ) Filter.atTop (nhds 0))
:
Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), ‖f n ω - g ω‖ ∂μ) Filter.atTop (nhds 0)
Translates L¹ convergence in the eLpNorm formulation to convergence of the real-valued
L¹ integrals ∫ ‖f n - g‖ dμ → 0.
theorem
tendsto_eLpNorm_of_tendsto_integral_norm_zero
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{f : ℕ → Ω → ℝ}
{g : Ω → ℝ}
(hint : ∀ (n : ℕ), MeasureTheory.Integrable (f n - g) μ)
(h : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), ‖f n ω - g ω‖ ∂μ) Filter.atTop (nhds 0))
:
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) 1 μ) Filter.atTop (nhds 0)
Converse of tendsto_integral_norm_zero_of_tendsto_eLpNorm: convergence of
∫ ‖f n - g‖ dμ → 0 upgrades to eLpNorm (f n - g) 1 μ → 0.
theorem
eLpNorm_bound_of_L1_tendsto
{Ω : Type u_1}
{m0 : 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¹ (in eLpNorm form) and g is integrable, then the family
f n is uniformly L¹-bounded by some constant C : ℝ≥0.
theorem
submartingale_ui_convergence_equiv
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{ℱ : MeasureTheory.Filtration ℕ m0}
{X : ℕ → Ω → ℝ}
(hsub : MeasureTheory.Submartingale X ℱ μ)
:
[MeasureTheory.UniformIntegrable X 1 μ, ∃ (X_inf : Ω → ℝ),
MeasureTheory.Integrable X_inf μ ∧ (∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => X n ω) Filter.atTop (nhds (X_inf ω))) ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), ‖X n ω - X_inf ω‖ ∂μ) Filter.atTop (nhds 0), ∃ (X_inf : Ω → ℝ),
MeasureTheory.Integrable X_inf μ ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), ‖X n ω - X_inf ω‖ ∂μ) Filter.atTop (nhds 0)].TFAE
Submartingale convergence theorem. For a submartingale X on a probability space, the
following are equivalent:
Xis uniformly integrable.- There exists an integrable
X_∞such thatX_n → X_∞almost surely and inL¹(in the∫ ‖X n - X_∞‖sense). - There exists an integrable
X_∞such thatX_n → X_∞inL¹.