FiniteZeroLogDerivative.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Constant logarithmic derivative after removing a finite zero set

theorem OAI.Ostmann.finite_zero_quotient_logDeriv_constant line 16

Source documentation

The precise elementary finite-order consequence needed for a hypothetical finite set of completed-character zeros.

theorem finite_zero_quotient_logDeriv_constant (f g : ℂ → ℂ) (S : Finset ℂ)
    (hg : ∀ z, AnalyticAt ℂ g z) (hne : ∀ z, g z ≠ 0)
    (he : ∀ z, f z = finiteZeroPolynomial f S z * g z)
    (A : ℝ) (hA : 0 < A)
    (hf : ∀ (N : ℕ) (z : ℂ), ‖z‖ ≤ (N : ℝ) + 1 →
      Real.log ‖f z‖ ≤ A * ((N : ℝ) + 3) * (1 + Real.log ((N : ℝ) + 3))) :
    ∃ c : ℂ, ∀ z, logDeriv g z = c := by
…

Mentions: OAI.Ostmann.finiteZeroPolynomial