Theorems · Theorem · complex analysis

ValueDistribution.abs_characteristic_sub_characteristic_shift_le

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a₀ : E} {f : ℂ → E} {r : ℝ},
  Meromorphic f →
    |ValueDistribution.characteristic f ⊤ r - ValueDistribution.characteristic (fun x => f x - a₀) ⊤ r| ≤
      ‖a₀‖.posLog + Real.log 2

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.

Defined in

Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace