Function.locallyFinsuppWithin.logCounting_divisor_le_of_log_growth

theorem logCounting_divisor_le_of_log_growth {f : ℂ → ℂ} {ρ C : ℝ} (hf : Differentiable ℂ f)    (hC : ∀ z : ℂ, log (1 + ‖f z‖) ≤ C * (1 + ‖z‖) ^ ρ) {R : ℝ} (hR0 : 0 < R) :    logCounting (divisor f (Set.univ : Set ℂ)) R      ≤ C * (1 + |R|) ^ ρ + |log ‖meromorphicTrailingCoeffAt f 0‖| := by  have hR : R ≠ 0 := ne_of_gt hR0  have hEq :=    logCounting_divisor_eq_circleAverage_sub_const_of_differentiable (f := f) hf hR  have hf_sphere : MeromorphicOn f (sphere (0 : ℂ) |R|) := by    intro z hz    exact (hf.analyticAt z).meromorphicAt  have hInt : CircleIntegrable (fun z : ℂ => log ‖f z‖) 0 R :=    MeromorphicOn.circleIntegrable_log_norm hf_sphere  have hbound_circle : ∀ z ∈ sphere (0 : ℂ) |R|,      log ‖f z‖ ≤ C * (1 + |R|) ^ ρ := by    intro z hz    exact log_norm_le_of_log_one_add_growth_on_sphere hC hz  have hCircleAvg_le :      circleAverage (fun z : ℂ => log ‖f z‖) 0 R ≤ C * (1 + |R|) ^ ρ :=    circleAverage_mono_on_of_le_circle (c := (0 : ℂ)) (R := R)      (f := fun z => log ‖f z‖) hInt hbound_circle  calc    logCounting (divisor f (Set.univ : Set ℂ)) R        = circleAverage (fun z : ℂ => log ‖f z‖) 0 R            - log ‖meromorphicTrailingCoeffAt f 0‖ := by            simpa [top_eq_univ] using hEq    _ ≤ circleAverage (fun z : ℂ => log ‖f z‖) 0 R          + |log ‖meromorphicTrailingCoeffAt f 0‖| := by          have :              -log ‖meromorphicTrailingCoeffAt f 0‖                ≤ |log ‖meromorphicTrailingCoeffAt f 0‖| :=            neg_le_abs (log ‖meromorphicTrailingCoeffAt f 0‖)          linarith    _ ≤ C * (1 + |R|) ^ ρ + |log ‖meromorphicTrailingCoeffAt f 0‖| := by          nlinarith [hCircleAvg_le]