proximity_coe — Mathlib

English

Expand proximity on finite targets: proximity f a0 equals circleAverage(log^+ ‖f − a0‖^{-1})0 when a0 is finite.

Русский

Раскрываем определение близости для конечного значения: proximity f a0 = circleAverage(log^+ ‖f − a0‖^{-1})0, когда a0 конечно.

LaTeX

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

Lean4

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

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