OAI/Analysis/KadisonSimilarity/Representation/VectorSpectralMeasure.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The scalar spectral measure of a vector in a representation of C(X).

  1. def OAI.KadisonSimilarity.VectorSpectralMeasure.realCM line 16
  2. lemma OAI.KadisonSimilarity.VectorSpectralMeasure.realCM_apply line 17
  3. lemma OAI.KadisonSimilarity.VectorSpectralMeasure.realCM_add line 18
  4. lemma OAI.KadisonSimilarity.VectorSpectralMeasure.realCM_sub line 19
  5. lemma OAI.KadisonSimilarity.VectorSpectralMeasure.realCM_smul line 20
  6. lemma OAI.KadisonSimilarity.VectorSpectralMeasure.realCM_one line 21
  7. lemma OAI.KadisonSimilarity.VectorSpectralMeasure.real_nonneg line 24
  8. def OAI.KadisonSimilarity.VectorSpectralMeasure.functional line 36
  9. def OAI.KadisonSimilarity.VectorSpectralMeasure.measure line 49
  10. instance OAI.KadisonSimilarity.VectorSpectralMeasure.(instance at line 50) line 50
  11. instance OAI.KadisonSimilarity.VectorSpectralMeasure.(instance at line 51) line 51
  12. lemma OAI.KadisonSimilarity.VectorSpectralMeasure.integral_real line 52
  13. lemma OAI.KadisonSimilarity.VectorSpectralMeasure.integral_complex line 54
  14. lemma OAI.KadisonSimilarity.VectorSpectralMeasure.measure_univ line 82