OAI/Analysis/KadisonKastler/DiagonalLocalVectors.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Local vector representatives for a diagonal operator

Apply the operator to constant vectors cut off on [-n,n]. Locality makes these representatives agree on overlaps. Selecting the interval of radius ceil |t| gives measurable vector values on the whole line.

  1. def OAI.KadisonKastler.diagonalTestVector line 22
  2. theorem OAI.KadisonKastler.diagonalTestVector_ae line 26
  3. theorem OAI.KadisonKastler.diagonalTestVector_add line 32
  4. theorem OAI.KadisonKastler.diagonalTestVector_smul line 37
  5. def OAI.KadisonKastler.diagonalRawVector line 46
  6. theorem OAI.KadisonKastler.diagonalRawVector_measurable line 50
  7. theorem OAI.KadisonKastler.diagonalRawVector_add_ae line 63
  8. theorem OAI.KadisonKastler.diagonalRawVector_smul_ae line 77
  9. theorem OAI.KadisonKastler.diagonalRawVector_norm_ae line 94
  10. theorem OAI.KadisonKastler.diagonalRawVector_eq_local_ae line 107