Theorems · Theorem · complex analysis

countingFunction_finsum_eq_finsum_add

∀ {c : ℂ} {R : ℝ} {D : ℂ → ℤ},
  R ≠ 0 →
    Function.HasFiniteSupport D →
      ∑ᶠ (u : ℂ), ↑(D u) * (Real.log R - Real.log ‖c - u‖) =
        ∑ᶠ (u : ℂ), ↑(D u) * Real.log (R * ‖c - u‖⁻¹) + ↑(D c) * Real.log R

Reformulation of a finsum that appears in Jensen's formula and in the definition of the counting function of Value Distribution Theory, as discussed in Mathlib/Analysis/Complex/ValueDistribution/CountingFunction.lean.

Defined in

Mathlib.Analysis.Complex.JensenFormula

Cited by

1 results in Mathlib

Foundations

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