CavityScalarSpin.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The ordinary terminal residual in the cavity spin factor. Its variance contributes a constant because every Ising spin has norm squared equal to the number of cavity sites.

lemma OAI.InvariantIsing.cavity_spin_linear_gaussian_integrable line 16
lemma OAI.InvariantIsing.cavity_spin_linear_gaussian_integral line 30
lemma OAI.InvariantIsing.cavity_residual_spin_integrable line 54

theorem OAI.InvariantIsing.cavity_residual_spin_integral line 71

Source documentation

The ordinary Gaussian residual supplies n*v/2 to the logarithm, independently of the chosen cavity spin.

theorem cavity_residual_spin_integral {n : ℕ} (v : ℝ≥0) (c : ℝ)
    (z : Fin n → ℝ) (ε : Spin n) :
    (∫ w : Fin n → ℝ, Real.exp (fieldEnergy (z + w) ε + (n : ℝ) * c / 2)
      ∂(vectorGaussianLaw n v : Measure (Fin n → ℝ))) =
        Real.exp (fieldEnergy z ε + (n : ℝ) * (c + v) / 2) := by
…

Mentions: OAI.InvariantIsing.Spin, OAI.InvariantIsing.fieldEnergy, OAI.InvariantIsing.vectorGaussianLaw

def OAI.InvariantIsing.cavityResidualSpinLog line 87
theorem OAI.InvariantIsing.cavityResidualSpinLog_eq line 94
Source documentation
The residual-integrated cavity terminal is a sum of one-site log cosh terminals plus the deterministic scalar contribution.
```
theorem cavityResidualSpinLog_eq (n : ℕ) (v : ℝ≥0) (c : ℝ) (z : Fin n → ℝ) :
    cavityResidualSpinLog n v c z =
      (n : ℝ) * (c + v) / 2 + ∑ i, Real.log (Real.cosh (z i)) := by
…
```
Mentions: OAI.InvariantIsing.cavityResidualSpinLog
lemma OAI.InvariantIsing.measurable_cavityResidualSpinLog line 103