CavityStepPrecision.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Precision positivity for a finite-alphabet covariance step. The upper covariance is positive diagonal; the lower one is either positive diagonal or zero, as at the terminal endpoint of the cavity recursion.

lemma OAI.InvariantIsing.cavity_diagonal_interpolation_isUnit line 15

theorem OAI.InvariantIsing.cavity_step_precision_posDef line 41

Source documentation

Positivity of I-Bᵀ K_i B from the actual diagonal covariance ordering and the upper spectral gap. B Bᵀ = P-C may be singular.

theorem cavity_step_precision_posDef {d : ℕ}
    (K B : Matrix (Fin d) (Fin d) ℝ) (hK : K.transpose = K)
    (p c : Fin d → ℝ) (hp : ∀ i, 0 < p i) (hc0 : ∀ i, 0 ≤ c i)
    (hcp : ∀ i, c i ≤ p i) (hc : (∀ i, c i = 0) ∨ (∀ i, 0 < c i))
    (hgap : (Matrix.diagonal (fun i => (p i)⁻¹) - K).PosDef)
    (hB : Matrix.diagonal p - Matrix.diagonal c = B * B.transpose) :
    (cavityFactorPrecision (cavityBackwardQuadratic K (Matrix.diagonal c)) B).PosDef := by
…

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