CavitySpectralGap.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The upper spectral gap supplies the diagonal inverse-gap hypothesis used by the quadratic cavity recursion.

lemma OAI.InvariantIsing.cavity_upper_spectral_gap line 13
lemma OAI.InvariantIsing.cavity_resolvent_diagonal_gap line 23

theorem OAI.InvariantIsing.cavity_resolvent_step_precision line 41

Source documentation

A nonterminal step, where both resolvents have positive arguments.

theorem cavity_resolvent_step_precision {d : ℕ}
    (A B : Matrix (Fin d) (Fin d) ℝ) (eig : Fin d → ℝ) (L b₀ b₁ : ℝ)
    (hK : (A - Matrix.diagonal eig).transpose = A - Matrix.diagonal eig)
    (hA : (L • (1 : Matrix (Fin d) (Fin d) ℝ) - A).PosSemidef)
    (heig : ∀ i, eig i ≤ L) (hb₀ : L < b₀) (hb₁ : b₀ ≤ b₁)
    (hB : Matrix.diagonal (fun i => (b₀ - eig i)⁻¹) -
      Matrix.diagonal (fun i => (b₁ - eig i)⁻¹) = B * B.transpose) :
    (cavityFactorPrecision
      (cavityBackwardQuadratic (A - Matrix.diagonal eig)
        (Matrix.diagonal (fun i => (b₁ - eig i)⁻¹))) B).PosDef := by
…

Mentions: OAI.InvariantIsing.cavityFactorPrecision, OAI.InvariantIsing.cavityBackwardQuadratic

theorem OAI.InvariantIsing.cavity_resolvent_terminal_precision line 67

Source documentation

The residual endpoint has lower covariance zero.

theorem cavity_resolvent_terminal_precision {d : ℕ}
    (A B : Matrix (Fin d) (Fin d) ℝ) (eig : Fin d → ℝ) (L b : ℝ)
    (hK : (A - Matrix.diagonal eig).transpose = A - Matrix.diagonal eig)
    (hA : (L • (1 : Matrix (Fin d) (Fin d) ℝ) - A).PosSemidef)
    (heig : ∀ i, eig i ≤ L) (hb : L < b)
    (hB : Matrix.diagonal (fun i => (b - eig i)⁻¹) = B * B.transpose) :
    (cavityFactorPrecision (A - Matrix.diagonal eig) B).PosDef := by
…

Mentions: OAI.InvariantIsing.cavityFactorPrecision