CavityGaussianFactorAlgebra.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The finite matrix identities connecting standard-Gaussian square completion with the original, possibly singular, covariance B Bᵀ.

def OAI.InvariantIsing.cavityFactorPrecision line 13
theorem OAI.InvariantIsing.cavity_factor_det line 16
theorem OAI.InvariantIsing.cavity_inverse_factor line 23
Source documentation
The ordered inverse identity required by the square-completion coefficient. No inverse of the covariance factor is needed.
```
theorem cavity_inverse_factor {d : ℕ} (A B : Matrix (Fin d) (Fin d) ℝ)
    (h : IsUnit (1 - B * A).det) :
    (1 - A * B)⁻¹ = 1 + A * (1 - B * A)⁻¹ * B := by
…
```
theorem OAI.InvariantIsing.cavity_covariance_inverse line 32
theorem OAI.InvariantIsing.cavity_factor_quadratic_coefficient line 39