VerticalRadius.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Vertical geometry of the actual inverse. The squared inverse radius has positive vertical derivative on the image of the upper half-disk.

def OAI.MahlerConformal.verticalRadiusSq line 13
lemma OAI.MahlerConformal.hasDerivAt_normSq line 15
lemma OAI.MahlerConformal.im_polar_mul_deriv_F line 24

theorem OAI.MahlerConformal.hasDerivAt_verticalRadiusSq line 37

Source documentation

Differentiation in the actual vertical coordinate of Omega.

theorem hasDerivAt_verticalRadiusSq {q ξ : ℝ} (hu : (q : ℂ)+ξ*I ∈ Omega) :
    HasDerivAt (verticalRadiusSq q)
      (2*(inverseF ((q : ℂ)+ξ*I)*deriv F (inverseF ((q : ℂ)+ξ*I))).im /
        ‖deriv F (inverseF ((q : ℂ)+ξ*I))‖^2) ξ := by
…

Mentions: OAI.MahlerConformal.Omega, OAI.MahlerConformal.verticalRadiusSq, OAI.MahlerConformal.inverseF, OAI.MahlerConformal.F

lemma OAI.MahlerConformal.Q_add_S_I line 58
theorem OAI.MahlerConformal.hasDerivAt_verticalRadiusSq_polar line 63
Source documentation
At each upper-semicircle image point, the inverse radius increases vertically. This is the inverse differential form of the vertical-speed identity.
```
theorem hasDerivAt_verticalRadiusSq_polar {r θ : ℝ} (hr : 0 < r) (hr1 : r < 1) :
    HasDerivAt (verticalRadiusSq (Q r θ))
      (2*B r θ/‖deriv F (polar r θ)‖^2) (S r θ) := by
…
```
Mentions: OAI.MahlerConformal.verticalRadiusSq, OAI.MahlerConformal.Q, OAI.MahlerConformal.B, OAI.MahlerConformal.F, OAI.MahlerConformal.polar, OAI.MahlerConformal.S
theorem OAI.MahlerConformal.verticalRadiusSq_polar line 74
theorem OAI.MahlerConformal.verticalRadiusSq_deriv_pos line 80