OAI/Analysis/Unitarizability/Triangular.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Bounded Hilbert sums and triangular representations.

  1. abbrev OAI.Dixmier.Triangular.Double line 14
  2. def OAI.Dixmier.Triangular.inl line 16
  3. def OAI.Dixmier.Triangular.inr line 20
  4. theorem OAI.Dixmier.Triangular.inl_apply line 24
  5. theorem OAI.Dixmier.Triangular.inr_apply line 25
  6. theorem OAI.Dixmier.Triangular.inl_norm line 26
  7. theorem OAI.Dixmier.Triangular.inr_norm line 27
  8. def OAI.Dixmier.Triangular.diagonal line 29
  9. theorem OAI.Dixmier.Triangular.diagonal_fst line 33
  10. theorem OAI.Dixmier.Triangular.diagonal_snd line 35
  11. def OAI.Dixmier.Triangular.operator line 38
  12. theorem OAI.Dixmier.Triangular.operator_fst line 41
  13. theorem OAI.Dixmier.Triangular.operator_snd line 43
  14. theorem OAI.Dixmier.Triangular.diagonal_norm_map line 46
  15. theorem OAI.Dixmier.Triangular.operator_norm_le line 52
  16. theorem OAI.Dixmier.Triangular.inv_apply line 70
  17. def OAI.Dixmier.Triangular.representation line 74
  18. theorem OAI.Dixmier.Triangular.representation_bound line 95