OAI/Analysis/NumericalRange/HerglotzReflection.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompleteCrouzeix.circleAverage_pos_at_I line 20
  2. def OAI.CompleteCrouzeix.herglotzExtension line 35
  3. lemma OAI.CompleteCrouzeix.analyticOnNhd_herglotzExtension line 38
  4. lemma OAI.CompleteCrouzeix.re_herglotzExtension line 44
  5. lemma OAI.CompleteCrouzeix.hasDerivAt_herglotzExtension_zero line 53
  6. lemma OAI.CompleteCrouzeix.im_deriv_herglotzExtension_zero line 72
  7. theorem OAI.CompleteCrouzeix.herglotz_oddBoundary_deriv_ne_zero line 87
  8. theorem OAI.CompleteCrouzeix.holomorphic_reflection_modulus line 115
  9. theorem OAI.CompleteCrouzeix.holomorphic_reflection_upperDisk line 156
  10. def OAI.CompleteCrouzeix.upperLogNorm line 196
  11. lemma OAI.CompleteCrouzeix.upperLogNorm_eventuallyEq line 199
  12. lemma OAI.CompleteCrouzeix.upperLogNorm_continuousOn line 204
  13. theorem OAI.CompleteCrouzeix.conformal_reflection_upperDisk line 234
  14. theorem OAI.CompleteCrouzeix.compact_local_injective_collar line 266
  15. theorem OAI.CompleteCrouzeix.analytic_compact_injective_collar line 294
  16. theorem OAI.CompleteCrouzeix.conformal_modulus_boundary line 310