English
If g is analytic without zero on a closed ball around c with radius R, then circleAverage(log ||g||) equals log ||g(c)||.
Русский
Если g аналитична без нуля на замкнутом шаре вокруг c с радиусом R, то circleAverage(лог ||g||) = лог ||g(c)||.
LaTeX
$$$\text{circleAverage}(\log \|g\|)\; c\; R = \log \|g(c)\|$$$
Lean4
/-- 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 circleAverage_log_norm_factorizedRational {R : ℝ} {c : ℂ}
(D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ) :
circleAverage (∑ᶠ u, (D u * log ‖· - u‖)) c R = ∑ᶠ u, D u * log R :=
by
have h := D.finiteSupport (isCompact_closedBall c |R|)
calc
circleAverage (∑ᶠ u, (D u * log ‖· - u‖)) c R
_ = circleAverage (∑ u ∈ h.toFinset, (D u * log ‖· - u‖)) c R :=
by
rw [finsum_eq_sum_of_support_subset]
intro u
contrapose
aesop
_ = ∑ i ∈ h.toFinset, circleAverage (fun x ↦ D i * log ‖x - i‖) c R :=
by
rw [circleAverage_sum]
intro u hu
apply IntervalIntegrable.const_mul
apply circleIntegrable_log_norm_meromorphicOn (f := (· - u))
apply (analyticOnNhd_id.sub analyticOnNhd_const).meromorphicOn
_ = ∑ u ∈ h.toFinset, D u * log R := by
apply Finset.sum_congr rfl
intro u hu
simp_rw [← smul_eq_mul, circleAverage_fun_smul]
congr
rw [circleAverage_log_norm_sub_const_of_mem_closedBall]
apply D.supportWithinDomain
simp_all
_ = ∑ᶠ u, D u * log R := by
rw [finsum_eq_sum_of_support_subset]
intro u
aesop
