Complex.Hadamard.tsum_two_mul_rpow_div_norm_divisorZeroIndex₀_le

lemma tsum_two_mul_rpow_div_norm_divisorZeroIndex₀_le    {f : ℂ → ℂ} {r τ : ℝ} (hr : 0 ≤ r) (hτ_nonneg : 0 ≤ τ) :    (∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ),        (2 : ℝ) * (r / ‖divisorZeroIndex₀_val p‖) ^ τ)      ≤ (2 : ℝ) * ((∑' 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 htsum :      (∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ),          (2 : ℝ) * (r / ‖divisorZeroIndex₀_val p‖) ^ τ)        = (2 : ℝ) * (r ^ τ) * Sτ := by    calc      (∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ),          (2 : ℝ) * (r / ‖divisorZeroIndex₀_val p‖) ^ τ)          = (2 : ℝ) * ∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ),              (r / ‖divisorZeroIndex₀_val p‖) ^ τ := by              simp [tsum_mul_left]      _ = (2 : ℝ) * ((r ^ τ) * Sτ) := by              rw [tsum_rpow_div_norm_divisorZeroIndex₀_eq (f := f) (τ := τ) hr]      _ = (2 : ℝ) * (r ^ τ) * Sτ := by ring  have hSτ_nonneg : 0 ≤ Sτ :=    tsum_nonneg (fun _ => Real.rpow_nonneg (inv_nonneg.2 (norm_nonneg _)) _)  have h1r : r ^ τ ≤ (1 + r) ^ τ :=    Real.rpow_le_rpow (by positivity) (by linarith) hτ_nonneg  have hS : Sτ ≤ Sτ + 1 := by linarith  have hle : (r ^ τ) * Sτ ≤ (1 + r) ^ τ * (Sτ + 1) :=    mul_le_mul h1r hS (by linarith) (by positivity)  rw [htsum]  have : (2 : ℝ) * (r ^ τ) * Sτ ≤ (2 : ℝ) * (Sτ + 1) * (1 + r) ^ τ := by    nlinarith [hle]  simpa [Sτ, mul_assoc, mul_left_comm, mul_comm] using this