proximity_top — Mathlib

English

For a meromorphic function f, proximity f ⊤ measures how well f approximates infinity on large circles: proximity f ⊤ = circleAverage(log^+ ‖f‖)0.

Русский

Для мероморфной функции f близость f ⊤ измеряет, как хорошо f приближается к бесконечности на больших кругах: proximity f ⊤ = circleAverage(log^+ ‖f‖)0.

LaTeX

$$$\mathrm{proximity}(f,\top) = \operatorname{circleAverage}(\log^+ \|f\|)0$$$

Lean4

/-- Expand the definition of `proximity f a` in case where `a₀ = ⊤`.
-/
theorem proximity_top : proximity f ⊤ = circleAverage (log⁺ ‖f ·‖) 0 := by simp [proximity]

Похожие утверждения