OAI/Analysis/Crouzeix/MatrixContours.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Matrix Contours.

  1. def OAI.CrouzeixHilbert.tensorCoefficientCLM line 24
  2. theorem OAI.CrouzeixHilbert.tensorCoefficientCLM_apply line 53
  3. theorem OAI.CrouzeixHilbert.sum_tensorOperator_entries line 56
  4. theorem OAI.CrouzeixHilbert.matrixContourEval_eq_integral line 71
  5. def OAI.CrouzeixHilbert.SmoothContour.arcLength line 121
  6. theorem OAI.CrouzeixHilbert.SmoothContour.arcLength_nonneg line 124
  7. theorem OAI.CrouzeixHilbert.norm_matrixContourEval_le line 127
  8. theorem OAI.CrouzeixHilbert.matrixContourEval_sub line 173
  9. theorem OAI.CrouzeixHilbert.norm_matrixContourEval_sub_le line 188