Complex.Hadamard.sum_rpow_div_norm_divisorZeroIndex₀_le

lemma sum_rpow_div_norm_divisorZeroIndex₀_le    {f : ℂ → ℂ} {r τ : ℝ} (small : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)))    (hr : 0 ≤ r) (hτ_nonneg : 0 ≤ τ)    (hsumτ :      Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>        ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ)) :    (∑ p ∈ small, (r / ‖divisorZeroIndex₀_val p‖) ^ τ)      ≤ ((∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ),          ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ) + 1) * (1 + r) ^ τ := by  set Sτ : ℝ :=    ∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ), ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ  have hsum_inv :      (∑ p ∈ small, (‖divisorZeroIndex₀_val p‖⁻¹ : ℝ) ^ τ) ≤ Sτ := by    have hnn : ∀ p : divisorZeroIndex₀ f (Set.univ : Set ℂ),        0 ≤ (‖divisorZeroIndex₀_val p‖⁻¹ : ℝ) ^ τ := by      intro p      positivity    simpa [Sτ] using      (Summable.sum_le_tsum (s := small)        (f := fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>          (‖divisorZeroIndex₀_val p‖⁻¹ : ℝ) ^ τ)        (fun p _ => hnn p) hsumτ)  have hsum_eq :      ∑ p ∈ small, (r / ‖divisorZeroIndex₀_val p‖) ^ τ =        (r ^ τ) * ∑ p ∈ small, (‖divisorZeroIndex₀_val p‖⁻¹ : ℝ) ^ τ := by    simp [rpow_div_norm_divisorZeroIndex₀_eq (f := f) (τ := τ) hr, Finset.mul_sum]  have h1r : r ^ τ ≤ (1 + r) ^ τ :=    Real.rpow_le_rpow (by positivity) (by linarith) hτ_nonneg  have hS : (∑ p ∈ small, (‖divisorZeroIndex₀_val p‖⁻¹ : ℝ) ^ τ) ≤ Sτ + 1 := by    linarith [hsum_inv]  have hle :      (r ^ τ) * (∑ p ∈ small, (‖divisorZeroIndex₀_val p‖⁻¹ : ℝ) ^ τ)        ≤ (1 + r) ^ τ * (Sτ + 1) :=    mul_le_mul h1r hS (by positivity) (by positivity)  simpa [Sτ, hsum_eq, mul_assoc, mul_left_comm, mul_comm] using hle