OAI/Probability/InvariantIsing/Gaussian/GaussianMeanInterpolation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite Gaussian mean interpolation with arbitrary base energy and weights.

  1. def OAI.InvariantIsing.affineGaussianCoefficients line 16
  2. lemma OAI.InvariantIsing.linearGaussian_affine line 20
  3. def OAI.InvariantIsing.affineGaussianMean line 27
  4. def OAI.InvariantIsing.affineGaussianSlope line 32
  5. lemma OAI.InvariantIsing.affineGaussianMean_hasDerivAt line 36
  6. lemma OAI.InvariantIsing.expectedGaussianEnergy_abs_le line 67
  7. theorem OAI.InvariantIsing.affineGaussianMean_abs_sub_le line 108

    Source documentation

    A dimension-independent mean comparison. The cross-covariance of the increment with the interpolated field, rather than the Gaussian coordinate count, determines the bound.

    theorem affineGaussianMean_abs_sub_le {d : ℕ} {w : X → ℝ} (hw : GibbsReference w)
    (H : X → ℝ) (C A : X → Fin (d + 1) → ℝ) {K : ℝ}
    (hK : ∀ s ∈ Set.Icc (0 : ℝ) 1, ∀ x y,
      |gaussianCross A (affineGaussianCoefficients C A s) x y| ≤ K) :
    |affineGaussianMean w H C A 1 - affineGaussianMean w H C A 0| ≤ 2 * K := by
…

    Mentions: OAI.InvariantIsing.affineGaussianCoefficients, OAI.InvariantIsing.affineGaussianMean