OAI/Analysis/Crouzeix/RationalEvaluation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Holomorphic continuity, pole-free rational evaluation, and tensor norm bounds.

  1. theorem OAI.CrouzeixHilbert.EntrywiseHolomorphic.continuousOn line 20
  2. theorem OAI.CrouzeixHilbert.holomorphic_sup_attained line 28
  3. theorem OAI.CrouzeixHilbert.isUnit_polynomial_aeval line 35
  4. theorem OAI.CrouzeixHilbert.rational_denominators_isUnit line 44
  5. theorem OAI.CrouzeixHilbert.rational_holomorphic_neighborhood line 50
  6. theorem OAI.CrouzeixHilbert.rational_sup_attained line 72
  7. theorem OAI.CrouzeixHilbert.norm_tensorOperator_le line 79
  8. theorem OAI.CrouzeixHilbert.tensorOperator_zero_right line 94