OAI/Analysis/Crouzeix/Density.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Density.

  1. theorem OAI.CrouzeixHilbert.Boundary.eq_of_norm_le_inner line 21
  2. theorem OAI.CrouzeixHilbert.Boundary.adjoint_eq_of_contraction line 33
  3. theorem OAI.CrouzeixHilbert.Boundary.equality_in_compression line 46
  4. def OAI.CrouzeixHilbert.Boundary.crossPartialTrace line 67
  5. theorem OAI.CrouzeixHilbert.Boundary.crossPartialTrace_apply line 70
  6. theorem OAI.CrouzeixHilbert.Boundary.crossPartialTrace_conjTranspose line 78
  7. theorem OAI.CrouzeixHilbert.Boundary.crossPartialTrace_self_posSemidef line 86
  8. theorem OAI.CrouzeixHilbert.Boundary.crossPartialTrace_block_posSemidef line 90
  9. theorem OAI.CrouzeixHilbert.Boundary.crossPartialTrace_ordered line 102
  10. def OAI.CrouzeixHilbert.Boundary.weightedPartialTrace line 118
  11. theorem OAI.CrouzeixHilbert.Boundary.weightedPartialTrace_factor line 122
  12. theorem OAI.CrouzeixHilbert.Boundary.weightedPartialTrace_block_posSemidef line 128