proximity_zero

Mathlib.Analysis.Complex.ValueDistribution.ProximityFunction

URI: https://scilib.ai/kg/mathlib#ValueDistribution.proximity_zero

← MathLib Explorer

English

When a0 = 0, proximity f 0 equals circleAverage(log^+ ‖f‖^{-1})0.

Русский

Когда a0 = 0, proximity f 0 равно circleAverage(log^+ ‖f‖^{-1})0.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru