CavityResolvent.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The noncommuting resolvent identities in the quadratic cavity tilt. These finite matrix statements include the zero-dimensional convention.

def OAI.InvariantIsing.cavityResolvent line 13
lemma OAI.InvariantIsing.cavity_inverse_pushThrough line 16
lemma OAI.InvariantIsing.cavity_inverse_difference line 24
lemma OAI.InvariantIsing.cavityResolvent_pushThrough line 33

theorem OAI.InvariantIsing.cavityResolvent_difference line 43

Source documentation

Equation cav:q-resolvent-difference, with the matrix factors in their required order. No commutation hypothesis is used.

theorem cavityResolvent_difference {d : ℕ} (K B C : Matrix (Fin d) (Fin d) ℝ)
    (hB : IsUnit (1 - B * K).det) (hC : IsUnit (1 - C * K).det) :
    cavityResolvent K B - cavityResolvent K C =
      (1 - B * K)⁻¹ * (B - C) * (1 - K * C)⁻¹ := by
…

Mentions: OAI.InvariantIsing.cavityResolvent

theorem OAI.InvariantIsing.cavityResolvent_difference_symmetric line 53

theorem OAI.InvariantIsing.cavityResolvent_spectral_transform line 66

Source documentation

The quadratic tilt replaces the original spectral block by the full block in its resolvent, exactly as in cav:q-transform.

theorem cavityResolvent_spectral_transform {d : ℕ}
    (A A0 : Matrix (Fin d) (Fin d) ℝ) (b : ℝ)
    (h0 : IsUnit (b • (1 : Matrix (Fin d) (Fin d) ℝ) - A0).det)
    (hA : IsUnit (b • (1 : Matrix (Fin d) (Fin d) ℝ) - A).det) :
    cavityResolvent (A - A0) ((b • (1 : Matrix (Fin d) (Fin d) ℝ) - A0)⁻¹) =
      (b • (1 : Matrix (Fin d) (Fin d) ℝ) - A)⁻¹ := by
…

Mentions: OAI.InvariantIsing.cavityResolvent