The Gauss measure of a symmetric convex set is at most its volume inside a product of balls

Bombieri–Gubler, Lemma C.3.7. Let Q be a product of euclidean balls each of volume one, one factor per block of a partition of the coordinates. Then for every measurable convex symmetric A, the Gauss measure of A is at most vol (A ∩ Q). This is the inequality Vaaler's cube-slicing theorem is extracted from by an ε-thickening.

The predicate HasSliceBound μ g Q states the conclusion for a measure μ, a density g and a set Q, in the form that both makes the induction on the number of blocks a Measure.prod statement and makes the base case a one-dimensional comparison along rays.

Main definitions

• HasSliceBound μ g Q: for every measurable convex symmetric A, ∫⁻ x in A, g x ∂μ ≤ μ (A ∩ Q).

Main results

• HasSliceBound.lintegral_le: the bound upgrades from sets to even log-concave functions, by the layer cake.
• hasSliceBound_unitVolumeBall: the base case, r = 1, for the ball of volume one.
• HasSliceBound.prod: the induction step, the case of a product of two blocks.
• HasSliceBound.of_measurePreserving: transport along a measure-preserving linear equivalence.

Implementation notes

⚠ The base case needs no Gamma function and no closed form for the radius. Polar decomposition turns both sides into integrals over the unit sphere; on each ray, a symmetric convex set meets the ray in an interval, so either the ray's segment of the volume-one ball lies in A or the reverse, and the two cases need only exp (-π r ^ 2) ≤ 1 and the equality of the two radial integrals. That equality is forced by the two normalizations — the Gauss measure and the ball both have total mass one — once the sphere measure, a positive finite constant, is cancelled. This is why Bombieri–Gubler's Remark C.3.6 does not appear.

⚠ The induction step needs the bound twice, in both factors, because slices of a symmetric set are not symmetric. A_y = {z | (y, z) ∈ A} satisfies A_{-y} = -A_y, not A_y = -A_y, so the bound cannot be applied slice by slice. Bombieri–Gubler's remedy, followed here, is to apply the upgraded form HasSliceBound.lintegral_le once in each factor, with the layer cake of the first density in between: the superlevel sets of a log-concave even density are convex and symmetric, and the marginals over them are log-concave by Lemma C.3.4 and even because the density is.

⚠ Closedness of A is not needed, only convexity, symmetry and measurability. Bombieri–Gubler ask for a closed symmetric convex set, and their approximation argument in the induction step needs closedness to know the superlevel sets are closed. The layer cake used here replaces that argument, and the superlevel sets of a log-concave function are convex whether or not they are closed, so the hypothesis disappears. It is worth having: in the induction step the sets the bound is applied to are superlevel sets of a marginal, whose closedness would be an upper semicontinuity question.

References

E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Lemma C.3.7.

This is Layer 4.5 (infrastructure) of the ArithmeticHeights roadmap.

def HasSliceBound {E : Type u_1} [MeasurableSpace E] [AddCommGroup E] [Module ℝ E] (μ : MeasureTheory.Measure E) (g : E → ENNReal) (Q : Set E) : Prop

HasSliceBound μ g Q says that the measure with density g of a measurable convex symmetric set A never exceeds μ (A ∩ Q). With g the Gauss density and Q a product of balls of volume one this is Bombieri–Gubler's Lemma C.3.7.

Equations

• HasSliceBound μ g Q = ∀ (A : Set E), MeasurableSet A → Convex ℝ A → (∀ x ∈ A, -x ∈ A) → ∫⁻ (x : E) in A, g x ∂μ ≤ μ (A ∩ Q)

theorem Set.neg_eq_self_of_neg_mem {G : Type u_3} [InvolutiveNeg G] {A : Set G} (h : ∀ x ∈ A, -x ∈ A) : -A = A

A set closed under negation equals its own negation.

theorem HasSliceBound.lintegral_le {E : Type u_1} [MeasurableSpace E] [AddCommGroup E] [Module ℝ E] {μ : MeasureTheory.Measure E} [MeasureTheory.SFinite μ] {g : E → ENNReal} {Q : Set E} (hb : HasSliceBound μ g Q) (hg : Measurable g) {f : E → ENNReal} (hf : Measurable f) (hfe : ∀ (x : E), f (-x) = f x) (hflc : LogConcave f) : ∫⁻ (x : E), f x * g x ∂μ ≤ ∫⁻ (x : E) in Q, f x ∂μ

The slice bound upgrades from sets to even log-concave functions. Writing f as a superposition of the indicators of its superlevel sets — which are convex because f is log-concave and symmetric because f is even — turns the bound for sets into a bound for integrals.

theorem hasSliceBound_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {ρ : ℝ} (hρ : 0 < ρ) (hball : μ (Metric.closedBall 0 ρ) = 1) (hgauss : ∫⁻ (x : E), gaussDensity x ∂μ = 1) : HasSliceBound μ gaussDensity (Metric.closedBall 0 ρ)

The base case of Bombieri–Gubler's Lemma C.3.7, stated for an arbitrary norm: if the Gauss density has total mass one and the closed ball of radius ρ has measure one, then the Gauss measure of a measurable convex symmetric set is at most its measure inside that ball.

theorem hasSliceBound_unitVolumeBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] : HasSliceBound MeasureTheory.volume gaussDensity (Metric.closedBall 0 (unitVolumeRadius E))

Bombieri–Gubler's Lemma C.3.7 for a single block: the Gauss measure of a measurable convex symmetric set is at most its volume inside the ball of volume one.

theorem HasSliceBound.prod {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [AddCommGroup E] [Module ℝ E] [MeasurableNeg E] [MeasurableSpace F] [AddCommGroup F] [Module ℝ F] [MeasurableNeg F] {μ : MeasureTheory.Measure E} {ν : MeasureTheory.Measure F} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [μ.IsNegInvariant] [ν.IsNegInvariant] {g : E → ENNReal} {h : F → ENNReal} {Q : Set E} {R : Set F} (hg : Measurable g) (hge : ∀ (x : E), g (-x) = g x) (hglc : LogConcave g) (hh : Measurable h) (hR : MeasurableSet R) (hRc : Convex ℝ R) (hRs : ∀ z ∈ R, -z ∈ R) (hPLμ : HasPrekopaLeindler μ) (hPLν : HasPrekopaLeindler ν) (hE : HasSliceBound μ g Q) (hF : HasSliceBound ν h R) : HasSliceBound (μ.prod ν) (fun (p : E × F) => g p.1 * h p.2) (Q ×ˢ R)

The induction step of Bombieri–Gubler's Lemma C.3.7. If the slice bound holds in each factor, for densities that are log-concave and even, then it holds for the product measure, the product density and the product of the two sets.

theorem HasSliceBound.of_measurePreserving {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [AddCommGroup E] [Module ℝ E] [MeasurableSpace F] [AddCommGroup F] [Module ℝ F] {μ : MeasureTheory.Measure E} {ν : MeasureTheory.Measure F} (e : E ≃ₗ[ℝ] F) (he : MeasureTheory.MeasurePreserving (⇑e) μ ν) (hsymm : Measurable ⇑e.symm) {g : F → ENNReal} (hg : Measurable g) {Q : Set F} (hQ : MeasurableSet Q) (hb : HasSliceBound ν g Q) : HasSliceBound μ (fun (x : E) => g (e x)) (⇑e ⁻¹' Q)

The slice bound transports along a measure-preserving linear equivalence.