OAI/Probability/InvariantIsing/Cavity/CavityNormalizerIntegral.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite root, positive-level and ordinary residual pieces of the quadratic normalizer are the integral of D_p(r) R'(D_p(r)).

  1. def OAI.InvariantIsing.cavityNormalizerDensity line 15
  2. lemma OAI.InvariantIsing.continuous_cavityNormalizerDensity line 19
  3. lemma OAI.InvariantIsing.integral_cavityNormalizer_gap line 25
  4. lemma OAI.InvariantIsing.integral_cavityNormalizer_root line 59
  5. lemma OAI.InvariantIsing.integral_cavityNormalizer_tail line 72
  6. lemma OAI.InvariantIsing.cavity_integral_finite_partition line 102
  7. theorem OAI.InvariantIsing.finite_overlap_normalizer_integral line 121

    Source documentation

    The exact finite-step normalizer integral, including both the common root and the terminal residual of exponent one.

    theorem finite_overlap_normalizer_integral {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 : StrictMono q)
    (hp : ∀ j r, r ∈ Ioo (cut j.castSucc) (cut j.succ) → p r = q j)
    (htop : q (Fin.last n) < 1) :
    (∫ r in 0..1, cavityNormalizerDensity rho lam hrho hsum p r) =
      q 0 * deficit p (q 0) * cavityRDerivative rho lam hrho hsum (deficit p (q 0)) +
      (∑ i : Fin n, (cavityLogDetPotential rho lam hrho hsum (deficit p (q i.castSucc)) -
        cavityLogDetPotential rho lam hrho hsum (deficit p (q i.succ))) / cut i.castSucc.succ) +
      cavityLogDetPotential rho lam hrho hsum (deficit p (q (Fin.last n))) := by
…

    Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.cavityNormalizerDensity, OAI.InvariantIsing.cavityRDerivative, OAI.InvariantIsing.cavityLogDetPotential