English
The difference between proximity for f in infinity and proximity for f⁻¹ in infinity is the circle average of log ‖f‖: proximity f ⊤ − proximity f⁻¹ ⊤ = circleAverage(log ‖f‖)0.
Русский
Разность между близостью f к бесконечности и близостью f⁻¹ к бесконечности равна среднему по окружности логарифму нормы f: proximity f ⊤ − proximity f⁻¹ ⊤ = circleAverage(log ‖f‖)0.
LaTeX
$$$\mathrm{proximity}(f,\top) - \mathrm{proximity}(f^{-1},\top) = \operatorname{circleAverage}(\log \|f\|)0$$$
Lean4
/-- For complex-valued `f`, the difference between `proximity f ⊤` and `proximity
f⁻¹ ⊤` is the circle average of `log ‖f ·‖`.
-/
theorem proximity_sub_proximity_inv_eq_circleAverage {f : ℂ → ℂ} (h₁f : MeromorphicOn f ⊤) :
proximity f ⊤ - proximity f⁻¹ ⊤ = circleAverage (log ‖f ·‖) 0 :=
by
ext R
simp only [proximity, ↓reduceDIte, Pi.inv_apply, norm_inv, Pi.sub_apply]
rw [← circleAverage_sub]
· simp_rw [← posLog_sub_posLog_inv, Pi.sub_def]
· apply circleIntegrable_posLog_norm_meromorphicOn (h₁f.mono_set (by tauto))
· simp_rw [← norm_inv]
apply circleIntegrable_posLog_norm_meromorphicOn (h₁f.inv.mono_set (by tauto))
