Jensen's Formula of Complex Analysis

If a function g : ℂ → ℂ is analytic without zero on the closed ball with center c and radius R, then log ‖g ·‖ is harmonic, and the mean value theorem of harmonic functions asserts that the circle average circleAverage (log ‖g ·‖) c R equals log ‖g c‖. Note that g c equals meromorphicTrailingCoeffAt g c and see AnalyticOnNhd.circleAverage_log_norm_of_ne_zero for the precise statement.

Jensen's Formula, formulated in MeromorphicOn.circleAverage_log_norm below, generalizes this to the setting where g is merely meromorphic. In that case, the circleAverage (log ‖g ·‖) c R equals log ‖meromorphicTrailingCoeffAt g c‖ plus a correction term that accounts for the zeros and poles of g within the ball.

Circle Averages

In preparation to the proof of Jensen's formula, compute several circle averages.

@[simp]

theorem 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.

@[simp]

theorem AnalyticOnNhd.circleAverage_log_norm_of_ne_zero {R : ℝ} {c : ℂ} {g : ℂ → ℂ} (h₁g : AnalyticOnNhd ℂ g (Metric.closedBall c |R|)) (h₂g : ∀ u ∈ Metric.closedBall c |R|, g u ≠ 0) : Real.circleAverage (fun (x : ℂ) => Real.log ‖g x‖) c R = Real.log ‖g c‖

If g : ℂ → ℂ is analytic without zero on the closed ball with center c and radius R, then the circle average circleAverage (log ‖g ·‖) c R equals log ‖g c‖.

Jensen's Formula

Jensen's Formula: If f : ℂ → ℂ is meromorphic on the closed ball with center c and radius R, then the circleAverage (log ‖f ·‖) c R equals log ‖meromorphicTrailingCoeffAt f c‖ plus a correction term that accounts for the zeros and poles of f within the ball.

theorem MeromorphicOn.circleAverage_log_norm {c : ℂ} {R : ℝ} {f : ℂ → ℂ} (hR : R ≠ 0) (h₁f : MeromorphicOn f (Metric.closedBall c |R|)) : Real.circleAverage (fun (x : ℂ) => Real.log ‖f x‖) c R = ∑ᶠ (u : ℂ), ↑((divisor f (Metric.closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + ↑((divisor f (Metric.closedBall c |R|)) c) * Real.log R + Real.log ‖meromorphicTrailingCoeffAt f c‖