Complex.Hadamard.tsum_divisorZeroIndex₀_dyadicShell_inv_rpow_le_geometric_of_growth

lemma tsum_divisorZeroIndex₀_dyadicShell_inv_rpow_le_geometric_of_growth    {f : ℂ → ℂ} {ρ τ r0 Cgrow : ℝ}    (hρ : 0 ≤ ρ) (hτpos : 0 < τ) (hf : Differentiable ℂ f)    (hCgrow_pos : 0 < Cgrow)    (hCgrow : ∀ z : ℂ, Real.log (1 + ‖f z‖) ≤ Cgrow * (1 + ‖z‖) ^ ρ)    (hr0pos : 0 < r0)    (hr0 : ∀ p : divisorZeroIndex₀ f (Set.univ : Set ℂ),      r0 ≤ ‖divisorZeroIndex₀_val p‖)    (k : ℕ) (hk_ge_one : 1 ≤ r0 * (2 : ℝ) ^ ((k : ℝ) + 1)) :    let kfun : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℕ :=      fun p => ⌊Real.logb 2 (‖divisorZeroIndex₀_val p‖ / r0)⌋₊    let S : Set (divisorZeroIndex₀ f (Set.univ : Set ℂ)) := {p | kfun p = k}    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⁻¹) ^ τ    let q : ℝ := (2 : ℝ) ^ (ρ - τ)    let qσ : ℝ := (2 : ℝ) ^ (-τ)    (∑' p : S, ‖divisorZeroIndex₀_val p.1‖⁻¹ ^ τ) ≤ A * q ^ k + B * qσ ^ k := by  classical  intro kfun S Ctrail A B q qσ  let rk : ℝ := r0 * (2 : ℝ) ^ (k : ℝ)  let Rk : ℝ := r0 * (2 : ℝ) ^ ((k : ℝ) + 1)  have hrk_pos : 0 < rk := mul_pos hr0pos (Real.rpow_pos_of_pos (by norm_num) _)  have hrk0 : 0 ≤ rk := le_of_lt hrk_pos  haveI : Finite S := by    simpa [S, kfun] using (finite_divisorZeroIndex₀_dyadicShell      (f := f) hr0pos hr0 k).to_subtype  haveI : Fintype S := Fintype.ofFinite S  have hk_upper : ∀ p : S, ‖divisorZeroIndex₀_val p.1‖ ≤ Rk := by    intro p    have hk' : kfun p.1 = k := p.2    simpa [Rk, kfun] using      divisorZeroIndex₀_dyadicShell_upper_bound (f := f) hr0pos hr0 hk'  have hk_lower : ∀ p : S, rk ≤ ‖divisorZeroIndex₀_val p.1‖ := by    intro p    have hk' : kfun p.1 = k := p.2    simpa [rk, kfun] using      divisorZeroIndex₀_dyadicShell_lower_bound (f := f) hr0pos hr0 hk'  have htsum_le :      (∑' p : S, ‖divisorZeroIndex₀_val p.1‖⁻¹ ^ τ)        ≤ (Fintype.card S : ℝ) * (rk⁻¹ ^ τ) := by    exact Real.tsum_inv_rpow_le_card_mul_of_lower_bound      (a := fun p : S => ‖divisorZeroIndex₀_val p.1‖)      hrk_pos hτpos (fun _ => norm_nonneg _) hk_lower  have hmass_le_growth :      divisorMassClosedBall₀ f Rk        ≤ (Cgrow * (1 + |2 * Rk|) ^ ρ + Ctrail) / (Real.log 2) := by    simpa [Ctrail, Rk] using      (divisorMassClosedBall₀_le_of_growth (f := f) (ρ := ρ) (C := Cgrow) hf hCgrow        (R := Rk) hk_ge_one)  have hcard_le_mass :      (Fintype.card S : ℝ) ≤ divisorMassClosedBall₀ f Rk := by    have hRk_pos : 0 < Rk := lt_of_lt_of_le (by norm_num) hk_ge_one    exact card_subtype_le_divisorMassClosedBall₀_of_norm_le (f := f) hf hRk_pos hk_upper  have htsum' :      (∑' p : S, ‖divisorZeroIndex₀_val p.1‖⁻¹ ^ τ)        ≤ ((Cgrow * (1 + |2 * Rk|) ^ ρ + Ctrail) / (Real.log 2)) * (rk⁻¹ ^ τ) := by    have hcard_le_growth :        (Fintype.card S : ℝ) ≤          (Cgrow * (1 + |2 * Rk|) ^ ρ + Ctrail) / (Real.log 2) :=      le_trans hcard_le_mass hmass_le_growth    exact le_trans htsum_le <|      mul_le_mul_of_nonneg_right hcard_le_growth (Real.rpow_nonneg (inv_nonneg.2 hrk0) τ)  have hpow_bound :      (1 + |2 * Rk|) ^ ρ ≤ (1 + 4 * r0) ^ ρ * ((2 : ℝ) ^ ρ) ^ k := by    simpa [Rk] using      Real.one_add_abs_two_mul_dyadicRadius_rpow_le (r0 := r0) (ρ := ρ) k hr0pos hρ  have hlog2pos : 0 < Real.log 2 := Real.log_pos (by norm_num : (1 : ℝ) < 2)  simpa [A, B, q, qσ, rk, Ctrail, mul_assoc, mul_left_comm, mul_comm] using    Real.dyadic_growth_mass_mul_inv_le_geometric      (C := Cgrow) (L := Real.log 2) (M := (1 + 4 * r0) ^ ρ)      (X := (1 + |2 * Rk|) ^ ρ)      (T := ∑' p : S, ‖divisorZeroIndex₀_val p.1‖⁻¹ ^ τ)      (Ctrail := Ctrail) (r0 := r0) (ρ := ρ) (τ := τ) (k := k)      hlog2pos hCgrow_pos.le hr0pos.le hpow_bound      (by simpa [rk] using htsum')