OAI/Probability/InvariantIsing/Cavity/CavityCouplingAlgebra.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The orthogonal spectral directions in the finite cavity coupling. Each spectral image of the cavity columns is normalized separately. The resulting frame carries the small square-root stack isometrically back to the original cavity columns.

  1. lemma OAI.InvariantIsing.cavityNormalizeFrame_mul_sqrt line 17
  2. lemma OAI.InvariantIsing.cavityNormalizeFrame_crossGram line 23
  3. def OAI.InvariantIsing.cavityEigenspaceFrame line 33
  4. theorem OAI.InvariantIsing.cavityEigenspaceFrame_gram line 38
  5. theorem OAI.InvariantIsing.cavityEigenspaceFrame_stack line 65
  6. lemma OAI.InvariantIsing.cavityNormalizeFrame_eigen line 82
  7. theorem OAI.InvariantIsing.cavityEigenspaceFrame_eigen line 88
  8. theorem OAI.InvariantIsing.cavityEigenspaceFrame_compression line 105
  9. theorem OAI.InvariantIsing.cavityEigenspaceFrame_special_gram line 116
  10. theorem OAI.InvariantIsing.cavityEigenspaceFrame_special_perp line 128
  11. lemma OAI.InvariantIsing.cavitySpecialBlocks_pullback line 142
  12. theorem OAI.InvariantIsing.cavityEigenspaceFrame_blocks line 149
  13. lemma OAI.InvariantIsing.measurable_cavityEigenspaceFrame line 162
  14. lemma OAI.InvariantIsing.cavityEigenspaceFrame_left_orthogonal line 170