OAI/Analysis/CircleDomains/Sobolev/HalfPlaneDerivativeBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The Schwarz derivative estimate for a map into the upper half-plane. It controls a boundary logarithm's derivative by its imaginary part, without requiring a bound on the real part.

  1. def OAI.CircleDomainRigidity.upperHalfPlaneFractional line 14
  2. lemma OAI.CircleDomainRigidity.upperHalfPlaneFractional_den line 16
  3. lemma OAI.CircleDomainRigidity.upperHalfPlaneFractional_norm_lt line 23
  4. lemma OAI.CircleDomainRigidity.upperHalfPlaneFractional_hasDerivAt line 33
  5. lemma OAI.CircleDomainRigidity.norm_sub_conj line 44
  6. lemma OAI.CircleDomainRigidity.norm_deriv_le_of_mapsTo_upper line 52