logCounting_add_analyticOn — Mathlib

English

Adding a constant to f does not change the logarithmic counting function on top.

Русский

Добавление константы к f не меняет логарифмический подсчёт на бесконечности.

LaTeX

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

Lean4

/-- Adding an analytic function does not change the counting function counting poles.
-/
theorem logCounting_add_analyticOn (hf : MeromorphicOn f univ) (hg : AnalyticOn 𝕜 g univ) :
    logCounting (f + g) ⊤ = logCounting f ⊤ :=
  by
  simp only [logCounting, ↓reduceDIte]
  rw [hf.negPart_divisor_add_of_analyticNhdOn_right (isOpen_univ.analyticOn_iff_analyticOnNhd.1 hg)]

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