CavityFiniteNormalizer.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Evaluation of the quadratic root/gap/residual normalizer on a finite trial overlap path. No quadratic marking or limiting formula is assumed.

def OAI.InvariantIsing.cavityFiniteQuadraticMean line 15
lemma OAI.InvariantIsing.cavity_finite_normalizer_algebra line 22

theorem OAI.InvariantIsing.cavity_finite_quadratic_mean line 55

Source documentation

The finite-multiplicity quadratic normalizer, including the ordinary last Gaussian integration, is exactly the required path integral.

theorem cavity_finite_quadratic_mean {m d N l : ℕ}
    (rho lam : Fin m → ℝ) (hrho : ∀ a, 0 < rho a) (hsum : ∑ a, rho a = 1)
    (B : Matrix (Fin (m * N)) (Fin d) ℝ) (hB : B.transpose * B = 1)
    (hBE : B.transpose * cavityLimitingStack (n := N) rho = 0)
…

Mentions: OAI.InvariantIsing.cavityLimitingStack