Smoothness of the Gaussian density and distribution function

The real Gaussian density is smooth, including at zero variance where its chosen value is zero. For nonzero variance the native Gaussian cumulative distribution function is smooth as well. These results allow smooth composition with the Gaussian CDF, for example in classical option-pricing formulas. No smoothness is asserted for the CDF of a Dirac mass.

theorem TauCeti.Probability.contDiff_gaussianPDFReal (m : ℝ) (v : NNReal) {n : WithTop ℕ∞} : ContDiff ℝ n (ProbabilityTheory.gaussianPDFReal m v)

The Gaussian density is smooth in its sample variable, for every variance.

theorem TauCeti.Probability.contDiff_cdf_gaussianReal (m : ℝ) {v : NNReal} {n : ℕ∞} (hv : v ≠ 0) : ContDiff ℝ ↑n ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal m v))

A nondegenerate Gaussian CDF is smooth to every finite or infinite differentiability order.