logCounting_sub_const — Mathlib

English

Adding a constant to a meromorphic function does not change the top-level logCounting.

Русский

Добавление константы к мероморфной функции не изменяет logCounting на верхнем уровне.

LaTeX

$$$\logCounting (f + a) \top = \logCounting f \top$$$

Lean4

/-- Special case of `logCounting_add_analyticOn`: Subtracting a constant does not change the counting
function counting poles.
-/
@[simp]
theorem logCounting_sub_const (hf : MeromorphicOn f univ) : logCounting (f - fun _ ↦ a₀) ⊤ = logCounting f ⊤ := by
  simpa [sub_eq_add_neg] using logCounting_add_const hf

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