OAI/Analysis/KadisonKastler/CompletedRows.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Completing a finite row by the square root of its missing mass.

  1. def OAI.KadisonKastler.rowSquare line 18
  2. theorem OAI.KadisonKastler.rowSquare_nonneg line 20
  3. def OAI.KadisonKastler.rowRemainder line 23
  4. theorem OAI.KadisonKastler.rowRemainder_star line 25
  5. theorem OAI.KadisonKastler.rowRemainder_square line 28
  6. theorem OAI.KadisonKastler.rowRemainder_norm_le line 32
  7. def OAI.KadisonKastler.completedRow line 42
  8. theorem OAI.KadisonKastler.completedRow_normalized line 45
  9. theorem OAI.KadisonKastler.completedRow_average line 52
  10. theorem OAI.KadisonKastler.rowRemainder_apply_norm_sq line 71
  11. theorem OAI.KadisonKastler.completedRow_average_error line 86