Theorems · Theorem · complex analysis

MeromorphicOn.logDeriv_finprod_zpow_eventuallyEq

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {U : Set 𝕜} {ι : Type u_3} {F : ι → 𝕜 → 𝕜'} {d : ι → ℤ},
  (Function.support d).Finite →
    (∀ (i : ι), MeromorphicOn (F i) U) →
      (∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤) →
        logDeriv (∏ᶠ (i : ι), F i ^ d i) =ᶠ[Filter.codiscreteWithin U] fun z => ∑ᶠ (i : ι), d i • logDeriv (F i) z

The logarithmic derivative converts products into sums: away from a codiscrete subset of U, the logarithmic derivative of a finite product of integer powers of meromorphic functions is the corresponding weighted sum of logarithmic derivatives. This is the shape of statement used in the differentiated Poisson–Jensen formula, where the exponents are given by a divisor.

Defined in

Mathlib.Analysis.Meromorphic.LogDeriv

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNontriviallyNormedFieldNormedAlgebra