OAI/Analysis/Crouzeix/Amplification.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Amplification.

  1. def OAI.CrouzeixHilbert.amplificationMap line 22
  2. theorem OAI.CrouzeixHilbert.norm_amplificationMap line 27
  3. theorem OAI.CrouzeixHilbert.amplificationMap_tmul line 38
  4. def OAI.CrouzeixHilbert.conjugateOperator line 44
  5. theorem OAI.CrouzeixHilbert.conjugateOperator_apply line 48
  6. theorem OAI.CrouzeixHilbert.conjugateOperator_pow_apply line 52
  7. theorem OAI.CrouzeixHilbert.numericalRange_conjugateOperator line 56
  8. theorem OAI.CrouzeixHilbert.polynomialEval_conjugateOperator_apply line 66
  9. theorem OAI.CrouzeixHilbert.norm_polynomialEval_le_conjugateOperator line 83
  10. theorem OAI.CrouzeixHilbert.norm_polynomialEval_conjugateOperator line 93
  11. def OAI.CrouzeixHilbert.matrixAmplificationCoordinates line 103
  12. theorem OAI.CrouzeixHilbert.norm_matrixAmplificationCoordinates line 109
  13. theorem OAI.CrouzeixHilbert.matrixAmplificationCoordinates_tmul line 121
  14. theorem OAI.CrouzeixHilbert.matrixAmplificationCoordinates_tensorOperator line 128
  15. theorem OAI.CrouzeixHilbert.matrixAmplificationCoordinates_polynomialEval line 153
  16. theorem OAI.CrouzeixHilbert.norm_polynomialEval_eq_kronecker line 162
  17. def OAI.CrouzeixHilbert.FiniteMatrixPolynomialBound line 187
  18. theorem OAI.CrouzeixHilbert.finiteDimensional_polynomial_bound line 193
  19. theorem OAI.CrouzeixHilbert.polynomial_bound_of_finite_matrix_bound line 212