OAI/Analysis/Crouzeix/CompleteFinite.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Complete Finite.

  1. lemma OAI.CrouzeixHilbert.entrywiseHolomorphic_matrixPolynomial line 18
  2. lemma OAI.CrouzeixHilbert.matrixHolomorphicEval_matrixPolynomial line 26
  3. lemma OAI.CrouzeixHilbert.norm_tensorOperator_one_le line 40
  4. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.holomorphic_bound line 59
  5. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.polynomial_bound line 95
  6. theorem OAI.CrouzeixHilbert.finite_matrix_polynomial_bound line 104