Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.EntireOfOrderAtMost.exists_log_growth

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Order.lean:107 to 116

Source documentation

A finite-order bound gives a logarithmic growth bound at any larger exponent.

Exact Lean statement

theorem exists_log_growth {ρ τ : ℝ} {f : ℂ → ℂ} (h : EntireOfOrderAtMost ρ f)
    (hτ : ρ < τ) (hτ_nonneg : 0 ≤ τ) :
    ∃ C' > 0, ∀ z : ℂ, Real.log (1 + ‖f z‖) ≤ C' * (1 + ‖z‖) ^ τ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem exists_log_growth {ρ τ : ℝ} {f : ℂ → ℂ} (h : EntireOfOrderAtMost ρ f)    (hτ : ρ < τ) (hτ_nonneg : 0 ≤ τ) :    ∃ C' > 0, ∀ z : ℂ, Real.log (1 + ‖f z‖) ≤ C' * (1 + ‖z‖) ^ τ := by  rcases h.exists_bound (sub_pos.2 hτ) with ⟨C, hCpos, hC⟩  have hnorm : ∀ z : ℂ, ‖f z‖ ≤ Real.exp (C * (1 + ‖z‖) ^ τ) := by    intro z    simpa [sub_add_cancel] using (hC z)  exact Real.log_growth_of_norm_le_exp_mul_rpow (f := f)    (r := fun z : ℂ => 1 + ‖z‖) hCpos hτ_nonneg    (fun z => by linarith [norm_nonneg z]) hnorm