Theorems · Theorem · complex analysis

ValueDistribution.characteristic_sub_characteristic_inv_of_ne_zero

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

Helper lemma for the first part of the First Main Theorem: Away from zero, the difference between the characteristic functions of f and f⁻¹ equals log ‖meromorphicTrailingCoeffAt f 0‖.

Defined in

Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Cited by

1 results in Mathlib

Foundations

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