Passing conditional expectations through convergence in mean #
The contraction inequality gives a direct scalar proof without choosing almost-sure versions of the approximating conditional expectations simultaneously in a real parameter.
References #
- J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.
theorem
BGW.StableTrees.condExp_eq_of_integral_abs_tendsto
{Ω : Type u_1}
[m₀ : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
(m : MeasurableSpace Ω)
{F H : Ω → ℝ}
{Fs Gs : ℕ → Ω → ℝ}
(hF : MeasureTheory.Integrable F μ)
(hH : MeasureTheory.Integrable H μ)
(hFs : ∀ (n : ℕ), MeasureTheory.Integrable (Fs n) μ)
(hGs : ∀ (n : ℕ), MeasureTheory.Integrable (Gs n) μ)
(hcond : ∀ (n : ℕ), μ[Fs n | m] =ᵐ[μ] Gs n)
(hlF : Filter.Tendsto (fun (n : ℕ) => ∫ (f : Ω), |Fs n f - F f| ∂μ) Filter.atTop (nhds 0))
(hlG : Filter.Tendsto (fun (n : ℕ) => ∫ (f : Ω), |Gs n f - H f| ∂μ) Filter.atTop (nhds 0))
:
Conditional expectation passes through two convergences in mean of integrable sequences.