OAI/Probability/InvariantIsing/Cavity/CavitySpectralImages.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The separate spectral images of the cavity columns. These are the concrete inputs to the normalized-frame coupling construction.

  1. def OAI.InvariantIsing.cavitySpectralImage line 14
  2. lemma OAI.InvariantIsing.cavitySpectralImage_sum line 18
  3. lemma OAI.InvariantIsing.cavitySpectralImage_crossGram line 24
  4. lemma OAI.InvariantIsing.cavitySpectralImage_gram line 36
  5. lemma OAI.InvariantIsing.cavitySpectralImage_eigen line 50
  6. lemma OAI.InvariantIsing.measurable_cavitySpectralImage line 62
  7. theorem OAI.InvariantIsing.cavitySpectralImage_coupling_blocks line 72