OAI/Analysis/Crouzeix/ResolventBounds.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Resolvent Bounds.

  1. theorem OAI.CrouzeixHilbert.continuousOn_resolvent line 20
  2. def OAI.CrouzeixHilbert.SmoothContour.trace line 29
  3. theorem OAI.CrouzeixHilbert.SmoothContour.isCompact_trace line 31
  4. theorem OAI.CrouzeixHilbert.SmoothContour.trace_nonempty line 34
  5. def OAI.CrouzeixHilbert.contourKernel line 37
  6. theorem OAI.CrouzeixHilbert.continuousOn_contourKernel line 40
  7. theorem OAI.CrouzeixHilbert.contourEval_eq_kernel line 47
  8. theorem OAI.CrouzeixHilbert.intervalIntegrable_contourIntegrand line 53
  9. theorem OAI.CrouzeixHilbert.tendsto_contourEval line 64
  10. theorem OAI.CrouzeixHilbert.exists_contourEval_bound line 105
  11. theorem OAI.CrouzeixHilbert.contourEval_sub line 132
  12. def OAI.CrouzeixHilbert.tensorOperatorCLM line 142
  13. theorem OAI.CrouzeixHilbert.tensorOperatorCLM_apply line 171
  14. def OAI.CrouzeixHilbert.matrixEntryCLM line 174
  15. def OAI.CrouzeixHilbert.matrixContourEval line 180
  16. theorem OAI.CrouzeixHilbert.tendsto_matrixContourEval line 184
  17. theorem OAI.CrouzeixHilbert.supNorm_le_add_of_dist_le line 204
  18. theorem OAI.CrouzeixHilbert.abs_supNorm_sub_le_of_dist_le line 216
  19. theorem OAI.CrouzeixHilbert.tendsto_supNorm_of_uniform line 227
  20. theorem OAI.CrouzeixHilbert.contour_bound_of_polynomial_approximation line 243
  21. theorem OAI.CrouzeixHilbert.norm_inverse_le_of_inner_lower_bound line 272
  22. theorem OAI.CrouzeixHilbert.norm_resolvent_le_inv_infDist line 287