The Gauss measure and polar decomposition #
The density exp (-π ‖x‖ ^ 2) of the Gauss measure, the fact that it is a probability density on
a finite-dimensional real inner product space, and the radius of the ball of volume one. These are
the two normalizations Vaaler's cube-slicing theorem compares: Bombieri–Gubler's Lemma C.3.7 says
that the Gauss measure of a symmetric convex set never exceeds the volume of its intersection with
a product of balls of volume one, and the base case of that induction is a comparison, ray by ray,
of these two measures of total mass one.
Alongside them, the polar decomposition of an additive Haar measure as an integral over the unit
sphere, in the ℝ≥0∞-valued form the comparison needs.
Main definitions #
gaussDensity x = ENNReal.ofReal (exp (-π * ‖x‖ ^ 2)), the Gauss density, with the defining equationgaussDensity_def.unitVolumeRadius E, the radiusρfor which the ball of radiusρinEhas volume1.
Main results #
lintegral_eq_lintegral_sphereandlintegral_eq_lintegral_sphere': polar decomposition of an additive Haar measure, in product and iterated form.lintegral_gaussDensity_eq_one:∫⁻ x, exp (-π ‖x‖ ^ 2) = 1on a finite-dimensional real inner product space.volume_closedBall_unitVolumeRadius: the ball of radiusunitVolumeRadius Ehas volume1.
Implementation notes #
⚠ The Gaussian is normalized with π in the exponent precisely so that no constant survives.
∫_ℝ exp (-π t ^ 2) dt = 1, so the n-dimensional integral is 1 for every n by Fubini, and the
comparison in SliceBound.lean can cancel the sphere measure between the two total masses instead
of evaluating either radial integral. This is what makes Bombieri–Gubler's Remark C.3.6 — the
closed form ρ(n) = π ^ (-1/2) * Γ (n/2 + 1) ^ (1/n) — unnecessary: unitVolumeRadius is defined
by the normalization it is used for, and no Gamma function appears anywhere below.
⚠ Mathlib's polar decomposition is a measure-preserving homeomorphism, not an integral formula.
MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd identifies the Haar measure of
E \ {0} with μ.toSphere.prod (volumeIoiPow (n - 1)); the only integral formula built on it,
integral_fun_norm_addHaar, is for Bochner integrals of radial functions. The comparison below
integrates the indicator of a convex set, which is not radial, so the formula is proved here in the
raw ℝ≥0∞ form, with no hypothesis on the integrand at all.
References #
E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Remarks C.3.5 and C.3.6.
This is Layer 4.5 (infrastructure) of the ArithmeticHeights roadmap.
The Gauss density exp (-π ‖x‖ ^ 2), as an ℝ≥0∞-valued function. With π in the
exponent it is a probability density for every finite-dimensional real inner product space.
Equations
- gaussDensity x = ENNReal.ofReal (Real.exp (-Real.pi * ‖x‖ ^ 2))
Instances For
Polar decomposition of an additive Haar measure. Every ℝ≥0∞-valued integral against an
additive Haar measure is an integral over sphere 0 1 × Ioi 0, with the radial factor r ^ (n-1)
carried by MeasureTheory.Measure.volumeIoiPow. No measurability hypothesis is needed.
Polar decomposition, iterated form: the inner integral is over the ray.
The Gauss measure is a probability measure on a finite-dimensional real inner product space.
The radius ρ of the ball of volume 1: Bombieri–Gubler's ρ(n), defined by the
normalization it is used for rather than by its closed form.
Equations
- unitVolumeRadius E = (MeasureTheory.volume (Metric.ball 0 1)).toReal ^ (-(1 / ↑(Module.finrank ℝ E)))
Instances For
The ball of radius unitVolumeRadius E has volume one.