Theorems · Theorem · complex analysis

ValueDistribution.characteristic_sum_top_le

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {α : Type u_2} (s : Finset α) (f : α → ℂ → E)
  {r : ℝ},
  (∀ a ∈ s, Meromorphic (f a)) →
    1 ≤ r →
      ValueDistribution.characteristic (∑ a ∈ s, f a) ⊤ r ≤
        (∑ a ∈ s, ValueDistribution.characteristic (f a) ⊤) r + Real.log ↑s.card

For 1 ≤ r, the characteristic function of a sum ∑ a, f a at ⊤ is less than or equal to the sum of the characteristic functions of f ·, plus log s.card.

Defined in

Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace