Function.locallyFinsuppWithin.massClosedBall₀_divisor_le_of_log_growth

theorem massClosedBall₀_divisor_le_of_log_growth {f : ℂ → ℂ} {ρ C : ℝ}    (hf : Differentiable ℂ f)    (hC : ∀ z : ℂ, log (1 + ‖f z‖) ≤ C * (1 + ‖z‖) ^ ρ) {R : ℝ} (hR : 1 ≤ R) :    massClosedBall₀ (divisor f (Set.univ : Set ℂ)) R      ≤ (C * (1 + |2 * R|) ^ ρ + |log ‖meromorphicTrailingCoeffAt f 0‖|) / log 2 := by  have hR0 : 0 < R := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) hR  have hlog2pos : 0 < log 2 := log_pos (by norm_num : (1 : ℝ) < 2)  have hlow :      (log 2) * massClosedBall₀ (divisor f (Set.univ : Set ℂ)) R        ≤ logCounting (divisor f (Set.univ : Set ℂ)) (2 * R) :=    log_two_mul_massClosedBall₀_le_logCounting      (D := divisor f (Set.univ : Set ℂ))      (MeromorphicOn.AnalyticOnNhd.divisor_nonneg        (hf.differentiableOn.analyticOnNhd isOpen_univ)) hR  have hupp :      logCounting (divisor f (Set.univ : Set ℂ)) (2 * R)        ≤ C * (1 + |2 * R|) ^ ρ + |log ‖meromorphicTrailingCoeffAt f 0‖| := by    have h2R0 : 0 < 2 * R := by nlinarith [hR0]    simpa using logCounting_divisor_le_of_log_growth (f := f) (ρ := ρ) (C := C) hf hC      (R := 2 * R) h2R0  have hmul :      (log 2) * massClosedBall₀ (divisor f (Set.univ : Set ℂ)) R        ≤ C * (1 + |2 * R|) ^ ρ + |log ‖meromorphicTrailingCoeffAt f 0‖| :=    hlow.trans hupp  have hmul' :      massClosedBall₀ (divisor f (Set.univ : Set ℂ)) R * log 2        ≤ C * (1 + |2 * R|) ^ ρ + |log ‖meromorphicTrailingCoeffAt f 0‖| := by    simpa [mul_assoc, mul_left_comm, mul_comm] using hmul  exact (le_div_iff₀ hlog2pos).2 hmul'