Complex.Hadamard.summable_norm_inv_rpow_divisorZeroIndex₀_of_growth

theorem summable_norm_inv_rpow_divisorZeroIndex₀_of_growth {f : ℂ → ℂ} {ρ τ : ℝ}    (hρ : 0 ≤ ρ) (hτ : ρ < τ) (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‖⁻¹ ^ τ) := by  rcases hgrowth with ⟨Cgrow, hCgrow_pos, hCgrow⟩  have hτpos : 0 < τ := lt_of_le_of_lt hρ hτ  rcases exists_r0_le_norm_divisorZeroIndex₀_val (f := f) hf hnot with ⟨r0, hr0pos, hr0⟩  have hr0ne : (r0 : ℝ) ≠ 0 := ne_of_gt hr0pos  let kfun : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℕ :=    fun p => ⌊Real.logb 2 (‖divisorZeroIndex₀_val p‖ / r0)⌋₊  let S : ℕ → Set (divisorZeroIndex₀ f (Set.univ : Set ℂ)) :=    fun k => {p | kfun p = k}  have hS : ∀ p : divisorZeroIndex₀ f (Set.univ : Set ℂ), ∃! k : ℕ, p ∈ S k := by    intro p    refine ⟨kfun p, ?_, ?_⟩    · simp [S]    · intro k hk      simpa [S] using hk.symm  have hnonneg : 0 ≤ fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ := by    intro p    exact Real.rpow_nonneg (inv_nonneg.2 (norm_nonneg _)) _  have hSk_summable : ∀ k : ℕ, Summable fun p : S k => ‖divisorZeroIndex₀_val p.1‖⁻¹ ^ τ := by    intro k    haveI : Finite (S k) := by      simpa [S, kfun] using (finite_divisorZeroIndex₀_dyadicShell        (f := f) hr0pos hr0 k).to_subtype    exact Summable.of_finite  have hshell_summable :      Summable fun k : ℕ => ∑' p : S k, ‖divisorZeroIndex₀_val p.1‖⁻¹ ^ τ := by    let q : ℝ := (2 : ℝ) ^ (ρ - τ)    let qσ : ℝ := (2 : ℝ) ^ (-τ)    have hq_nonneg : 0 ≤ q := le_of_lt (Real.rpow_pos_of_pos (by norm_num : (0 : ℝ) < 2) _)    have hq_lt_one : q < 1 :=      Real.rpow_lt_one_of_one_lt_of_neg (x := (2 : ℝ)) (by norm_num : (1 : ℝ) < 2)        (sub_neg.2 hτ)    have hqσ_nonneg : 0 ≤ qσ := le_of_lt (Real.rpow_pos_of_pos (by norm_num : (0 : ℝ) < 2) _)    have hqσ_lt_one : qσ < 1 :=      Real.rpow_lt_one_of_one_lt_of_neg (x := (2 : ℝ)) (by norm_num : (1 : ℝ) < 2)        (by simpa using (neg_neg_of_pos hτpos))    have hgeom_q : Summable (fun k : ℕ => q ^ k) :=      summable_geometric_of_lt_one hq_nonneg hq_lt_one    have hgeom_qσ : Summable (fun k : ℕ => qσ ^ k) :=      summable_geometric_of_lt_one hqσ_nonneg hqσ_lt_one    let Ctrail : ℝ := |Real.log ‖meromorphicTrailingCoeffAt f 0‖|    let A : ℝ := ((Cgrow / Real.log 2) * (1 + 4 * r0) ^ ρ) * (r0⁻¹) ^ τ    let B : ℝ := ((Ctrail / Real.log 2) + 1) * (r0⁻¹) ^ τ    rcases Real.exists_nat_le_two_pow (1 / r0) with ⟨k0, hk0⟩    let A0 : ℝ := A * q ^ k0    let B0 : ℝ := B * qσ ^ k0    have hmajor : Summable (fun k : ℕ => A0 * q ^ k + B0 * qσ ^ k) :=      (hgeom_q.mul_left A0).add (hgeom_qσ.mul_left B0)    have hshell_summable_shift :        Summable fun k : ℕ => ∑' p : S (k + k0), ‖divisorZeroIndex₀_val p.1‖⁻¹ ^ τ := by      refine hmajor.of_nonneg_of_le        (fun k => by          have : ∀ p : S (k + k0), 0 ≤ ‖divisorZeroIndex₀_val p.1‖⁻¹ ^ τ := by            intro p; exact Real.rpow_nonneg (inv_nonneg.2 (norm_nonneg _)) _          exact tsum_nonneg this)        (fun k => by          let kk : ℕ := k + k0          let Rk : ℝ := r0 * (2 : ℝ) ^ ((kk : ℝ) + 1)          have hRk_ge_one : (1 : ℝ) ≤ Rk := by            have hkk : k0 ≤ kk + 1 := by              simp [kk, Nat.add_assoc, Nat.add_comm]            simpa [Rk] using              Real.one_le_dyadicRadius_succ_of_inv_le_two_pow hr0pos hk0 hkk          have hmain :              (∑' p : S kk, ‖divisorZeroIndex₀_val p.1‖⁻¹ ^ τ) ≤ A * q ^ kk + B * qσ ^ kk := by            simpa [S, kfun, Ctrail, A, B, q, qσ] using              tsum_divisorZeroIndex₀_dyadicShell_inv_rpow_le_geometric_of_growth                (f := f) (ρ := ρ) (τ := τ) hρ hτpos hf hCgrow_pos hCgrow hr0pos hr0 kk hRk_ge_one          have : A * q ^ kk + B * qσ ^ kk = A0 * q ^ k + B0 * qσ ^ k := by            simpa [A0, B0, kk] using Real.two_geometric_shift_add A B q qσ k k0          simpa [kk] using (hmain.trans_eq this)        )    exact (summable_nat_add_iff k0).1 hshell_summable_shift  have hpart :=    (summable_partition (f := fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>        ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ) hnonneg (s := S) hS)  exact (hpart.2 ⟨hSk_summable, hshell_summable⟩)