Theorems · Theorem · complex analysis

ValueDistribution.characteristic_sub_characteristic_inv_le

∀ {f : ℂ → ℂ} {R : ℝ},
  Meromorphic f →
    |ValueDistribution.characteristic f ⊤ R - ValueDistribution.characteristic f⁻¹ ⊤ R| ≤
      max |Real.log ‖f 0‖| |Real.log ‖meromorphicTrailingCoeffAt f 0‖|

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.

Defined in

Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Cited by

1 results in Mathlib

Foundations

Depth 299 from the axioms · uses propext, Classical.choice, Quot.sound