logCounting_add_const — Mathlib

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

Похожие утверждения