English
Let f be meromorphic on a closed ball centered at c with radius R ≠ 0. Then the circle average of log of the modulus of f over the circle C(c,R) equals the contributions from zeros and poles inside the ball plus the trailing coefficient at c: circleAverage(log ||f||)_{c,R} = sum over interior u of divisor(f, closedBall(c,|R|))_u · log(R · ||c−u||^−1) + divisor(f, closedBall(c|R|))_c · log R + log ||meromorphicTrailingCoeffAt f c||.
Русский
Пусть f мероморфна на замкнутом диске с центром в c и радиусом R ≠ 0. Тогда усреднение по окружности круга C(c,R) логарифма модуля f есть сумма вкладов нулей и полюсов внутри диска плюс члены, связанные с коэффициентом на centr: circleAverage(log ||f||)_{c,R} = ∑ᶠ_u divisor(f, closedBall(c,|R|))_u · log(R · ||c−u||^−1) + divisor(f, closedBall(c|R|))_c · log R + log ||meromorphicTrailingCoeffAt f c||.
LaTeX
$$$\\displaystyle \\operatorname{circleAverage}(\\log \\|f\\|)\\; c\\; R = \\sum^{\\mathsf{f}} u\\, \\operatorname{divisor} f\\; (\\text{closedBall } c |R|)\\; u \\, \\log\\bigl(R \\cdot \\|c - u\\|^{-1}\\bigr) \\\\ + \\operatorname{divisor} f\\; (\\text{closedBall } c |R|)\\; c \\, \\log R + \\log \\|\\operatorname{meromorphicTrailingCoeffAt} f c\\|.$$$
Lean4
theorem circleAverage_log_norm {c : ℂ} {R : ℝ} {f : ℂ → ℂ} (hR : R ≠ 0) (h₁f : MeromorphicOn f (closedBall c |R|)) :
circleAverage (log ‖f ·‖) c R =
∑ᶠ u, divisor f (closedBall c |R|) u * log (R * ‖c - u‖⁻¹) + divisor f (closedBall c |R|) c * log R +
log ‖meromorphicTrailingCoeffAt f c‖ :=
by
-- Shorthand notation to keep line size in check
let CB := closedBall c |R|
by_cases h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
· have h₃f :=
(divisor f CB).finiteSupport
(isCompact_closedBall c |R|)
-- Extract zeros & poles and compute
obtain ⟨g, h₁g, h₂g, h₃g⟩ := h₁f.extract_zeros_poles (by simp_all) h₃f
calc
circleAverage (log ‖f ·‖) c R
_ = circleAverage ((∑ᶠ u, (divisor f CB u * log ‖· - u‖)) + (log ‖g ·‖)) c R :=
by
have h₄g := extract_zeros_poles_log h₂g h₃g
rw [circleAverage_congr_codiscreteWithin (codiscreteWithin.mono sphere_subset_closedBall h₄g) hR]
_ = circleAverage (∑ᶠ u, (divisor f CB u * log ‖· - u‖)) c R + circleAverage (log ‖g ·‖) c R :=
(circleAverage_add (circleIntegrable_log_norm_factorizedRational (divisor f CB))
(circleIntegrable_log_norm_meromorphicOn (h₁g.mono sphere_subset_closedBall).meromorphicOn))
_ = ∑ᶠ u, divisor f CB u * log R + log ‖g c‖ := by
simp [h₁g]
rw [h₁g.circleAverage_log_norm_of_ne_zero]
exact fun u hu ↦ h₂g ⟨u, hu⟩
_ = ∑ᶠ u, divisor f CB u * log R + (log ‖meromorphicTrailingCoeffAt f c‖ - ∑ᶠ u, divisor f CB u * log ‖c - u‖) :=
by
have t₀ : c ∈ CB := by simp [CB]
have t₁ : AccPt c (𝓟 CB) := by
apply accPt_iff_frequently_nhdsNE.mpr
apply compl_notMem
apply mem_nhdsWithin.mpr
use ball c |R|
simpa [hR] using fun _ ⟨h, _⟩ ↦ ball_subset_closedBall h
simp [MeromorphicOn.log_norm_meromorphicTrailingCoeffAt_extract_zeros_poles h₃f t₀ t₁ (h₁f c t₀) (h₁g c t₀)
(h₂g ⟨c, t₀⟩) h₃g]
_ = ∑ᶠ u, divisor f CB u * log R - ∑ᶠ u, divisor f CB u * log ‖c - u‖ + log ‖meromorphicTrailingCoeffAt f c‖ := by
ring
_ = (∑ᶠ u, divisor f CB u * (log R - log ‖c - u‖)) + log ‖meromorphicTrailingCoeffAt f c‖ :=
by
rw [← finsum_sub_distrib]
· simp_rw [← mul_sub]
repeat apply h₃f.subset (fun _ ↦ (by simp_all))
_ = ∑ᶠ u, divisor f CB u * log (R * ‖c - u‖⁻¹) + divisor f CB c * log R + log ‖meromorphicTrailingCoeffAt f c‖ :=
by rw [Function.locallyFinsuppWithin.countingFunction_finsum_eq_finsum_add hR h₃f]
· -- Trivial case: `f` vanishes on a codiscrete set
have h₂f : ¬∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u ≠ ⊤ := by aesop
rw [←
h₁f.exists_meromorphicOrderAt_ne_top_iff_forall
⟨nonempty_closedBall.mpr (abs_nonneg R), (convex_closedBall c |R|).isPreconnected⟩] at h₂f
push_neg at h₂f
have : divisor f CB = 0 := by
ext x
by_cases h : x ∈ CB <;> simp_all [CB]
simp only [CB, this, Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, Int.cast_zero, zero_mul, finsum_zero,
add_zero, zero_add]
rw [MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top (by aesop), norm_zero, log_zero]
have : f =ᶠ[codiscreteWithin CB] 0 :=
by
filter_upwards [h₁f.meromorphicNFAt_mem_codiscreteWithin, self_mem_codiscreteWithin CB] with z h₁z h₂z
simpa [h₂f ⟨z, h₂z⟩] using (not_iff_not.2 h₁z.meromorphicOrderAt_eq_zero_iff)
rw [circleAverage_congr_codiscreteWithin (f₂ := 0) _ hR]
· simp only [circleAverage, mul_inv_rev, Pi.zero_apply, intervalIntegral.integral_zero, smul_eq_mul, mul_zero]
apply Filter.codiscreteWithin.mono (U := CB) sphere_subset_closedBall
filter_upwards [this] with z hz
simp_all
