CavitySchurEvaluation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The finite Schur-complement evaluation in cav:compression and cav:scalar-field. All block inverses are ordinary nonsingular inverses.

lemma OAI.InvariantIsing.cavity_block_inverse_bottom line 13
lemma OAI.InvariantIsing.cavity_block_shift line 24

theorem OAI.InvariantIsing.cavity_schur_resolvent_compression line 36

Source documentation

Compressing the full resolvent onto the cavity block gives the inverse of the Schur complement; no commutation of the special blocks is needed.

theorem cavity_schur_resolvent_compression {d n : ℕ}
    (A : Matrix (Fin d) (Fin d) ℝ) (L : Matrix (Fin d) (Fin n) ℝ)
    (C : Matrix (Fin n) (Fin n) ℝ) (b : ℝ)
    (hA : IsUnit (b • (1 : Matrix (Fin d) (Fin d) ℝ) - A).det)
    (hM : IsUnit (b • (1 : Matrix (Fin d ⊕ Fin n) (Fin d ⊕ Fin n) ℝ) -
      Matrix.fromBlocks A L L.transpose C).det) :
    ((b • (1 : Matrix (Fin d ⊕ Fin n) (Fin d ⊕ Fin n) ℝ) -
      Matrix.fromBlocks A L L.transpose C)⁻¹).toBlocks₂₂ =
        (b • 1 - C - L.transpose * (b • 1 - A)⁻¹ * L)⁻¹ := by
…

theorem OAI.InvariantIsing.cavity_schur_scalar_field line 51

Source documentation

The scalar compression x I forces the cavity field to be (b - 1/x) I, the finite identity cav:scalar-field.

theorem cavity_schur_scalar_field {d n : ℕ}
    (A : Matrix (Fin d) (Fin d) ℝ) (L : Matrix (Fin d) (Fin n) ℝ)
    (C : Matrix (Fin n) (Fin n) ℝ) (b x : ℝ) (hx : x ≠ 0)
    (hA : IsUnit (b • (1 : Matrix (Fin d) (Fin d) ℝ) - A).det)
    (hM : IsUnit (b • (1 : Matrix (Fin d ⊕ Fin n) (Fin d ⊕ Fin n) ℝ) -
      Matrix.fromBlocks A L L.transpose C).det)
    (hcompression : ((b • (1 : Matrix (Fin d ⊕ Fin n) (Fin d ⊕ Fin n) ℝ) -
      Matrix.fromBlocks A L L.transpose C)⁻¹).toBlocks₂₂ = x • 1) :
    C + L.transpose * (b • 1 - A)⁻¹ * L = (b - x⁻¹) • 1 := by
…

theorem OAI.InvariantIsing.cavity_schur_tilted_field line 91

Source documentation

Inserting the already proved quadratic resolvent transform gives the same scalar cavity field expressed in the original covariance.

theorem cavity_schur_tilted_field {d n : ℕ}
    (A A₀ : Matrix (Fin d) (Fin d) ℝ) (L : Matrix (Fin d) (Fin n) ℝ)
    (C : Matrix (Fin n) (Fin n) ℝ) (b x : ℝ) (hx : x ≠ 0)
    (hA₀ : IsUnit (b • (1 : Matrix (Fin d) (Fin d) ℝ) - A₀).det)
    (hA : IsUnit (b • (1 : Matrix (Fin d) (Fin d) ℝ) - A).det)
    (hM : IsUnit (b • (1 : Matrix (Fin d ⊕ Fin n) (Fin d ⊕ Fin n) ℝ) -
      Matrix.fromBlocks A L L.transpose C).det)
    (hcompression : ((b • (1 : Matrix (Fin d ⊕ Fin n) (Fin d ⊕ Fin n) ℝ) -
      Matrix.fromBlocks A L L.transpose C)⁻¹).toBlocks₂₂ = x • 1) :
    C + L.transpose * cavityResolvent (A - A₀) (b • 1 - A₀)⁻¹ * L =
      (b - x⁻¹) • 1 := by
…

Mentions: OAI.InvariantIsing.cavityResolvent