English
Let f be meromorphic on the complex plane. Then the two value-distribution characteristic functions χ_f⊤ and χ_{f−a0}⊤ differ by a bounded amount as the radius tends to infinity; i.e., their difference is bounded along the atTop direction.
Русский
Пусть f мероморфна на комплексной плоскости. Тогда две функции характеристик распределения значений χ_f⊤ и χ_{f−a0}⊤ отличаются ограниченно при стремлении радиуса к бесконечности; т.е. разность ограничена вдоль направления atTop.
LaTeX
$$$(\chi_f^{\top} - \chi_{f - a_0}^{\top}) = O_{atTop}(1)$$$
Lean4
/-- Second part of the First Main Theorem of Value Distribution Theory, qualitative version: If `f` is
meromorphic on the complex plane, then the characteristic functions for the value `⊤` of the
function `f` and `f - a₀` agree asymptotically up to a bounded function.
-/
theorem isBigO_characteristic_sub_characteristic_shift (h : MeromorphicOn f ⊤) :
(characteristic f ⊤ - characteristic (f · - a₀) ⊤) =O[atTop] (1 : ℝ → ℝ) :=
isBigO_of_le' (c := log⁺ ‖a₀‖ + log 2) _ (fun R ↦ by simpa using abs_characteristic_sub_characteristic_shift_le h)
