Vaaler's cube-slicing theorem

Every central slice of the cube [-1, 1] ^ ι by a linear subspace V of dimension k has k-dimensional volume at least 2 ^ k (Vaaler 1979). Every central slice of the unit polydisc of ℂ ^ ι by a complex subspace of dimension k has real volume at least π ^ k. This file proves both along the route of Bombieri–Gubler, Appendix C.3.

1. The Gauss measure against a product of balls (Lemma C.3.7). Let B = ∏ i, B i be a product of closed balls B i ⊆ α i, each of volume at least one, in finite-dimensional real inner product spaces. Then the Gauss measure of every measurable convex set A ⊆ ∀ i, α i with -A = A is at most volume (A ∩ B). For a single ball this is TauCeti.setLIntegral_ofReal_exp_neg_pi_mul_sq_norm_le_volume_inter_closedBall, and TauCeti.pi_apply_le_pi_apply_of_forall_convex passes it to products, since the Gauss density and the indicator of a ball are log-concave and even.
2. Central slices (the slicing step of Theorem C.3.8). If Q ⊆ E is measurable, convex and symmetric, and the Gauss measure of every measurable symmetric convex set A is at most volume (A ∩ Q), then every central slice V ∩ Q has volume at least one in V. Apply the hypothesis to the slab A of points within distance ε of V. Its Gauss measure is at least exp (-π ε ^ 2) * volume (closedBall (0 : Vᗮ) ε), because the Gauss density factors along E = Vᗮ ⊕ V. The parallel slices V ∩ (Q - w) of Q are at most as large as the central one (Brunn's principle, Convex.measure_preimage_prodMk_le_measure_preimage_prodMk_zero), so volume (A ∩ Q) ≤ volume (V ∩ Q) * volume (closedBall (0 : Vᗮ) ε). Let ε tend to 0.
3. Products of balls. In the L² product PiLp 2 α, whose volume is the product of the volumes of the factors, the first step supplies the hypothesis of the second for the product {x | ∀ i, ‖x i‖ ≤ ρ i} of balls of volume at least one, so its central slices have volume at least one.
4. The cube and the polydisc. The cube [-1/2, 1/2] ^ ι is a product of intervals of length one, and scaling by 2 gives 2 ^ k. The polydisc of radius 1 / √π is a product of discs of area one, and scaling by √π in real dimension 2 * k gives π ^ k.

No dominated convergence is needed in the second step, because Brunn's principle bounds every parallel slice by the central one.

Main results

• TauCeti.setLIntegral_prod_ofReal_exp_neg_pi_mul_sq_norm_le_volume_inter_pi: Bombieri–Gubler, Lemma C.3.7, the Gauss measure of a symmetric convex set against a product of balls of volume at least one.
• Submodule.one_le_volume_preimage_coe: the slicing step of Bombieri–Gubler, Theorem C.3.8, every central slice of a symmetric convex set that dominates the Gauss measure has volume at least one.
• Submodule.one_le_volume_setOf_forall_norm_le: every central slice of a product of balls of volume at least one has volume at least one.
• Submodule.two_pow_finrank_le_volume_setOf_forall_abs_le_one: Vaaler's cube-slicing theorem.
• Submodule.pi_pow_finrank_le_volume_setOf_forall_norm_le_one: its complex counterpart, for the unit polydisc.

References

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

The thickening argument that bounds the parallel slices by the central one follows the Apache-2.0 formalization of Vaaler's theorem in rwst/Subspace-Theorems (file ArithmeticHeights/CubeSlicing.lean), by Ralf Stephan.

theorem TauCeti.setLIntegral_prod_ofReal_exp_neg_pi_mul_sq_norm_le_volume_inter_pi {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → NormedAddCommGroup (α i)] [(i : ι) → InnerProductSpace ℝ (α i)] [∀ (i : ι), FiniteDimensional ℝ (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), BorelSpace (α i)] {ρ : ι → ℝ} (hρ : ∀ (i : ι), 1 ≤ MeasureTheory.volume (Metric.closedBall 0 (ρ i))) {A : Set ((i : ι) → α i)} (hA : MeasurableSet A) (hAc : Convex ℝ A) (hneg : ∀ x ∈ A, -x ∈ A) : ∫⁻ (x : (i : ι) → α i) in A, ∏ i : ι, ENNReal.ofReal (Real.exp (-Real.pi * ‖x i‖ ^ 2)) ≤ MeasureTheory.volume (A ∩ Set.univ.pi fun (i : ι) => Metric.closedBall 0 (ρ i))

The Gauss measure against a product of balls (Bombieri–Gubler, Lemma C.3.7, for balls of volume one). Let closedBall (0 : α i) (ρ i) have volume at least one in each of finitely many finite-dimensional real inner product spaces α i. Then for every measurable convex set A ⊆ ∀ i, α i with -A = A,

∫⁻ x in A, ∏ i, exp (-π ‖x i‖ ^ 2) ≤ volume (A ∩ univ.pi fun i ↦ closedBall 0 (ρ i)).

Radii with balls of volume exactly one exist by TauCeti.exists_volume_closedBall_eq_one. Unlike Bombieri–Gubler, A need not be closed.

theorem Submodule.one_le_volume_preimage_coe {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (V : Submodule ℝ E) {Q : Set E} (hQ : MeasurableSet Q) (hQc : Convex ℝ Q) (hQneg : ∀ x ∈ Q, -x ∈ Q) (hgauss : ∀ (A : Set E), MeasurableSet A → Convex ℝ A → (∀ x ∈ A, -x ∈ A) → ∫⁻ (x : E) in A, ENNReal.ofReal (Real.exp (-Real.pi * ‖x‖ ^ 2)) ≤ MeasureTheory.volume (A ∩ Q)) : 1 ≤ MeasureTheory.volume (Subtype.val ⁻¹' Q)

Central slices of a set that dominates the Gauss measure (the slicing step of Bombieri–Gubler, Theorem C.3.8). Let Q ⊆ E be measurable, convex and symmetric about the origin, and suppose that the Gauss measure ∫⁻ x in A, exp (-π ‖x‖ ^ 2) of every measurable convex set A with -A = A is at most volume (A ∩ Q). Then for every subspace V, the central slice V ∩ Q has volume at least one, computed in V.

The hypothesis holds for a product of balls of volume at least one, by TauCeti.setLIntegral_prod_ofReal_exp_neg_pi_mul_sq_norm_le_volume_inter_pi.

theorem Submodule.one_le_volume_setOf_forall_norm_le {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → NormedAddCommGroup (α i)] [(i : ι) → InnerProductSpace ℝ (α i)] [∀ (i : ι), FiniteDimensional ℝ (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), BorelSpace (α i)] {ρ : ι → ℝ} (hρ : ∀ (i : ι), 1 ≤ MeasureTheory.volume (Metric.closedBall 0 (ρ i))) (V : Submodule ℝ (PiLp 2 α)) : 1 ≤ MeasureTheory.volume {x : ↥V | ∀ (i : ι), ‖(↑x).ofLp i‖ ≤ ρ i}

Central slices of a product of balls of volume at least one. Let closedBall (0 : α i) (ρ i) have volume at least one in each of finitely many finite-dimensional real inner product spaces α i. Then every central slice of the product {x | ∀ i, ‖x i‖ ≤ ρ i} of these balls by a real subspace V of the L² product PiLp 2 α has volume at least one, computed in V.

The cube [-1, 1] ^ ι and the unit polydisc of ℂ ^ ι are dilates of such products.

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

Vaaler's cube-slicing theorem. Every central slice of the cube [-1, 1] ^ ι by a subspace V of EuclideanSpace ℝ ι has volume at least 2 ^ finrank ℝ V, computed in V.

theorem Submodule.pi_pow_finrank_le_volume_setOf_forall_norm_le_one {ι : Type u_1} [Fintype ι] (V : Submodule ℂ (EuclideanSpace ℂ ι)) : ENNReal.ofReal Real.pi ^ Module.finrank ℂ ↥V ≤ MeasureTheory.volume {x : ↥(restrictScalars ℝ V) | ∀ (i : ι), ‖(↑x).ofLp i‖ ≤ 1}

Central slices of the unit polydisc. Every central slice of the unit polydisc {x | ∀ i, ‖x i‖ ≤ 1} of ℂ ^ ι by a complex subspace V of EuclideanSpace ℂ ι has real volume at least π ^ finrank ℂ V, computed in the real subspace V.restrictScalars ℝ.

This is the complex counterpart of Vaaler's cube-slicing theorem Submodule.two_pow_finrank_le_volume_setOf_forall_abs_le_one: the polydisc is the product of the discs of radius 1 / √π, of area one, dilated by √π, and V has real dimension 2 * finrank ℂ V.