characteristic_sub_characteristic_inv_le

English

A quantitative version: the absolute difference of characteristics is bounded by a constant depending on f, independent of R.

Русский

Количественная версия: абсолютная разность характеристик ограничена константой, зависящей от f и не зависящей от R.

LaTeX

$$$|\text{characteristic}(f) - \text{characteristic}(f^{-1})| \le C$ for some constant C$$

Lean4

/-- First part of the First Main Theorem, quantitative version: If `f` is meromorphic on the complex
plane, then the difference between the characteristic functions of `f` and `f⁻¹` is bounded by an
explicit constant.
-/
theorem characteristic_sub_characteristic_inv_le (hf : MeromorphicOn f Set.univ) :
    |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖| :=
  by
  by_cases h : R = 0
  · simp [h, characteristic_sub_characteristic_inv_at_zero hf]
  · simp [characteristic_sub_characteristic_inv_of_ne_zero hf h]

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