Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.EntireOfOrderAtMost.summable_norm_inv_pow_divisorZeroIndex₀

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Order.lean:160 to 172

Source documentation

A nontrivial finite-order entire function has the summability needed for the genus ⌊ρ⌋ divisor canonical product.

Exact Lean statement

theorem summable_norm_inv_pow_divisorZeroIndex₀ {ρ : ℝ} {f : ℂ → ℂ}
    (h : EntireOfOrderAtMost ρ f) (hρ : 0 ≤ ρ) (hnot : ∃ z : ℂ, f z ≠ 0) :
    Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>
      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (Nat.floor ρ + 1))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem summable_norm_inv_pow_divisorZeroIndex₀ {ρ : ℝ} {f : ℂ → ℂ}    (h : EntireOfOrderAtMost ρ f) (hρ : 0 ≤ ρ) (hnot : ∃ z : ℂ, f z ≠ 0) :    Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (Nat.floor ρ + 1)) := by  rcases Real.exists_between_self_and_floor_add_one_same_floor hρ with    ⟨τ, hτ, _hτ_lt, hτ_nonneg, hfloorτ⟩  have hgrowthτ :      ∃ C' > 0, ∀ z : ℂ, Real.log (1 + ‖f z‖) ≤ C' * (1 + ‖z‖) ^ τ :=    h.exists_log_growth hτ hτ_nonneg  have hsummable :=    summable_norm_inv_pow_divisorZeroIndex₀_of_growth      (f := f) (ρ := τ) hτ_nonneg h.differentiable hnot hgrowthτ  simpa [hfloorτ] using hsummable