OAI/Probability/InvariantIsing/Cavity/CavityCompressionRank.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Full rank of the actual spectral compressions, with the eigenvalue groups arranged in their given consecutive coordinate windows.

  1. lemma OAI.InvariantIsing.cavityColumns_gram line 15
  2. lemma OAI.InvariantIsing.cavityColumns_eq_mul line 26
  3. lemma OAI.InvariantIsing.cavityCompressionGrams_eq_window line 35
  4. theorem OAI.InvariantIsing.cavityCompressionGrams_posDef_ae line 49