English
expNegInvGlue is the real function defined by 0 for x ≤ 0 and e^{-1/x} for x > 0; it serves as a smooth glueing function.
Русский
expNegInvGlue — функция, заданная как 0 при x ≤ 0 и e^{-1/x} при x > 0; служит плавной склейкой.
LaTeX
$$$\expNegInvGlue(x) = \begin{cases}0,& x\le 0\\ e^{-1/x},& x>0\end{cases}$$$
Lean4
/-- `expNegInvGlue` is the real function given by `x ↦ exp (-1/x)` for `x > 0` and `0`
for `x ≤ 0`. It is a basic building block to construct smooth partitions of unity. Its main property
is that it vanishes for `x ≤ 0`, it is positive for `x > 0`, and the junction between the two
behaviors is flat enough to retain smoothness. The fact that this function is `C^∞` is proved in
`expNegInvGlue.contDiff`. -/
def expNegInvGlue (x : ℝ) : ℝ :=
if x ≤ 0 then 0 else exp (-x⁻¹)
