OAI/Probability/InvariantIsing/Cavity/CavitySchurMultiplicity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.cavity_complete_conjugate_det line 14
2. theorem OAI.InvariantIsing.cavity_complete_blocks_determinant line 30

   Source documentation

   Determinants are preserved by the complete special/cavity basis, even though its two index types need not be definitionally equal.

   theorem cavity_complete_blocks_determinant {r d n : ℕ}
       (D : Matrix (Fin r) (Fin r) ℝ) (B : Matrix (Fin r) (Fin d) ℝ)
       (E : Matrix (Fin r) (Fin n) ℝ) (b : ℝ)
       (hB : B.transpose * B = 1) (hE : E.transpose * E = 1)
       (hBE : B.transpose * E = 0) (hcomplete : B * B.transpose + E * E.transpose = 1) :
       (b • (1 : Matrix (Fin d ⊕ Fin n) (Fin d ⊕ Fin n) ℝ) -
         cavitySpecialBlocks D B E).det =
           (b • (1 : Matrix (Fin r) (Fin r) ℝ) - D).det := by
   …

   Mentions: OAI.InvariantIsing.cavitySpecialBlocks

3. lemma OAI.InvariantIsing.cavityRepeatedSpectrum_shift_eq line 57
4. theorem OAI.InvariantIsing.cavityRepeatedSpectrum_determinant line 69

   Source documentation

   Every eigenvalue in the full limiting block occurs once for each cavity coordinate.

   theorem cavityRepeatedSpectrum_determinant {m n : ℕ} (lam : Fin m → ℝ) (b : ℝ) :
       (b • (1 : Matrix (Fin (m * n)) (Fin (m * n)) ℝ) -
         cavityRepeatedSpectrum (n := n) lam).det = ∏ a, (b - lam a) ^ n := by
   …

   Mentions: OAI.InvariantIsing.cavityRepeatedSpectrum

5. theorem OAI.InvariantIsing.cavity_limiting_blocks_determinant line 77
6. theorem OAI.InvariantIsing.cavity_finiteInverse_blocks_compression line 93

   Source documentation

   The actual inverse-transform argument realizes the compression x I without assuming a separate scalar resolvent identity.

   theorem cavity_finiteInverse_blocks_compression {m d n : ℕ}
       (rho lam : Fin m → ℝ) (hrho : ∀ a, 0 < rho a) (hsum : ∑ a, rho a = 1)
       (B : Matrix (Fin (m * n)) (Fin d) ℝ) (hB : B.transpose * B = 1)
       (hBE : B.transpose * cavityLimitingStack (n := n) rho = 0)
   …

   Mentions: OAI.InvariantIsing.cavityLimitingStack