Source indexedlemma · leanprover/lean4:v4.32.0

Complex.summable_norm_weierstrassFactor_div_sub_one_of_summable_inv_pow

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/WeierstrassFactor.lean:383 to 392

Mathematical statement

Exact Lean statement

lemma summable_norm_weierstrassFactor_div_sub_one_of_summable_inv_pow {m : ℕ} {a : ℕ → ℂ}
    (h_sum : Summable (fun n : ℕ => ‖a n‖⁻¹ ^ (m + 1))) (h_nonzero : ∀ n, a n ≠ 0) (z : ℂ) :
    Summable (fun n : ℕ ↦ ‖weierstrassFactor m (z / a n) - 1‖)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma summable_norm_weierstrassFactor_div_sub_one_of_summable_inv_pow {m : ℕ} {a : ℕ → ℂ}    (h_sum : Summable (fun n : ℕ => ‖a n‖⁻¹ ^ (m + 1))) (h_nonzero : ∀ n, a n ≠ 0) (z : ℂ) :    Summable (fun n : ℕ ↦ ‖weierstrassFactor m (z / a n) - 1‖) := by  refine Summable.of_norm_bounded_eventually_nat    (summable_scaled_bound_of_summable_inv_pow h_sum ‖z‖ (norm_nonneg z)) ?_  filter_upwards    [eventually_le_norm_div_two_of_summable_inv_pow h_sum h_nonzero ‖z‖ (norm_nonneg z)]    with n hn  simpa [Real.norm_eq_abs, abs_of_nonneg (norm_nonneg _)] using    norm_weierstrassFactor_div_sub_one_le_pow_div (m := m) (a := a n) (z := z) hn