OAI/Analysis/NumericalRange/ExteriorProjection.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompleteCrouzeix.analyticOnNhd_exteriorMap line 27
  2. def OAI.CompleteCrouzeix.actualExteriorKernel line 41
  3. lemma OAI.CompleteCrouzeix.interval_integral_swap_continuous line 82
  4. lemma OAI.CompleteCrouzeix.analytic_segment_integral line 92
  5. theorem OAI.CompleteCrouzeix.convex_closed_curve_remainder line 112
  6. theorem OAI.CompleteCrouzeix.convex_closed_curve_cauchy line 181
  7. def OAI.CompleteCrouzeix.reciprocalResolventDenom line 212
  8. def OAI.CompleteCrouzeix.reciprocalResolvent line 215
  9. lemma OAI.CompleteCrouzeix.reciprocalResolventDenom_ne_zero line 218
  10. lemma OAI.CompleteCrouzeix.reciprocalResolvent_analytic line 234
  11. lemma OAI.CompleteCrouzeix.reciprocalResolvent_eq line 243
  12. theorem OAI.CompleteCrouzeix.exterior_cauchy_kernel_integral line 255
  13. lemma OAI.CompleteCrouzeix.unitAddCircle_integral_eq_unitInterval line 272
  14. theorem OAI.CompleteCrouzeix.circle_convex_cauchy line 283
  15. lemma OAI.CompleteCrouzeix.actualExteriorKernel_circleB line 336
  16. theorem OAI.CompleteCrouzeix.actualExteriorCauchy_fix_trace line 357