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.

Preparatory Material

In preparation to the proof of Jensen's formula, compute several circle averages and reformulate some of the terms that appear in the formula and its proof.

theorem circleAverage_re_herglotzRieszKernel_mul_log₀ {w ρ : ℂ} {R : ℝ} (hρ : ρ ∈ Metric.sphere 0 R) (hw : w ∈ Metric.ball 0 R) : Real.circleAverage (Complex.re ∘ herglotzRieszKernel 0 w • fun (x : ℂ) => Real.log ‖x - ρ‖) 0 R = Real.log ‖w - ρ‖

theorem circleAverage_re_herglotzRieszKernel_mul_log {w ρ c : ℂ} {R : ℝ} (hρ : ρ ∈ Metric.sphere c R) (hw : w ∈ Metric.ball c R) : Real.circleAverage (Complex.re ∘ herglotzRieszKernel c w * fun (x : ℂ) => Real.log ‖x - ρ‖) c R = Real.log ‖w - ρ‖

Analogue of the Poisson Integral Formula for the circle average function log ‖· - ρ‖ along the circle with radius ‖ρ‖.

• See InnerProductSpace.HarmonicContOnCl.circleAverage_re_herglotzRieszKernel_smul in the file Mathlib/Analysis/Complex/Harmonic/Poisson for the classic Poisson Integral Formula, for harmonic functions without logarithmic poles.

• See MeromorphicOn.extract_zeros_poles in the file Mathlib/Analysis/Meromorphic/FactorizedRational for a construction that splits factors of the form · - ρ off arbitrary meromorphic functions.

@[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‖.

theorem countingFunction_finsum_eq_finsum_add {c : ℂ} {R : ℝ} {D : ℂ → ℤ} (hR : R ≠ 0) (hD : 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.

Jensen's Formula

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‖

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.

See Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const for a reformulation in terms of the logarithmic counting function of Value Distribution Theory.

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

Jensen's Formula specialized to the case that f is analytic and f c ≠ 0.

theorem AnalyticOnNhd.sum_divisor_le {c : ℂ} {r R M : ℝ} {f : ℂ → ℂ} (r_pos : 0 < |r|) (r_lt_R : |r| < |R|) (hM : 1 ≤ M) (h₁f : AnalyticOnNhd ℂ f (Metric.closedBall c |R|)) (h₂f : f c ≠ 0) (f_bound : ∀ z ∈ Metric.sphere c |R|, ‖f z‖ ≤ M) : ↑(∑ᶠ (u : ℂ), (MeromorphicOn.divisor f (Metric.closedBall c |r|)) u) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)

Jensen's Inequality: Estimates the number of zeros of f in a ball of radius r given that f is analytic and bounded by M on a larger ball of radius R.