SmoothExistence

Let \(\nu\) be a bumpfunction.

TheoremSmoothExistence#

There exists a smooth (once differentiable would be enough), nonnegative “bumpfunction” \(\nu\), supported in \([1/2,2]\) with total mass one:

\[ \int_0^\infty \nu(x)\frac{dx}{x} = 1. \]
Proof

Same idea as Urysohn-type argument.

Lean

Formalized as SmoothExistence.

Sources
LeanSmoothExistence
Used by 1
Used byGenStrengthPNT

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.