OAI/Analysis/KadisonKastler/FiniteSupportRows.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Normalized finite rows from an orthogonal family of partial isometries. The missing initial projection is included as one extra row entry.

  1. def OAI.KadisonKastler.finiteSupportSum line 19
  2. theorem OAI.KadisonKastler.finiteSupportSum_projection line 22
  3. theorem OAI.KadisonKastler.finiteSupportSum_mul_member line 28
  4. theorem OAI.KadisonKastler.finiteSupportSum_mul_of_subset line 39
  5. def OAI.KadisonKastler.finiteSupportRow line 47
  6. theorem OAI.KadisonKastler.finiteSupportRow_normalized line 51
  7. theorem OAI.KadisonKastler.partialIsometry_mul_finiteSupportSum line 64
  8. theorem OAI.KadisonKastler.finiteSupportRow_diagonal_compression line 77
  9. theorem OAI.KadisonKastler.finiteSupportRow_localized_norm_le line 132