OAI/Probability/InvariantIsing/Cavity/CavitySchurDeterminant.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.cavity_schur_determinant line 13
2. theorem OAI.InvariantIsing.cavity_schur_det_of_scalar_compression line 30

   Source documentation

   The x^n Schur factor in cav:determinant, before evaluating the characteristic polynomial of the full repeated spectrum.

   theorem cavity_schur_det_of_scalar_compression {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) :
       (b • (1 : Matrix (Fin d) (Fin d) ℝ) - A).det =
         x ^ n * (b • (1 : Matrix (Fin d ⊕ Fin n) (Fin d ⊕ Fin n) ℝ) -
           Matrix.fromBlocks A L L.transpose C).det := by
   …

3. theorem OAI.InvariantIsing.cavity_tilt_determinant_ratio line 57

   Source documentation

   The first equality of cav:determinant, valid without commuting A and A₀.

   theorem cavity_tilt_determinant_ratio {d : ℕ}
       (A A₀ : Matrix (Fin d) (Fin d) ℝ) (b : ℝ)
       (hA₀ : IsUnit (b • (1 : Matrix (Fin d) (Fin d) ℝ) - A₀).det) :
       (1 - (b • (1 : Matrix (Fin d) (Fin d) ℝ) - A₀)⁻¹ * (A - A₀)).det =
         (b • (1 : Matrix (Fin d) (Fin d) ℝ) - A).det /
           (b • (1 : Matrix (Fin d) (Fin d) ℝ) - A₀).det := by
   …