toFun — Mathlib

English

The value of a bump at x is given by an explicit affine-rescaled base bump: f(x) = (some base bump).toFun( f.rOut / f.rIn ) ( f.rIn^{-1} • (x - c) ).

Русский

Значение всплеска в точке x задаётся явной формулой через основание: f(x) = someBase(...) ( ... ).

LaTeX

$$$ f.toFun(x) = (someContDiffBumpBase(E)).toFun\left( \frac{f.rOut}{f.rIn} \right)\left( f.rIn^{-1}\cdot (x-c) \right). $$$

Lean4

/-- The function defined by `f : ContDiffBump c`. Use automatic coercion to
function instead. -/
@[coe]
def toFun {c : E} (f : ContDiffBump c) : E → ℝ :=
  (someContDiffBumpBase E).toFun (f.rOut / f.rIn) ∘ fun x ↦ (f.rIn⁻¹ • (x - c))

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