cuspFunction — Mathlib

English

The cuspFunction h f is the composition of f with invQParam h, extended at 0 by a chosen limit.

Русский

CuspFunction h f есть композиция f с invQParam h, продолженная в 0 выбранным пределом.

LaTeX

$$cuspFunction : \mathbb{C} \to \mathbb{C} \\ cuspFunction(h, f)(q) = (f \circ invQParam(h))(q) with a specified value at q = 0$$

Lean4

/-- The function `q ↦ f (invQParam h q)`, extended by a non-canonical choice of limit at 0. -/
def cuspFunction : ℂ → ℂ :=
  update (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))

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