OAI/Analysis/Unitarizability/LocalBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Individual block row and column bounds from the endpoint assignment.

  1. theorem OAI.Dixmier.Masked.support_bound line 15
  2. def OAI.Dixmier.Masked.rowMask line 25
  3. def OAI.Dixmier.Masked.columnMask line 28
  4. theorem OAI.Dixmier.Masked.rowMask_norm line 32
  5. theorem OAI.Dixmier.Masked.complement_norm line 39
  6. theorem OAI.Dixmier.Masked.columnMask_norm line 43
  7. theorem OAI.Dixmier.Masked.rowMask_support line 51
  8. theorem OAI.Dixmier.Masked.columnMask_support line 59
  9. theorem OAI.Dixmier.Masked.row_localization line 67
  10. theorem OAI.Dixmier.Masked.column_localization line 74
  11. theorem OAI.Dixmier.Masked.local_row_bound line 95
  12. theorem OAI.Dixmier.Masked.local_column_bound line 107