OAI/Probability/InvariantIsing/Cavity/CavityFiniteLogDet.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.cavity_labeled_shift_isUnit line 16
2. theorem OAI.InvariantIsing.cavity_finite_tilt_determinant line 32

   Source documentation

   The multiplicity formula with all Schur/invertibility hypotheses obtained from the actual repeated-spectrum geometry.

   theorem cavity_finite_tilt_determinant {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

3. theorem OAI.InvariantIsing.cavity_finite_tilt_logdet line 90
4. theorem OAI.InvariantIsing.cavity_finite_root_trace line 110

   Source documentation

   Root contraction after the matrix and scalar log-determinant calculations. The only multiplicity data are those of the finite model.

   theorem cavity_finite_root_trace {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