Positivity of the Gaussian absolute first moment
ProvedHlawkaGaussian.gaussAbsConst_posgaussianhlawka-schattensharp-constant
The Gaussian absolute first moment is strictly positive. Proof by contradiction: if then is supported at , forcing its variance to , contradicting .
Preamble
import Mathlib open MeasureTheory ProbabilityTheory
Formal statement
theorem HlawkaGaussian.gaussAbsConst_pos : 0 < ∫ t, |t| ∂(gaussianReal 0 1) := by sorry
Source
Hlawka p=2 campaign (Gaussian route); standard Gaussian pushforward computation