OAI/Probability/InvariantIsing/Cavity/CavityValueIdentity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The deterministic cavity value in the variational normalization. The field pairing and spectral term arise from the weighted layer cake and the spectral integration-by-parts identity.

  1. lemma OAI.InvariantIsing.cavity_value_pairing_identity line 16
  2. lemma OAI.InvariantIsing.cavityFieldStep_pairing line 54
  3. theorem OAI.InvariantIsing.cavity_finite_value_identity line 70

    Source documentation

    The scalar Gaussian spin term plus the quadratic normalizer is exactly the field value, field pairing, and spectral functional.

    theorem cavity_finite_value_identity {m n : ℕ} (rho lam : Fin m → ℝ)
    (hrho : ∀ a, 0 < rho a) (hsum : ∑ a, rho a = 1) (p : OverlapPath)
    (cut : Fin (n + 2) → ℝ) (hcut : StrictMono cut)
    (hfirst : cut 0 = 0) (hlast : cut (Fin.last (n + 1)) = 1)
    (q : Fin (n + 1) → ℝ) (hq : Monotone q) (hq0 : ∀ i, 0 ≤ q i)
    (hp : ∀ j s, s ∈ Ioo (cut j.castSucc) (cut j.succ) → p s = q j) :
    let h := cavityFieldStep rho lam hrho hsum p cut hcut hfirst hlast q hq hq0
…

    Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.cavityFieldStep