English
If g is analytic on univ and f is meromorphic, then logCounting(f+g) top = logCounting f top; analytic perturbations do not change pole counting.
Русский
Если g аналитична на всей плоскости, а f мероморфна, то logCounting(f+g) верх = logCounting f верх; аналитические возмущения не меняют подсчёт полюсов.
LaTeX
$$$\logCounting (f+g) \top = \logCounting f \top$$$
Lean4
/-- Special case of `logCounting_add_analyticOn`: Adding a constant does not change the counting
function counting poles.
-/
@[simp]
theorem logCounting_add_const (hf : MeromorphicOn f univ) : logCounting (f + fun _ ↦ a₀) ⊤ = logCounting f ⊤ := by
apply logCounting_add_analyticOn hf analyticOn_const