Theorems · Theorem · complex analysis

ValueDistribution.characteristic_mul_zero_le

∀ {f₁ f₂ : ℂ → ℂ} {r : ℝ},
  1 ≤ r →
    Meromorphic f₁ →
      (∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤) →
        Meromorphic f₂ →
          (∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤) →
            ValueDistribution.characteristic (f₁ * f₂) 0 r ≤
              (ValueDistribution.characteristic f₁ 0 + ValueDistribution.characteristic f₂ 0) r

For 1 ≤ r, the characteristic function for the zeros of f * g is less than or equal to the sum of the characteristic functions for the zeros of f and g, respectively.

Defined in

Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Cited by

1 results in Mathlib

Foundations

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