proximity_zero_of_complexValued — Mathlib

English

For complex-valued f, proximity at zero is given by circleAverage(log^+ ‖f⁻¹ ‖)0, i.e., using the inverse values.

Русский

Для комплекснозначной f близость в нуле задается как circleAverage(log^+ ‖f⁻¹‖)0, то есть через обратные значения.

LaTeX

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

Lean4

/-- For complex-valued functions, expand the definition of `proximity f a₀` in case where `a₀` is zero.
This is a simple variant of `proximity_zero` defined above.
-/
theorem proximity_zero_of_complexValued {f : ℂ → ℂ} : proximity f 0 = circleAverage (log⁺ ‖f⁻¹ ·‖) 0 := by
  simp [proximity]

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