Convergence Lemmas for Conditional Expectation #
This file provides convergence lemmas for conditional expectations, including dominated convergence theorems and subsequence extraction.
Main results #
tendsto_condExpL1_domconv: DCT for conditional expectation in L¹exists_subseq_ae_tendsto_of_condExpL1_tendsto: From L¹ convergence to a.e. convergence of a subsequence
theorem
tendsto_condExpL1_domconv
{α : Type u_1}
{E : Type u_2}
{m m₀ : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hm : m ≤ m₀)
[MeasureTheory.SigmaFinite (μ.trim hm)]
{fs : ℕ → α → E}
{f : α → E}
(bound : α → ℝ)
(hfs_meas : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fs n) μ)
(h_int : MeasureTheory.Integrable bound μ)
(hbound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound x)
(hpt : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => fs n x) Filter.atTop (nhds (f x)))
:
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.condExpL1 hm μ (fs n)) Filter.atTop (nhds (MeasureTheory.condExpL1 hm μ f))
DCT for conditional expectation in L¹.
theorem
exists_subseq_ae_tendsto_of_condExpL1_tendsto
{α : Type u_1}
{E : Type u_2}
{m m₀ : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hm : m ≤ m₀)
[MeasureTheory.SigmaFinite (μ.trim hm)]
{fs : ℕ → α → E}
{f : α → E}
(hL1 :
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.condExpL1 hm μ (fs n)) Filter.atTop
(nhds (MeasureTheory.condExpL1 hm μ f)))
:
∃ (ns : ℕ → ℕ),
StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => ↑↑(MeasureTheory.condExpL1 hm μ (fs (ns n))) x) Filter.atTop
(nhds (↑↑(MeasureTheory.condExpL1 hm μ f) x))
From L¹ convergence of condExpL1 to a.e. convergence of a subsequence of its representatives.