OAI/Analysis/Crouzeix/Realization.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Realization.

  1. theorem OAI.CrouzeixHilbert.Realization.exists_isometryEquiv_of_norm_eq line 21
  2. abbrev OAI.CrouzeixHilbert.Realization.SumSpace line 52
  3. def OAI.CrouzeixHilbert.Realization.pairL line 54
  4. def OAI.CrouzeixHilbert.Realization.rowL line 57
  5. theorem OAI.CrouzeixHilbert.Realization.pairL_apply line 60
  6. theorem OAI.CrouzeixHilbert.Realization.rowL_apply line 63
  7. theorem OAI.CrouzeixHilbert.Realization.adjoint_pairL line 68
  8. theorem OAI.CrouzeixHilbert.Realization.exists_colligation line 85
  9. structure OAI.CrouzeixHilbert.Realization.Colligation line 122
  10. def OAI.CrouzeixHilbert.Realization.Colligation.a line 127
  11. def OAI.CrouzeixHilbert.Realization.Colligation.b line 131
  12. def OAI.CrouzeixHilbert.Realization.Colligation.c line 135
  13. def OAI.CrouzeixHilbert.Realization.Colligation.d line 139
  14. theorem OAI.CrouzeixHilbert.Realization.Colligation.apply_pair line 143
  15. theorem OAI.CrouzeixHilbert.Realization.Colligation.energy line 155
  16. theorem OAI.CrouzeixHilbert.Realization.Colligation.norm_a_le line 161
  17. theorem OAI.CrouzeixHilbert.Realization.Colligation.norm_b_le line 169
  18. theorem OAI.CrouzeixHilbert.Realization.Colligation.norm_c_le line 177
  19. theorem OAI.CrouzeixHilbert.Realization.Colligation.norm_d_le line 185
  20. def OAI.CrouzeixHilbert.Realization.Colligation.transfer line 193
  21. theorem OAI.CrouzeixHilbert.Realization.Colligation.one_sub_isUnit line 198
  22. theorem OAI.CrouzeixHilbert.Realization.Colligation.transfer_energy line 205
  23. theorem OAI.CrouzeixHilbert.Realization.Colligation.norm_transfer_le line 220
  24. theorem OAI.CrouzeixHilbert.Realization.exists_colligation_data line 234