OAI/Analysis/KadisonSimilarity/Derivation/CommonCyclicEmbedding.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Embed the original separable Hilbert space into a single L² space by placing its cyclic spectral coordinates over one finite dominating measure.

  1. def OAI.KadisonSimilarity.cyclicCommonBaseMeasure line 26
  2. instance OAI.KadisonSimilarity.cyclicCommonBaseMeasure_finite line 29
  3. instance OAI.KadisonSimilarity.cyclicCommonBaseMeasure_regular line 33
  4. abbrev OAI.KadisonSimilarity.CommonCyclicHilbert line 39
  5. def OAI.KadisonSimilarity.cyclicDensityIsometryData line 42
  6. def OAI.KadisonSimilarity.cyclicDensityIsometry line 56
  7. def OAI.KadisonSimilarity.cyclicCommonFamilyData line 61
  8. def OAI.KadisonSimilarity.cyclicCommonFamily line 71
  9. theorem OAI.KadisonSimilarity.cyclicCommonFamily_orthogonal line 74
  10. opaque OAI.KadisonSimilarity.cyclicCommonEmbeddingData line 83
  11. def OAI.KadisonSimilarity.cyclicCommonEmbedding line 91
  12. theorem OAI.KadisonSimilarity.cyclicCommonEmbedding_component line 94