OAI/Analysis/KadisonSimilarity/Representation/SpectralDensityIsometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Multiplication by a square-root density identifies the scalar L² coordinates of a spectral measure with a subspace over a common base measure.

  1. def OAI.KadisonSimilarity.squaredDensityMeasure line 19
  2. theorem OAI.KadisonSimilarity.weightedContinuous_memLp line 23
  3. def OAI.KadisonSimilarity.weightedContinuousVector line 31
  4. theorem OAI.KadisonSimilarity.weightedContinuousVector_ae line 35
  5. def OAI.KadisonSimilarity.weightedContinuousLinear line 39
  6. theorem OAI.KadisonSimilarity.weight_memLp_of_finite_squareDensity line 67
  7. theorem OAI.KadisonSimilarity.weightedContinuous_norm line 77
  8. def OAI.KadisonSimilarity.spectralDensityIsometry line 92
  9. theorem OAI.KadisonSimilarity.spectralDensityIsometry_toLp line 114
  10. def OAI.KadisonSimilarity.spectralDensityIsometryOfEq line 134
  11. theorem OAI.KadisonSimilarity.spectralDensityIsometryOfEq_toLp line 140