OAI/NumberTheory/Ostmann/ZeroDensity/LogDerivativeDiskBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A logarithmic-derivative estimate from the actual modulus on a disk

  1. theorem OAI.Ostmann.logDeriv_norm_le_of_disk line 14
  2. theorem OAI.Ostmann.logDeriv_norm_le_inner_disk line 50

    Source documentation

    The same modulus information controls the logarithmic derivative throughout an inner half-disk, with the normalization still taken at its original center.

    theorem logDeriv_norm_le_inner_disk (g : ℂ → ℂ) (R A : ℝ) (hR : 0 < R) (hA : 0 < A)
    (hg : AnalyticOnNhd ℂ g (ball 0 R)) (hne : ∀ z ∈ ball 0 R, g z ≠ 0)
    (hlog : ∀ z ∈ ball 0 R, Real.log ‖g z‖ - Real.log ‖g 0‖ ≤ A)
    (w : ℂ) (hw : ‖w‖ ≤ R / 2) : ‖logDeriv g w‖ ≤ 24 * A / R := by
…