OAI/Analysis/Mahler/InverseRadialRegularity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MahlerConformal.inverseRadiusRadialSlope line 9
2. theorem OAI.MahlerConformal.hasDerivAt_inverseRadius_radial line 14

   Source documentation

   The derivative in the outward radial direction, at a point of Omega.

   theorem hasDerivAt_inverseRadius_radial {u : ℂ} (hu : u ∈ Omega) :
       HasDerivAt (fun t : ℝ => Complex.normSq (inverseF ((t : ℂ)*u)))
         (inverseRadiusRadialSlope u) 1 := by
   …

   Mentions: OAI.MahlerConformal.Omega, OAI.MahlerConformal.inverseF, OAI.MahlerConformal.inverseRadiusRadialSlope

3. theorem OAI.MahlerConformal.inverseRadiusRadialSlope_pos line 31
4. lemma OAI.MahlerConformal.inverseRadiusRadialSlope_zero line 40
5. theorem OAI.MahlerConformal.inverseRadiusRadialSlope_nonneg line 43