OAI/Probability/InvariantIsing/Cavity/CavitySchurSpectrum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.cavity_complete_basis_gram line 14
2. lemma OAI.InvariantIsing.cavity_complete_basis_blocks line 26
3. theorem OAI.InvariantIsing.cavity_complete_blocks_inverse line 36

   Source documentation

   The resolvent of the full special/cavity block is the same complete orthogonal compression of the original spectral resolvent.

   theorem cavity_complete_blocks_inverse {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)
       (hD : IsUnit (b • (1 : Matrix (Fin r) (Fin r) ℝ) - D).det) :
       (b • (1 : Matrix (Fin d ⊕ Fin n) (Fin d ⊕ Fin n) ℝ) -
         cavitySpecialBlocks D B E)⁻¹ = cavitySpecialBlocks (b • 1 - D)⁻¹ B E := by
   …

   Mentions: OAI.InvariantIsing.cavitySpecialBlocks

4. lemma OAI.InvariantIsing.cavityRepeatedSpectrum_shift line 63
5. lemma OAI.InvariantIsing.cavityRepeatedSpectrum_inverse_mul line 73
6. lemma OAI.InvariantIsing.cavityRepeatedSpectrum_resolvent line 85
7. theorem OAI.InvariantIsing.cavity_limiting_blocks_compression line 94

   Source documentation

   Exact cav:compression: the limiting cavity columns produce the scalar finite-law Stieltjes transform, for every complete complement.

   theorem cavity_limiting_blocks_compression {m d n : ℕ}
       (rho lam : Fin m → ℝ) (b : ℝ)
       (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