OAI/Analysis/DirectCrouzeix/HolomorphicReflection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectCrouzeix.Conformal.logModulusUpper line 31
  2. theorem OAI.DirectCrouzeix.Conformal.logModulusUpper_real line 34
  3. theorem OAI.DirectCrouzeix.Conformal.logModulusUpper_continuous line 37
  4. theorem OAI.DirectCrouzeix.Conformal.upperBall_convex line 62
  5. theorem OAI.DirectCrouzeix.Conformal.upperBall_half_radius line 65
  6. theorem OAI.DirectCrouzeix.Conformal.circleAverage_pos_upper line 74
  7. theorem OAI.DirectCrouzeix.Conformal.herglotz_deriv_im_pos line 90
  8. theorem OAI.DirectCrouzeix.Conformal.holomorphic_reflection_modulus line 137