OAI/Probability/InvariantIsing/Cavity/CavitySchurFiniteR.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The scalar Schur field of the actual limiting cavity block is the finite spectral R-transform, including its prescribed value at zero.

  1. lemma OAI.InvariantIsing.cavity_compressed_shift_posDef line 13
  2. lemma OAI.InvariantIsing.cavitySpecialBlocks_symmetric_fromBlocks line 25
  3. theorem OAI.InvariantIsing.cavity_limiting_field_eq_finiteR line 36

    Source documentation

    The source field identity at its true finite-law inverse argument. Both required determinant hypotheses are derived from spectral positivity.

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

  4. theorem OAI.InvariantIsing.cavity_limiting_cavityBlock_eq_finiteR_zero line 83