CavityScalarRecursion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Independent-site backward recursion after the ordinary cavity residual is integrated. The residual contributes an additive constant.

lemma OAI.InvariantIsing.cavity_sum_logCosh_linearGrowth line 14
lemma OAI.InvariantIsing.cavity_vector_recursion_const_add line 27

theorem OAI.InvariantIsing.cavityResidualSpinLog_recursion line 64

Source documentation

The transformed cavity spin recursion separates into one identical scalar recursion per cavity site; the ordinary residual is not a new Poisson level.

theorem cavityResidualSpinLog_recursion (N : ℕ) (hN : 0 < N)
    (n : ℕ) (b : ℕ → ℝ) (v : ℕ → ℝ≥0) (hb : ∀ i < n, 0 < b i)
    (r : ℝ≥0) (c : ℝ) (z : Fin N → ℝ) :
    cascadeRecursion n b (fun i => vectorGaussianLaw N (v i)) (fun _ p => p.1 + p.2)
      (cavityResidualSpinLog N r c) z =
      (N : ℝ) * (c + r) / 2 +
        ∑ i, cascadeRecursion n b (gaussianCascadeMarks v) (fun _ p => p.1 + p.2)
          (fun y => Real.log (Real.cosh y)) (z i) := by
…

Mentions: OAI.InvariantIsing.vectorGaussianLaw, OAI.InvariantIsing.cavityResidualSpinLog, OAI.InvariantIsing.gaussianCascadeMarks