CountableGaussianVariance.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The variance estimate passes from finite positive-mass leaf cutoffs to the actual countable spin/cascade-leaf prior.

theorem OAI.InvariantIsing.cylinder_cgf_variance_le_of_finite_restrictions line 17

theorem OAI.InvariantIsing.countable_cylinder_cgf_variance_le line 69

Source documentation

The countable spin/leaf Gaussian log partition inherits the uniform coefficient variance bound from the finite-dimensional Gaussian Poincaré inequality.

theorem countable_cylinder_cgf_variance_le (hpub : GaussianLipschitzVarianceInput)
    {X : Type*} [MeasurableSpace X] [Countable X] [MeasurableSingletonClass X]
    (ν : Measure X) [IsProbabilityMeasure ν] (A : X → ℕ →₀ ℝ)
    (B : ℝ) (hB : 0 ≤ B) (hA : ∀ x, (A x).sum (fun _ c => c ^ 2) ≤ B) (t : ℝ) :
    variance (fun g : ℕ → ℝ => cgf (fun x => cylinderField (A x) g) ν t)
      gaussianCoordinates ≤ t ^ 2 * B := by
…

Mentions: OAI.InvariantIsing.GaussianLipschitzVarianceInput