Theorems · Theorem · complex analysis

circleAverage_log_norm_factorizedRational

∀ {R : ℝ} {c : ℂ} (D : Function.locallyFinsuppWithin (Metric.closedBall c |R|) ℤ),
  Real.circleAverage (∑ᶠ (u : ℂ), fun x => ↑(D u) * Real.log ‖x - u‖) c R = ∑ᶠ (u : ℂ), ↑(D u) * Real.log R

Let D : ℂ → ℤ be a function with locally finite support within the closed ball with center c and radius R, such as the zero- and pole divisor of a meromorphic function. Then, the circle average of the function ∑ᶠ u, (D u * log ‖· - u‖) over the boundary of the ball equals ∑ᶠ u, D u * log R.

Defined in

Mathlib.Analysis.Complex.JensenFormula

Cited by

1 results in Mathlib

Foundations

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