Gaussian integral representation of the norm
ProvedHlawkaGaussian.gauss_integral_scalinggaussianhlawka-schattensharp-constant
For in a finite-dimensional real inner product space , , where is the standard Gaussian measure on . The key analytic input for the Hlawka proof: it reduces the norm inequality to the one-dimensional case, bypassing the box-SOS method which is provably powerless at .
Preamble
import Mathlib open MeasureTheory ProbabilityTheory
Formal statement
theorem HlawkaGaussian.gauss_integral_scaling : ∀ {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (v : E), ∫ w, |inner (𝕜 := ℝ) v w| ∂(stdGaussian E) = ‖v‖ * ∫ s, |s| ∂(gaussianReal 0 1) := by sorrySource
Hlawka p=2 campaign (Gaussian route); standard Gaussian pushforward computation