English
Define an auxiliary function w that depends on a real parameter D and a point x in E by scaling the bump u by D and translating the input. This w serves as a building block for partitions of unity in finite-dimensional real spaces.
Русский
Определим вспомогательную функцию w, зависящую от вещественного параметра D и точки x ∈ E, путем масштабирования-бум-функции u и сдвига входа. Эта w служит основой для разбиений на единицы в конечномерных реалиях.
LaTeX
$$$w(D,x)=\\left(\\int_E u(z)\\,dz\\right)^{-1} |D|^{-\\,\\operatorname{finrank}_{\\mathbb{R}} E} \\; u(D^{-1} x).$$$
Lean4
/-- An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces,
which is smooth, symmetric, with support equal to the ball of radius `D` and integral `1`. -/
def w (D : ℝ) (x : E) : ℝ :=
((∫ x : E, u x ∂μ) * |D| ^ finrank ℝ E)⁻¹ • u (D⁻¹ • x)
