VarianceLimit.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Passing the Gaussian variance bound from finite leaf cutoffs to their limit.

theorem OAI.InvariantIsing.variance_le_of_ae_tendsto_of_mean_tendsto line 16

Source documentation

Fatou's lemma for centered squares. This permits finite-leaf Gaussian variance estimates to pass to the countable cascade prior.

theorem variance_le_of_ae_tendsto_of_mean_tendsto {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} [IsProbabilityMeasure μ] {f : ℕ → Ω → ℝ} {g : Ω → ℝ} {C : ℝ}
    (hf : ∀ n, MemLp (f n) 2 μ) (hg : MemLp g 2 μ)
    (ht : ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)))
    (hm : Tendsto (fun n => ∫ ω, f n ω ∂μ) atTop (𝓝 (∫ ω, g ω ∂μ)))
    (hv : ∀ n, variance (f n) μ ≤ C) : variance g μ ≤ C := by
…