OAI/Analysis/Crouzeix/DiskEndpoint.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Disk Endpoint.

  1. theorem OAI.CrouzeixHilbert.vectorization_smul line 20
  2. theorem OAI.CrouzeixHilbert.tensor_endpoint_of_matrix_endpoint line 32
  3. theorem OAI.CrouzeixHilbert.trace_gram_eq_norm_vectorization_sq line 40
  4. theorem OAI.CrouzeixHilbert.disk_endpoint_extremal line 45