y — Mathlib · SciLib

English

Define y(D) as the convolution of w(D) with φ, i.e., y(D)=w(D) ⋆ φ.

Русский

Определим y(D) как свертку w(D) и φ, то есть y(D)=w(D) ⋆ φ.

LaTeX

$$y(D, x) = (w(D) ⋆ φ)(x)$$

Lean4

/-- An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces.
It is the convolution between a smooth function of integral `1` supported in the ball of radius `D`,
with the indicator function of the closed unit ball. Therefore, it is smooth, equal to `1` on the
ball of radius `1 - D`, with support equal to the ball of radius `1 + D`. -/
def y (D : ℝ) : E → ℝ :=
  w D ⋆[lsmul ℝ ℝ, μ] φ

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