FiniteGaussianVariance.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite Gaussian cutoff partition functions in the Euclidean norm.

def OAI.InvariantIsing.finiteGaussianLogPartition line 19
Source documentation
The finite-cutoff Gaussian log partition, with arbitrary probability weights and deterministic base energy. In the application the finite state space is a positive-mass restriction of the spin/cascade-leaf prior.
```
def finiteGaussianLogPartition {X : Type*} [MeasurableSpace X]
    (ν : Measure X) (H : X → ℝ) {d : ℕ}
    (A : X → EuclideanSpace ℝ (Fin d)) (g : EuclideanSpace ℝ (Fin d)) : ℝ :=
…
```
theorem OAI.InvariantIsing.finiteGaussianLogPartition_lipschitz line 24

theorem OAI.InvariantIsing.finiteGaussianLogPartition_variance_le line 45

Source documentation

The Gaussian Poincaré inequality bounds the finite-cutoff log partition variance by the coefficient squared norm, uniformly in the cutoff and base energy.

theorem finiteGaussianLogPartition_variance_le (hpub : GaussianLipschitzVarianceInput)
    {X : Type*} [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X]
    (ν : Measure X) [IsProbabilityMeasure ν] (H : X → ℝ) {d : ℕ}
    (A : X → EuclideanSpace ℝ (Fin d)) (B : ℝ≥0)
    (hA : ∀ x, ‖A x‖ ^ 2 ≤ B) :
    variance (finiteGaussianLogPartition ν H A)
      (stdGaussian (EuclideanSpace ℝ (Fin d))) ≤ B := by
…

Mentions: OAI.InvariantIsing.GaussianLipschitzVarianceInput, OAI.InvariantIsing.finiteGaussianLogPartition

theorem OAI.InvariantIsing.finite_cylinder_cgf_variance_le line 61

Source documentation

Finite-state countable-cylinder restriction. A finite family of finitely supported coefficients uses a common finite prefix, whose Gaussian law is the standard Euclidean Gaussian.

theorem finite_cylinder_cgf_variance_le (hpub : GaussianLipschitzVarianceInput)
    {X : Type*} [Fintype X] [MeasurableSpace 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