The Gauss measure of a star-shaped set and the ball of volume one

Let E be a finite-dimensional real inner product space. The Gauss density exp (-π ‖x‖ ^ 2) and the indicator of the closed ball B of volume one both have total mass one. This file proves that the Gauss measure of a measurable set A that is star-shaped about the origin (for instance a convex set symmetric about the origin) is at most the volume of A ∩ B:

∫⁻ x in A, exp (-π ‖x‖ ^ 2) ≤ volume (A ∩ B).

This is the case of a single block in Bombieri–Gubler's Lemma C.3.7, which bounds the Gauss measure of a convex symmetric set by its volume inside a product of balls of volume one. That lemma is the analytic input to Vaaler's cube-slicing theorem: every k-dimensional central slice of the cube [-1, 1] ^ n has k-dimensional volume at least 2 ^ k.

The comparison is made ray by ray, in polar coordinates. A set that is star-shaped about the origin meets each ray from the origin in an initial segment. Either that segment contains the segment of the ray inside B, or it is contained in it, and the two cases need only exp (-π r ^ 2) ≤ 1 and comparison of the two radial integrals. This comparison follows from comparison of the two total masses, since the radial integrals do not depend on the direction of the ray. So the argument works for any radial density φ (‖x‖) with φ r ≤ 1 for r > 0, against any closed ball of at least the same total mass, and for any additive Haar measure; the general statement is TauCeti.setLIntegral_comp_norm_le_measure_inter_closedBall.

With the factor π in the exponent the Gauss density has total mass one in every dimension, so no Gamma function and no closed form for the radius of the ball of volume one is needed.

Main results

• TauCeti.setLIntegral_comp_norm_le_measure_inter_closedBall: for a radial density bounded by one away from the origin whose total mass is at most the measure of a closed ball, its integral over a measurable set star-shaped about the origin is at most the measure of the set inside the ball.
• TauCeti.lintegral_ofReal_exp_neg_pi_mul_sq_norm: the Gauss density exp (-π ‖x‖ ^ 2) has total mass one.
• TauCeti.setLIntegral_ofReal_exp_neg_pi_mul_sq_norm_le_volume_inter_closedBall: the Gauss measure of a measurable set star-shaped about the origin is at most its volume inside a closed ball of volume at least one.

References

• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Lemma C.3.7 and Remarks C.3.5, C.3.6.
• J. D. Vaaler, A geometric inequality with applications to linear forms, Pacific J. Math. 83 (1979), 543–553.

The ray-by-ray argument and the normalization of the Gauss density are adapted from the Apache-2.0 formalization of Vaaler's theorem in rwst/Subspace-Theorems (files ArithmeticHeights/GaussMeasure.lean and ArithmeticHeights/SliceBound.lean), by Ralf Stephan.

theorem TauCeti.setLIntegral_comp_norm_le_measure_inter_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {φ : ℝ → ENNReal} (hφm : Measurable φ) (hφ : ∀ r ∈ Set.Ioi 0, φ r ≤ 1) {ρ : ℝ} (hmass : ∫⁻ (x : E), φ ‖x‖ ∂μ ≤ μ (Metric.closedBall 0 ρ)) {A : Set E} (hA : MeasurableSet A) (hA₀ : StarConvex ℝ 0 A) : ∫⁻ (x : E) in A, φ ‖x‖ ∂μ ≤ μ (A ∩ Metric.closedBall 0 ρ)

The Gauss measure against a ball, for radial densities. Let μ be an additive Haar measure on a finite-dimensional real normed space, and φ : ℝ → ℝ≥0∞ a measurable function bounded by 1 at positive radii such that the radial density φ ‖x‖ has total mass at most that of the closed ball closedBall 0 ρ. Then for every measurable set A that is star-shaped about the origin, the mass of φ ‖x‖ on A is at most μ (A ∩ closedBall 0 ρ).

With φ r = exp (-π r ^ 2) and μ the volume of an inner product space this is the case of a single block in Bombieri–Gubler's Lemma C.3.7; see TauCeti.setLIntegral_ofReal_exp_neg_pi_mul_sq_norm_le_volume_inter_closedBall.

theorem TauCeti.lintegral_ofReal_exp_neg_pi_mul_sq_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : ∫⁻ (x : E), ENNReal.ofReal (Real.exp (-Real.pi * ‖x‖ ^ 2)) = 1

The Gauss measure is a probability measure. On a finite-dimensional real inner product space the density exp (-π ‖x‖ ^ 2) has total mass one.

theorem TauCeti.setLIntegral_ofReal_exp_neg_pi_mul_sq_norm_le_volume_inter_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ρ : ℝ} (hρ : 1 ≤ MeasureTheory.volume (Metric.closedBall 0 ρ)) {A : Set E} (hA : MeasurableSet A) (hA₀ : StarConvex ℝ 0 A) : ∫⁻ (x : E) in A, ENNReal.ofReal (Real.exp (-Real.pi * ‖x‖ ^ 2)) ≤ MeasureTheory.volume (A ∩ Metric.closedBall 0 ρ)

The Gauss measure of a star-shaped set is at most its volume inside a ball of volume at least one (Bombieri–Gubler, Lemma C.3.7, for a single ball of volume one). On a finite-dimensional real inner product space, let closedBall 0 ρ have volume at least one. Then for every measurable set A that is star-shaped about the origin, in particular for every measurable convex set symmetric about the origin,

∫⁻ x in A, exp (-π ‖x‖ ^ 2) ≤ volume (A ∩ closedBall 0 ρ).

Such a radius ρ exists by TauCeti.exists_volume_closedBall_eq_one.