OAI/Probability/InvariantIsing/Cavity/CavityGaussianRecursion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.cavity_scaled_sqrt_factor line 14
2. lemma OAI.InvariantIsing.cavity_scaled_factor_precision line 21
3. theorem OAI.InvariantIsing.cavity_scaled_step_precision line 29

   Source documentation

   The exact precision required by the Gaussian law, obtained from the diagonal covariance ordering, including zero covariance increments.

   theorem cavity_scaled_step_precision {d : ℕ}
       (K S : Matrix (Fin d) (Fin d) ℝ) (hK : K.transpose = K)
       (hS : S.PosSemidef) (ζ : ℝ) (hζ : 0 ≤ ζ)
       (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)
       (hΔ : Matrix.diagonal p - Matrix.diagonal c = ζ • S) :
       (cavityFactorPrecision (ζ • cavityBackwardQuadratic K (Matrix.diagonal c))
         (CFC.sqrt S)).PosDef := by
   …

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

4. lemma OAI.InvariantIsing.cavity_scaled_backward_step line 44
5. lemma OAI.InvariantIsing.cavity_scaled_step_determinant line 59
6. theorem OAI.InvariantIsing.cavity_gaussian_recursive_logIntegral line 73

   Source documentation

   The single backward Gaussian step cav:q-gaussian-integral. The precision hypothesis is supplied by cavity_scaled_step_precision for the manuscript's diagonal covariance path.

   theorem cavity_gaussian_recursive_logIntegral {d : ℕ}
       (K P C S : Matrix (Fin d) (Fin d) ℝ) (hK : K.transpose = K)
       (hC : C.transpose = C) (hS : S.PosSemidef) (ζ : ℝ) (hζ : 0 < ζ)
       (hPdet : IsUnit (1 - P * K).det) (hCdet : IsUnit (1 - C * K).det)
       (hΔ : P - C = ζ • S)
       (hQ : (cavityFactorPrecision (ζ • cavityBackwardQuadratic K C)
         (CFC.sqrt S)).PosDef) (u : EuclideanSpace ℝ (Fin d)) :
       (1 / ζ) * Real.log (∫ z : EuclideanSpace ℝ (Fin d),
         Real.exp (ζ / 2 * ⟪u + z, Matrix.toEuclideanCLM (𝕜 := ℝ)
   …

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