OAI/Analysis/NumericalRange/BoundaryNormals.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompleteCrouzeix.invertedExterior_local_chart line 44
  2. lemma OAI.CompleteCrouzeix.barrier_interior_disk_coordinate line 81
  3. lemma OAI.CompleteCrouzeix.barrier_exterior_disk_coordinate line 96
  4. def OAI.CompleteCrouzeix.exteriorCorrection line 126
  5. lemma OAI.CompleteCrouzeix.analyticAt_dslope_self line 129
  6. lemma OAI.CompleteCrouzeix.analyticOnNhd_dslope line 134
  7. lemma OAI.CompleteCrouzeix.dslope_ne_zero_of_injOn line 139
  8. def OAI.CompleteCrouzeix.exteriorMap line 148

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

  9. lemma OAI.CompleteCrouzeix.reciprocal_simple_zero_laurent line 150
  10. structure OAI.CompleteCrouzeix.ExteriorCoordinate line 187

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

  11. lemma OAI.CompleteCrouzeix.exteriorCoordinate_of_disk_inversion line 202
  12. lemma OAI.CompleteCrouzeix.complex_real_decomposition line 299
  13. lemma OAI.CompleteCrouzeix.real_linear_normal line 309
  14. lemma OAI.CompleteCrouzeix.analytic_convex_boundary_normal line 319