OAI/Analysis/Crouzeix/Resolvent.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Resolvent.

  1. theorem OAI.CrouzeixHilbert.nonneg_re_inner_of_unit line 18
  2. theorem OAI.CrouzeixHilbert.isPositive_add_adjoint_of_unit line 35
  3. theorem OAI.CrouzeixHilbert.isPositive_supporting_halfplane line 49
  4. theorem OAI.CrouzeixHilbert.resolvent_hermitian_congruence line 59
  5. theorem OAI.CrouzeixHilbert.isPositive_original_resolvent line 78
  6. theorem OAI.CrouzeixHilbert.isPositive_original_resolvent_of_not_mem line 91
  7. theorem OAI.CrouzeixHilbert.isPositive_contraction_defect line 101
  8. theorem OAI.CrouzeixHilbert.disk_resolvent_congruence line 115
  9. def OAI.CrouzeixHilbert.diskDensity line 133
  10. theorem OAI.CrouzeixHilbert.isPositive_diskResolvent line 136
  11. theorem OAI.CrouzeixHilbert.isPositive_diskDensity line 147
  12. theorem OAI.CrouzeixHilbert.disk_resolvent_isUnit line 154
  13. theorem OAI.CrouzeixHilbert.isPositive_diskDensity_of_spectrum line 169