OAI/Probability/InvariantIsing/Cavity/CavityCompressionLimitGeometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The limiting frame extracted from the concrete compression has the orthogonality and completeness used in the finite spectral cavity model.

  1. def OAI.InvariantIsing.cavityCompressionLimitFrame line 15
  2. lemma OAI.InvariantIsing.cavitySpectralStack_scalar_eq line 19
  3. lemma OAI.InvariantIsing.cavityCompressionLimitFrame_gram line 26
  4. lemma OAI.InvariantIsing.cavityCompressionLimitFrame_perp line 34
  5. theorem OAI.InvariantIsing.cavityCompressionLimitFrame_complete line 49