truncation — Mathlib

English

A truncation of a real-valued function is a function that equals the function inside the interval (-A, A] and is zero outside.

Русский

ТраuncationReal — функция, совпадающая с f на интервале (-A,A] и нулевая вне его.

LaTeX

$$$$\text{truncation}(f,A)(x) = 1_{(-A,A]}(f(x)) \cdot f(x).$$$$

Lean4

/-- Truncating a real-valued function to the interval `(-A, A]`. -/
def truncation (f : α → ℝ) (A : ℝ) :=
  indicator (Set.Ioc (-A) A) id ∘ f

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