log_counting_zero_sub_logCounting_top

English

The absolute difference between the characteristic functions of f and f−1 is bounded by the maximum of |log‖f0‖| and |log‖meromorphicTrailingCoeffAt f 0‖|.

Русский

Модуль разности характеристических функций f и f−1 ограничен максимумом из модулей |log‖f0‖| и |log‖meromorphicTrailingCoeffAt f 0‖|.

LaTeX

$$|characteristic f ⊤ R - characteristic f−1 ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|$$

Lean4

/-- The counting function associated with the divisor of `f` is the difference between `logCounting f 0`
and `logCounting f ⊤`.
-/
theorem log_counting_zero_sub_logCounting_top {f : 𝕜 → E} :
    (divisor f univ).logCounting = logCounting f 0 - logCounting f ⊤ := by
  rw [← posPart_sub_negPart (divisor f univ), logCounting_zero, logCounting_top, map_sub]

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