Theorems · Theorem · complex analysis

Function.FactorizedRational.log_norm_meromorphicTrailingCoeffAt

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {d : 𝕜 → ℤ} {x : 𝕜},
  Function.HasFiniteSupport d →
    Real.log ‖meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), (fun x => x - u) ^ d u) x‖ = ∑ᶠ (u : 𝕜), ↑(d u) * Real.log ‖x - u‖

Variant of meromorphicTrailingCoeffAt_factorizedRational: Compute log of the norm of the trailing coefficient. The convention that log 0 = 0 gives a closed formula easier than the one in meromorphicTrailingCoeffAt_factorizedRational.

Defined in

Mathlib.Analysis.Meromorphic.FactorizedRational

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedField