CavityQuadraticAlgebra.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional algebra in cav:q-factor and the backward quadratic recursion. The factors retain their order: neither the two covariances nor the quadratic coefficient need commute.

def OAI.InvariantIsing.cavityBackwardQuadratic line 15
Source documentation
The coefficient K_i = K (1 - H_i K)⁻¹ of the backward quadratic.
```
def cavityBackwardQuadratic {d : ℕ} (K H : Matrix (Fin d) (Fin d) ℝ) :
    Matrix (Fin d) (Fin d) ℝ := K * (1 - H * K)⁻¹
```
def OAI.InvariantIsing.cavityStepTransition line 19
Source documentation
The conditional-mean matrix at a step from covariance P to C.
```
def cavityStepTransition {d : ℕ} (K P C : Matrix (Fin d) (Fin d) ℝ) :
    Matrix (Fin d) (Fin d) ℝ := (1 - (P - C) * cavityBackwardQuadratic K C)⁻¹
```
Mentions: OAI.InvariantIsing.cavityBackwardQuadratic
theorem OAI.InvariantIsing.cavity_quadratic_factor line 22
theorem OAI.InvariantIsing.cavity_quadratic_det_ratio line 34
theorem OAI.InvariantIsing.cavity_quadratic_step_isUnit line 42
theorem OAI.InvariantIsing.cavityStepTransition_eq line 48

theorem OAI.InvariantIsing.cavity_quadratic_backward_inverse line 63

Source documentation

The identity J_i T_i = J_{i-1} used in square completion.

theorem cavity_quadratic_backward_inverse {d : ℕ}
    (K P C : Matrix (Fin d) (Fin d) ℝ)
    (hP : IsUnit (1 - P * K).det) (hC : IsUnit (1 - C * K).det) :
    (1 - C * K)⁻¹ * cavityStepTransition K P C = (1 - P * K)⁻¹ := by
…

Mentions: OAI.InvariantIsing.cavityStepTransition

theorem OAI.InvariantIsing.cavityBackwardQuadratic_step line 72
Source documentation
The backward coefficient after integrating one level is exactly K_{i-1}; this is the matrix identity in cav:q-gaussian-integral.
```
theorem cavityBackwardQuadratic_step {d : ℕ} (K P C : Matrix (Fin d) (Fin d) ℝ)
    (hP : IsUnit (1 - P * K).det) (hC : IsUnit (1 - C * K).det) :
    cavityBackwardQuadratic K C * cavityStepTransition K P C =
      cavityBackwardQuadratic K P := by
…
```
Mentions: OAI.InvariantIsing.cavityBackwardQuadratic, OAI.InvariantIsing.cavityStepTransition
theorem OAI.InvariantIsing.cavityBackwardQuadratic_transpose line 79
theorem OAI.InvariantIsing.cavityBackwardQuadratic_zero line 90