OAI/Probability/InvariantIsing/Cavity/CavityGaussianPenalty.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Gaussian integration by parts with a nonuniform one-replica penalty. The bound depends on the cavity projection size, not its maximum over all spin configurations.

  1. lemma OAI.InvariantIsing.cavity_gaussian_penalty_insertion line 15
  2. theorem OAI.InvariantIsing.cavity_gaussian_penalty_nonneg line 64

    Source documentation

    A penalty of 4c V absorbs a covariance insertion bounded by c(V(x)+V(y)), uniformly over the other base energy.

    theorem cavity_gaussian_penalty_nonneg {X : Type*} [Fintype X]
    {d : ℕ} {w : X → ℝ} (hw : GibbsReference w) (H V : X → ℝ)
    (A C : X → Fin (d + 1) → ℝ) (c : ℝ)
    (hK : ∀ x y, |gaussianCross A C x y| ≤ c * (V x + V y)) :
    0 ≤ ∫ g, ∑ x, gaussianGibbs w H C g x * (4 * c * V x + linearGaussian A g x)
      ∂Measure.pi (fun _ : Fin (d + 1) => gaussianReal 0 1) := by
…