isBigO_characteristic_sub_characteristic_inv

English

The absolute value of the difference between log counting for f and f−a0 is bounded by a function of a0, namely log⁺ ‖a0‖ + log 2.

Русский

Модуль разности между логарифмическими счетчиками f и f−a0 ограничен функцией от a0: log⁺ ‖a0‖ + log 2.

LaTeX

$$|characteristic f ⊤ r - characteristic (f − a0) ⊤ r| ≤ log⁺ ‖a0‖ + log 2$$

Lean4

/-- First part of the First Main Theorem, qualitative version: If `f` is meromorphic on the complex
plane, then the characteristic functions of `f` and `f⁻¹` agree asymptotically up to a bounded
function.
-/
theorem isBigO_characteristic_sub_characteristic_inv (h : MeromorphicOn f ⊤) :
    (characteristic f ⊤ - characteristic f⁻¹ ⊤) =O[atTop] (1 : ℝ → ℝ) :=
  isBigO_of_le' (c := max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|) _
    (fun R ↦ by simpa using characteristic_sub_characteristic_inv_le h (R := R))

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