The slice bound for a product of balls of volume one

Bombieri–Gubler, Lemma C.3.7. Partition the coordinates of ι → ℝ into blocks by a map blk : ι → κ, and let prodBallPi blk be the product over the blocks of the euclidean ball of volume one in that block's coordinates. Then for every measurable convex symmetric A, the Gauss measure of A is at most vol (A ∩ prodBallPi blk).

The induction is on the number of coordinates, splitting off the block of a chosen coordinate; the remaining blocks keep the same label type κ, with one label whose block has become empty — and an empty block imposes no condition, so no re-indexing of the labels is needed.

Main definitions

• gaussPi, the Gauss density on ι → ℝ for the euclidean norm.
• ballRadius n, the radius of the ball of volume one in n dimensions.
• prodBallPi blk, the product of the balls of volume one over the blocks of blk.

Main results

• hasSliceBound_ballPi: the case of a single block.
• hasSliceBound_prodBallPi: Bombieri–Gubler, Lemma C.3.7, on ι → ℝ.
• hasSliceBound_prodBallEuclidean: the same on EuclideanSpace ℝ ι.
• hasPrekopaLeindler_innerProductSpace: Prékopa–Leindler on any finite-dimensional real inner product space, which is what Lemma C.3.4 is applied to in Layer 4.5's endgame.

Implementation notes

⚠ The induction is on coordinates, not on blocks, and that removes all re-indexing. Splitting off the block of one coordinate leaves a smaller coordinate set with the same label type; the label just peeled off now has an empty block, and the condition attached to an empty block — 0 ≤ ballRadius 0 ^ 2 — is vacuous. Inducting on the number of blocks instead would force the labels to be renumbered at every step.

⚠ The radius is indexed by the cardinality of the block, not by the block. ballRadius n is the radius of the ball of volume one in EuclideanSpace ℝ (Fin n); a block is a subtype, and unitVolumeRadius_euclideanSpace identifies its radius with ballRadius of its cardinality. This is the one place where the index type is changed, and it is done once rather than at every step of the induction.

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.

noncomputable def gaussPi {ι : Type u_1} [Fintype ι] (x : ι → ℝ) : ENNReal

The Gauss density on ι → ℝ for the euclidean norm.

Equations

• gaussPi x = ENNReal.ofReal (Real.exp (-Real.pi * ∑ i : ι, x i ^ 2))

theorem measurable_gaussPi {ι : Type u_1} [Fintype ι] : Measurable gaussPi

theorem gaussPi_le_one {ι : Type u_1} [Fintype ι] (x : ι → ℝ) : gaussPi x ≤ 1

theorem gaussPi_neg {ι : Type u_1} [Fintype ι] (x : ι → ℝ) : gaussPi (-x) = gaussPi x

theorem gaussPi_eq_gaussDensity {ι : Type u_1} [Fintype ι] (x : ι → ℝ) : gaussPi x = gaussDensity (WithLp.toLp 2 x)

theorem logConcave_gaussPi {ι : Type u_1} [Fintype ι] : LogConcave gaussPi

The Gauss density is log-concave: the quadratic form ∑ x i ^ 2 is convex.

noncomputable def ballRadius (n : ℕ) : ℝ

The radius of the ball of volume one in n dimensions: Bombieri–Gubler's ρ(n).

Equations

• ballRadius n = unitVolumeRadius (EuclideanSpace ℝ (Fin n))

theorem ballRadius_pos (n : ℕ) : 0 < ballRadius n

theorem volume_ball_euclideanSpace_congr {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (e : α ≃ β) : MeasureTheory.volume (Metric.ball 0 1) = MeasureTheory.volume (Metric.ball 0 1)

theorem unitVolumeRadius_euclideanSpace (α : Type u_1) [Fintype α] : unitVolumeRadius (EuclideanSpace ℝ α) = ballRadius (Fintype.card α)

theorem hasSliceBound_ballPi (α : Type u_1) [Fintype α] : HasSliceBound MeasureTheory.volume gaussPi {y : α → ℝ | ∑ j : α, y j ^ 2 ≤ ballRadius (Fintype.card α) ^ 2}

The slice bound for a single block: the ball of volume one in α → ℝ.

theorem hasSliceBound_univ_of_le_one {E : Type u_1} [MeasurableSpace E] [AddCommGroup E] [Module ℝ E] {μ : MeasureTheory.Measure E} {g : E → ENNReal} (hg : ∀ (x : E), g x ≤ 1) {Q : Set E} (hQ : ∀ (x : E), x ∈ Q) : HasSliceBound μ g Q

theorem convex_setOf_sum_sq_le {ι : Type u_1} {S : Type u_2} [Fintype S] (f : S → ι) (c : ℝ) : Convex ℝ {x : ι → ℝ | ∑ j : S, x (f j) ^ 2 ≤ c}

theorem measurableSet_setOf_sum_sq_le {ι : Type u_1} {S : Type u_2} [Fintype S] (f : S → ι) (c : ℝ) : MeasurableSet {x : ι → ℝ | ∑ j : S, x (f j) ^ 2 ≤ c}

theorem neg_mem_setOf_sum_sq_le {ι : Type u_1} {S : Type u_2} [Fintype S] (f : S → ι) (c : ℝ) {x : ι → ℝ} (hx : x ∈ {x : ι → ℝ | ∑ j : S, x (f j) ^ 2 ≤ c}) : -x ∈ {x : ι → ℝ | ∑ j : S, x (f j) ^ 2 ≤ c}

def prodBallPi {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq κ] (blk : ι → κ) : Set (ι → ℝ)

The product over the blocks of blk of the euclidean ball of volume one in that block's coordinates: Bombieri–Gubler's Q_N = B_{ρ(n₁)} × ⋯ × B_{ρ(n_r)}.

Equations

• prodBallPi blk = {x : ι → ℝ | ∀ (k : κ), ∑ j : { j : ι // blk j = k }, x ↑j ^ 2 ≤ ballRadius (Fintype.card { j : ι // blk j = k }) ^ 2}

theorem prodBallPi_eq_iInter {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq κ] (blk : ι → κ) : prodBallPi blk = ⋂ (k : κ), {x : ι → ℝ | ∑ j : { j : ι // blk j = k }, x ↑j ^ 2 ≤ ballRadius (Fintype.card { j : ι // blk j = k }) ^ 2}

theorem measurableSet_prodBallPi {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq κ] [Countable κ] (blk : ι → κ) : MeasurableSet (prodBallPi blk)

theorem convex_prodBallPi {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq κ] (blk : ι → κ) : Convex ℝ (prodBallPi blk)

theorem neg_mem_prodBallPi {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq κ] (blk : ι → κ) {x : ι → ℝ} (hx : x ∈ prodBallPi blk) : -x ∈ prodBallPi blk

theorem hasPrekopaLeindler_euclideanSpace' (α : Type u_1) [Fintype α] : HasPrekopaLeindler MeasureTheory.volume

Prékopa–Leindler on EuclideanSpace ℝ α for an arbitrary finite index type.

theorem hasPrekopaLeindler_pi' (α : Type u_1) [Fintype α] : HasPrekopaLeindler MeasureTheory.volume

Prékopa–Leindler on α → ℝ for an arbitrary finite index type.

theorem hasPrekopaLeindler_innerProductSpace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : HasPrekopaLeindler MeasureTheory.volume

Prékopa–Leindler on a finite-dimensional real inner product space.

theorem hasSliceBound_prodBallPi {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq κ] [Countable κ] (blk : ι → κ) : HasSliceBound MeasureTheory.volume gaussPi (prodBallPi blk)

Bombieri–Gubler, Lemma C.3.7: the Gauss measure of a measurable convex symmetric set is at most its volume inside a product of euclidean balls of volume one.

def prodBall {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq κ] (blk : ι → κ) : Set (EuclideanSpace ℝ ι)

The product of balls of volume one, in EuclideanSpace ℝ ι.

Equations

• prodBall blk = {x : EuclideanSpace ℝ ι | ∀ (k : κ), ∑ j : { j : ι // blk j = k }, x.ofLp ↑j ^ 2 ≤ ballRadius (Fintype.card { j : ι // blk j = k }) ^ 2}

theorem prodBall_eq_preimage {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq κ] (blk : ι → κ) : prodBall blk = ⇑(WithLp.linearEquiv 2 ℝ (ι → ℝ)) ⁻¹' prodBallPi blk

theorem measurableSet_prodBall {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq κ] [Countable κ] (blk : ι → κ) : MeasurableSet (prodBall blk)

theorem convex_prodBall {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq κ] (blk : ι → κ) : Convex ℝ (prodBall blk)

theorem neg_mem_prodBall {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq κ] (blk : ι → κ) {x : EuclideanSpace ℝ ι} (hx : x ∈ prodBall blk) : -x ∈ prodBall blk

theorem hasSliceBound_prodBall {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq κ] [Countable κ] (blk : ι → κ) : HasSliceBound MeasureTheory.volume gaussDensity (prodBall blk)

Bombieri–Gubler, Lemma C.3.7 on EuclideanSpace ℝ ι.