CavityQuadraticCovariance.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The matrix covariance identities of cav:q-innovations. These identities apply also to zero covariance increments.

theorem OAI.InvariantIsing.cavity_rescaled_step_covariance line 15

Source documentation

Rescaling a tilted-step covariance by J_i gives the innovation covariance with the previous inverse on the left.

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

Mentions: OAI.InvariantIsing.cavityStepTransition

theorem OAI.InvariantIsing.cavity_innovation_covariance_mul line 25

Source documentation

The covariance increment transforms by the resolvent difference. This multiplication form does not require a nonzero cascade exponent.

theorem cavity_innovation_covariance_mul {d : ℕ}
    (K P C S : Matrix (Fin d) (Fin d) ℝ) (ζ : ℝ)
    (hK : K.transpose = K) (hC : C.transpose = C)
    (hPdet : IsUnit (1 - P * K).det) (hCdet : IsUnit (1 - C * K).det)
    (hΔ : P - C = ζ • S) :
    ζ • ((1 - P * K)⁻¹ * S * ((1 - C * K)⁻¹).transpose) =
      cavityResolvent K P - cavityResolvent K C := by
…

Mentions: OAI.InvariantIsing.cavityResolvent

theorem OAI.InvariantIsing.cavity_innovation_covariance line 36

Source documentation

The positive-level covariance formula in cav:q-innovations.

theorem cavity_innovation_covariance {d : ℕ}
    (K P C S : Matrix (Fin d) (Fin d) ℝ) (ζ : ℝ) (hζ : ζ ≠ 0)
    (hK : K.transpose = K) (hC : C.transpose = C)
    (hPdet : IsUnit (1 - P * K).det) (hCdet : IsUnit (1 - C * K).det)
    (hΔ : P - C = ζ • S) :
    (1 - C * K)⁻¹ * (cavityStepTransition K P C * S) *
        ((1 - C * K)⁻¹).transpose =
      ζ⁻¹ • (cavityResolvent K P - cavityResolvent K C) := by
…

Mentions: OAI.InvariantIsing.cavityStepTransition, OAI.InvariantIsing.cavityResolvent