Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.summable_norm_inv_pow_divisorZeroIndex₀_of_growth

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Summability.lean:568 to 581

Source documentation

Natural-power form of the divisor summability theorem.

Exact Lean statement

theorem summable_norm_inv_pow_divisorZeroIndex₀_of_growth {f : ℂ → ℂ} {ρ : ℝ}
    (hρ : 0 ≤ ρ) (hf : Differentiable ℂ f) (hnot : ∃ z : ℂ, f z ≠ 0)
    (hgrowth : ∃ C > 0, ∀ z : ℂ, Real.log (1 + ‖f z‖) ≤ C * (1 + ‖z‖) ^ ρ) :
    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₀_of_growth {f : ℂ → ℂ} {ρ : ℝ}    (hρ : 0 ≤ ρ) (hf : Differentiable ℂ f) (hnot : ∃ z : ℂ, f z ≠ 0)    (hgrowth : ∃ C > 0, ∀ z : ℂ, Real.log (1 + ‖f z‖) ≤ C * (1 + ‖z‖) ^ ρ) :    Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (Nat.floor ρ + 1)) := by  have hτ : ρ < (Nat.floor ρ + 1 : ℝ) := by    simpa [Nat.cast_add, Nat.cast_one] using (Nat.lt_floor_add_one (a := ρ))  have hs :=    summable_norm_inv_rpow_divisorZeroIndex₀_of_growth (f := f) (ρ := ρ)      (τ := (Nat.floor ρ + 1 : ℝ)) hρ hτ hf hnot hgrowth  exact hs.congr fun p => by    have hcast : ((Nat.floor ρ : ℝ) + 1) = ((Nat.floor ρ + 1 : ℕ) : ℝ) := by      norm_num    rw [hcast, Real.rpow_natCast]