OAI/Analysis/NumericalRange/ConvexBarrier.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompleteCrouzeix.analytic_chart_rescale_avoid line 35
  2. def OAI.CompleteCrouzeix.LocalAnalyticBoundary line 88
  3. structure OAI.CompleteCrouzeix.DiskCoordinate line 93

    Also declared: ComparatorChallenges/StructuralCrouzeix.lean:25 (same declaration text).

  4. lemma OAI.CompleteCrouzeix.analytic_noncritical_set_open line 111
  5. theorem OAI.CompleteCrouzeix.analytic_domain_disk_coordinate line 117
  6. lemma OAI.CompleteCrouzeix.DiskCoordinate.closure_maps line 179
  7. lemma OAI.CompleteCrouzeix.DiskCoordinate.inverse_ball line 184
  8. lemma OAI.CompleteCrouzeix.DiskCoordinate.inverse_image_ball line 189
  9. lemma OAI.CompleteCrouzeix.DiskCoordinate.inverse_closed line 196
  10. lemma OAI.CompleteCrouzeix.DiskCoordinate.inverse_injective line 201
  11. lemma OAI.CompleteCrouzeix.DiskCoordinate.inverse_noncritical line 205
  12. lemma OAI.CompleteCrouzeix.DiskCoordinate.exists_inverse_radius line 217
  13. lemma OAI.CompleteCrouzeix.DiskCoordinate.inverse_base line 223
  14. lemma OAI.CompleteCrouzeix.DiskCoordinate.inverse_mem_domain_iff line 226
  15. lemma OAI.CompleteCrouzeix.DiskCoordinate.inverse_mem_closure_iff line 234
  16. lemma OAI.CompleteCrouzeix.DiskCoordinate.inverse_sphere_frontier line 242
  17. def OAI.CompleteCrouzeix.convexBarrier line 268
  18. lemma OAI.CompleteCrouzeix.convexBarrier_continuous line 272
  19. lemma OAI.CompleteCrouzeix.convexBarrier_quadratic_le line 277
  20. lemma OAI.CompleteCrouzeix.convexBarrier_exp_le line 283
  21. lemma OAI.CompleteCrouzeix.convexBarrier_convex line 290
  22. lemma OAI.CompleteCrouzeix.finite_strict_separators line 309
  23. lemma OAI.CompleteCrouzeix.separates_scaled_exp line 340
  24. theorem OAI.CompleteCrouzeix.exists_convex_barrier line 351
  25. lemma OAI.CompleteCrouzeix.convexBarrier_analytic line 406
  26. lemma OAI.CompleteCrouzeix.convexBarrier_sublevel_convex line 416
  27. lemma OAI.CompleteCrouzeix.convexBarrier_sublevel_open line 421
  28. lemma OAI.CompleteCrouzeix.convexBarrier_sublevel_bounded line 426
  29. lemma OAI.CompleteCrouzeix.convexOn_fderiv_support line 435
  30. lemma OAI.CompleteCrouzeix.convexBarrier_boundary_regular line 446
  31. lemma OAI.CompleteCrouzeix.convexOn_closure_sublevel line 456
  32. lemma OAI.CompleteCrouzeix.convexOn_frontier_sublevel line 478