The support of a normalized mollification lies in a thickening of the support

Let $g:\mathbb{C}\to\mathbb{R}$, let $\rho$ be a bump function centred at $0$ with outer radius $r$ and let $\rho_{\mathrm{n}}=\rho/\int\rho$. Then the closed support of $\rho_{\mathrm{n}}*g$ is contained in the closed $r$-thickening of the closed support of $g$.

Formalization Note For a bump function $\rho$ centred at $0$ (ContDiffBump (0 : ℂ)), $\rho_{\mathrm{n}}$ is ρ.normed volume, the multiple of $\rho$ with integral $1$; $\rho_{\mathrm{n}}*g$ is the convolution ρ.normed volume ⋆[lsmul ℝ ℝ, volume] g with respect to Lebesgue measure on $\mathbb{C}$. The outer radius is ρ.rOut, closed supports are tsupport, and the closed thickening is Metric.cthickening.