English
The difference between the characteristic functions is Big-O of a bounded function; i.e., the difference is bounded up to a constant as R grows, demonstrating asymptotic agreement.
Русский
Разность характеристических функций имеет порядокBig-O по отношению к ограниченной функции; то есть она асимптотически согласуется с константой.
LaTeX
$$(characteristic f ⊤ - characteristic f^{-1} ⊤) =O[atTop] 1$$
Lean4
/-- Second part of the First Main Theorem of Value Distribution Theory, quantitative version: If `f` is
meromorphic on the complex plane, then the characteristic functions (for value `⊤`) of `f` and `f -
a₀` differ at most by `log⁺ ‖a₀‖ + log 2`.
-/
theorem abs_characteristic_sub_characteristic_shift_le {r : ℝ} (h : MeromorphicOn f ⊤) :
|characteristic f ⊤ r - characteristic (f · - a₀) ⊤ r| ≤ log⁺ ‖a₀‖ + log 2 :=
by
have h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r :=
circleIntegrable_posLog_norm_meromorphicOn (fun x a ↦ h x trivial)
have h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r :=
by
apply circleIntegrable_posLog_norm_meromorphicOn
apply MeromorphicOn.sub (fun x a => h x trivial) (MeromorphicOn.const a₀)
rw [← Pi.sub_apply, characteristic_sub_characteristic_eq_proximity_sub_proximity h]
simp only [proximity, reduceDIte, Pi.sub_apply, ← circleAverage_sub h₁f h₂f]
apply le_trans abs_circleAverage_le_circleAverage_abs
apply circleAverage_mono_on_of_le_circle
· apply (h₁f.sub h₂f).abs
· intro θ hθ
simp only [Pi.abs_apply, Pi.sub_apply]
by_cases h : 0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
·
simpa [abs_of_nonneg h, sub_le_iff_le_add, add_comm (log⁺ ‖a₀‖ + log 2), ← add_assoc] using
(posLog_norm_add_le (f θ - a₀) a₀)
· simp only [abs_of_nonpos (le_of_not_ge h), neg_sub, tsub_le_iff_right, add_comm (log⁺ ‖a₀‖ + log 2), ← add_assoc]
convert posLog_norm_add_le (-f θ) (a₀) using 2
· rw [← norm_neg]
abel_nf
· simp
