Vaaler's cube-slicing theorem

Bombieri–Gubler, Theorem C.3.8 (Vaaler 1979). Let Q be a product of euclidean balls each of volume one, one factor per block of a partition of the coordinates of ℝᴺ. Then every central slice of Q by a linear subspace V has volume at least one, the volume being computed on V with its own inner-product structure. Two corollaries: the cube [-1, 1]ᴺ has central slices of volume at least 2 ^ dim V, and the unit polydisc of ℂⁿ has central slices of real volume at least 2 ^ (dim V / 2).

Main definitions

• Submodule.prodOrthogonalEquiv V: the orthogonal decomposition E ≃ₗ[ℝ] V × Vᗮ, as a measure-preserving linear equivalence.
• unitBallVolume n: the volume of the unit ball of EuclideanSpace ℝ (Fin n).

Main results

• one_le_volume_subtype_mem: Bombieri–Gubler, Theorem C.3.8 in the form the slice bound gives it, for an arbitrary measurable convex symmetric Q satisfying HasSliceBound.
• one_le_volume_inter_prodBall: the product-of-balls theorem in the roadmap's form.
• two_pow_finrank_le_volume_inter_cube: Vaaler's cube-slicing theorem.
• two_pow_le_volume_inter_polydisc: the inscribed-cube bound at a complex place.

Implementation notes

⚠ The ε-thickening needs no dominated convergence, because a slice of a symmetric convex body is largest at the centre. Bombieri–Gubler pass to the limit ε → 0 in vol (Q ∩ L_ε) / vol (B_ε) by computing the limit of the integrand and dominating it. The same limit is avoided here: the function z ↦ vol_V {y | y + z ∈ Q} on Vᗮ is log-concave, by Lemma C.3.4, and even, because Q is symmetric, so it is bounded by its value at zero — which is the slice volume being estimated. That turns the right-hand side into vol_V (Q ∩ V) * vol (B_ε) with no limit at all, and the left-hand side is bounded below by exp (-π ε ^ 2) * vol (B_ε) because the Gauss density is. Dividing and letting ε → 0 is then a one-line limit of exp (-π ε ^ 2). Brunn's principle — that the central slice is the largest one — is thus the only extra ingredient, and log-concavity of marginals already supplies it.

⚠ The complex structure is not needed for the polydisc bound. The roadmap states two_pow_le_volume_inter_polydisc for a subspace closed under the complex structure J, since that is where the bound is applied; but the proof inscribes the cube of half-side 2 ^ (-1/2) in the polydisc and applies the cube case, which gives √2 ^ dim V, and 2 ^ (dim V / 2) ≤ √2 ^ dim V holds whether or not dim V is even. So the hypothesis is dropped here.

References

E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Theorem C.3.8; J. D. Vaaler, A geometric inequality with applications to linear forms, Pacific Journal of Mathematics 83 (1979), 543–553.

This is Layer 4.5 of the ArithmeticHeights roadmap.

noncomputable def Submodule.prodOrthogonalEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (V : Submodule ℝ E) : E ≃ₗ[ℝ] ↥V × ↥Vᗮ

The orthogonal decomposition E ≃ₗ[ℝ] V × Vᗮ, forgetting the L² structure of the target.

Equations

• V.prodOrthogonalEquiv = V.orthogonalDecomposition.toLinearEquiv ≪≫ₗ WithLp.linearEquiv 2 ℝ (↥V × ↥Vᗮ)

theorem Submodule.prodOrthogonalEquiv_symm_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (V : Submodule ℝ E) (q : ↥V × ↥Vᗮ) : V.prodOrthogonalEquiv.symm q = ↑q.1 + ↑q.2

theorem Submodule.norm_prodOrthogonalEquiv_symm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (V : Submodule ℝ E) (q : ↥V × ↥Vᗮ) : ‖V.prodOrthogonalEquiv.symm q‖ ^ 2 = ‖q.1‖ ^ 2 + ‖q.2‖ ^ 2

theorem Submodule.measurePreserving_prodOrthogonalEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (V : Submodule ℝ E) : MeasureTheory.MeasurePreserving (⇑V.prodOrthogonalEquiv) MeasureTheory.volume (MeasureTheory.volume.prod MeasureTheory.volume)

theorem LogConcave.le_apply_zero {F : Type u_2} [AddCommGroup F] [Module ℝ F] {f : F → ENNReal} (hf : LogConcave f) (hfe : ∀ (x : F), f (-x) = f x) (x : F) : f x ≤ f 0

A log-concave even function attains its maximum at the origin (Brunn's principle, for the marginals of a symmetric convex body).

theorem one_le_volume_subtype_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Q : Set E} (hQm : MeasurableSet Q) (hQc : Convex ℝ Q) (hQs : ∀ x ∈ Q, -x ∈ Q) (hQ : HasSliceBound MeasureTheory.volume gaussDensity Q) (V : Submodule ℝ E) : 1 ≤ MeasureTheory.volume {y : ↥V | ↑y ∈ Q}

Bombieri–Gubler, Theorem C.3.8. If the Gauss measure of every measurable convex symmetric set is at most its volume inside Q, then every central slice of Q by a linear subspace has volume at least one, computed on the subspace.

noncomputable def unitBallVolume (n : ℕ) : ℝ

The volume ω_n of the unit ball of EuclideanSpace ℝ (Fin n).

Equations

• unitBallVolume n = (MeasureTheory.volume (Metric.ball 0 1)).toReal

theorem unitBallVolume_pos (n : ℕ) : 0 < unitBallVolume n

theorem ballRadius_eq (n : ℕ) : ballRadius n = unitBallVolume n ^ (-(1 / ↑n))

theorem ballRadius_sq (n : ℕ) : ballRadius n ^ 2 = unitBallVolume n ^ (-(2 / ↑n))

theorem unitBallVolume_one : unitBallVolume 1 = 2

theorem ballRadius_one : ballRadius 1 = 1 / 2

theorem unitBallVolume_two : unitBallVolume 2 = Real.pi

theorem ballRadius_two : ballRadius 2 = 1 / √Real.pi

theorem sq_le_sq_iff_abs_le {a c : ℝ} (hc : 0 ≤ c) : a ^ 2 ≤ c ^ 2 ↔ |a| ≤ c

theorem one_le_volume_prodBall_subtype {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq κ] [Countable κ] (blk : ι → κ) (V : Submodule ℝ (EuclideanSpace ℝ ι)) : 1 ≤ MeasureTheory.volume {y : ↥V | ↑y ∈ prodBall blk}

The product-of-balls theorem for an arbitrary index type.

theorem prodBall_id {ι : Type u_2} [Fintype ι] [DecidableEq ι] : prodBall id = {x : EuclideanSpace ℝ ι | ∀ (i : ι), |x.ofLp i| ≤ 1 / 2}

With singleton blocks, the product of balls of volume one is the cube of half-side 1 / 2.

theorem smul_setOf_abs_le {ι : Type u_2} (V : Submodule ℝ (EuclideanSpace ℝ ι)) {r c : ℝ} (hr : 0 < r) : r • {y : ↥V | ∀ (i : ι), |(↑y).ofLp i| ≤ c} = {y : ↥V | ∀ (i : ι), |(↑y).ofLp i| ≤ r * c}

theorem two_pow_finrank_le_volume_inter_cube {ι : Type u_2} [Fintype ι] (V : Submodule ℝ (EuclideanSpace ℝ ι)) : 2 ^ Module.finrank ℝ ↥V ≤ MeasureTheory.volume {y : ↥V | ∀ (i : ι), |(↑y).ofLp i| ≤ 1}

Vaaler's cube-slicing theorem (Vaaler 1979; Bombieri–Gubler, Theorem C.3.8): every central slice of the cube [-1, 1]ᴺ by a k-dimensional subspace has k-volume at least 2 ^ k.

theorem one_le_volume_inter_prodBall {N r : ℕ} (blk : Fin N → Fin r) (V : Submodule ℝ (EuclideanSpace ℝ (Fin N))) : 1 ≤ MeasureTheory.volume {x : ↥V | ∀ (i : Fin r), ∑ j : Fin N with blk j = i, (↑x).ofLp j ^ 2 ≤ unitBallVolume {j : Fin N | blk j = i}.card ^ (-(2 / ↑{j : Fin N | blk j = i}.card))}

The product-of-balls theorem (Bombieri–Gubler, Theorem C.3.8), in the roadmap's form: partition the N coordinates into blocks by blk, let Q be the product over the blocks of the euclidean ball of volume one in that block's coordinates, and every central slice of Q by a subspace V has volume at least one, computed on V.

theorem two_pow_le_volume_inter_polydisc {n : ℕ} (V : Submodule ℝ (EuclideanSpace ℝ (Fin n × Fin 2))) : 2 ^ (Module.finrank ℝ ↥V / 2) ≤ MeasureTheory.volume {y : ↥V | ∀ (i : Fin n), (↑y).ofLp (i, 0) ^ 2 + (↑y).ofLp (i, 1) ^ 2 ≤ 1}

The inscribed-cube bound at a complex place: a subspace of ℝ^{2n}, with coordinates paired as the real and imaginary parts of ℂⁿ, meets the unit polydisc in volume at least 2 ^ (dim V / 2). The polydisc contains the cube of half-side 2 ^ (-1/2), and the cube case gives √2 ^ dim V there, which dominates 2 ^ (dim V / 2) for every dimension, even or odd.