Source indexedlemma · leanprover/lean4:v4.32.0

Complex.Hadamard.tsum_rpow_div_norm_divisorZeroIndex₀_eq

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanMajorantBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanMajorantBound.lean:86 to 102

Mathematical statement

Exact Lean statement

lemma tsum_rpow_div_norm_divisorZeroIndex₀_eq
    {f : ℂ → ℂ} {r τ : ℝ} (hr : 0 ≤ r) :
    (∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ),
        (r / ‖divisorZeroIndex₀_val p‖) ^ τ)
      = (r ^ τ) * ∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ),
          ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma tsum_rpow_div_norm_divisorZeroIndex₀_eq    {f : ℂ → ℂ} {r τ : ℝ} (hr : 0 ≤ r) :    (∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ),        (r / ‖divisorZeroIndex₀_val p‖) ^ τ)      = (r ^ τ) * ∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ),          ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ := by  calc    (∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ),        (r / ‖divisorZeroIndex₀_val p‖) ^ τ)        = ∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ),            (r ^ τ) * (‖divisorZeroIndex₀_val p‖⁻¹ : ℝ) ^ τ := by            refine tsum_congr ?_            intro p            exact rpow_div_norm_divisorZeroIndex₀_eq (f := f) (τ := τ) hr p    _ = (r ^ τ) * ∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ),          ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ := by        simp [tsum_mul_left]