Complex.Hadamard.finite_divisorZeroIndex₀_dyadicShell

lemma finite_divisorZeroIndex₀_dyadicShell    {f : ℂ → ℂ} {r0 : ℝ}    (hr0pos : 0 < r0)    (hr0 : ∀ p : divisorZeroIndex₀ f (Set.univ : Set ℂ), r0 ≤ ‖divisorZeroIndex₀_val p‖)    (k : ℕ) :    ({p : divisorZeroIndex₀ f (Set.univ : Set ℂ) |      ⌊Real.logb 2 (‖divisorZeroIndex₀_val p‖ / r0)⌋₊ = k} : Set _).Finite := by  have hsub :      {p : divisorZeroIndex₀ f (Set.univ : Set ℂ) |        ⌊Real.logb 2 (‖divisorZeroIndex₀_val p‖ / r0)⌋₊ = k} ⊆        {p : divisorZeroIndex₀ f (Set.univ : Set ℂ) |          ‖divisorZeroIndex₀_val p‖ ≤ r0 * (2 : ℝ) ^ ((k : ℝ) + 1)} := by    intro p hp    exact divisorZeroIndex₀_dyadicShell_upper_bound hr0pos hr0 hp  have hfin :      ({p : divisorZeroIndex₀ f (Set.univ : Set ℂ) |        ‖divisorZeroIndex₀_val p‖ ≤ r0 * (2 : ℝ) ^ ((k : ℝ) + 1)} : Set _).Finite := by    have :        Metric.closedBall (0 : ℂ) (r0 * (2 : ℝ) ^ ((k : ℝ) + 1)) ⊆          (Set.univ : Set ℂ) := by      simp    simpa using      (divisorZeroIndex₀_norm_le_finite (f := f) (U := (Set.univ : Set ℂ))        (B := r0 * (2 : ℝ) ^ ((k : ℝ) + 1)) this)  exact hfin.subset hsub