Few lattice points of a box lie far below its centre

For positive integers r i, i : ι, the box ∏ i, {0, …, r i} has ∏ i, (r i + 1) points d, and the normalized coordinate sum ∑ i, d i / r i has mean n / 2, where n = #ι. This file proves that the points with ∑ i, d i / r i ≤ (n / 2) (1 - ε) make up at most the fraction exp (-ε² n / 2) of the box.

This is the counting estimate behind the auxiliary polynomial in Roth's theorem. There the unknowns are the coefficients of a polynomial in n variables of partial degrees at most r i, and vanishing to weighted index (n / 2) (1 - ε) at a diagonal point imposes one linear condition for each d in the small set counted here. Once n is large, the conditions are far fewer than the unknowns, so Siegel's lemma gives a solution with small coefficients.

Main results

• TauCeti.card_piFinset_range, TauCeti.card_piFinset_range_le_two_pow: the box has ∏ i, (r i + 1) ≤ 2 ^ (∑ i, r i) points.
• TauCeti.sum_range_exp_mul_div_sub_half_le: Hoeffding's lemma on the grid {0, 1 / r, …, 1}, ∑ k ≤ r, exp (t (k / r - 1 / 2)) ≤ (r + 1) exp (t² / 8).
• TauCeti.card_filter_sum_div_le_mul_one_sub_le: the count #{d : ∑ i, d i / r i ≤ (n / 2) (1 - ε)} ≤ (∏ i, (r i + 1)) exp (-ε² n / 2) for ε ≥ 0.
• TauCeti.two_mul_mul_card_filter_le: if 2 D ≤ exp (ε² n / 2), then 2 D times that count is at most the size ∏ i, (r i + 1) of the box.
• TauCeti.one_le_sum_of_le_exp: such a bound with D > 0 forces n > 0, so ∑ i, r i ≥ 1.

Implementation notes

The proof is the Chernoff bound written as a count. Each point of the small set contributes at least 1 to exp (2 ε ((n / 2) (1 - ε) - ∑ i, d i / r i)), and the sum of this exponential over the whole box factors over the coordinates. In each coordinate, pairing k with r - k turns the exponential sum into a sum of hyperbolic cosines, which Real.cosh_le_exp_half_sq bounds.

Mathlib's measure-theoretic Hoeffding inequality ProbabilityTheory.measure_sum_ge_le_of_iIndepFun gives the same estimate, but applying it here would first require identifying the normalized counting measure on the box with a product of uniform measures on the coordinates, which is longer than the direct argument.

Pottmeyer states the bound with exp (-ε² n / 4) and assumes ε < 1. The direct argument gives the exponent ε² n / 2 and needs only 0 ≤ ε; for negative ε the estimate fails, since the whole box can satisfy the condition.

References

• L. Pottmeyer, Diophantine Approximation (2022), Lemma 2.6.4.
• W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58 (1963), 13–30.

theorem TauCeti.card_piFinset_range {ι : Type u_1} [Fintype ι] [DecidableEq ι] (r : ι → ℕ) : (Fintype.piFinset fun (i : ι) => Finset.range (r i + 1)).card = ∏ i : ι, (r i + 1)

The box ∏ i, {0, …, r i} has ∏ i, (r i + 1) points.

theorem TauCeti.card_piFinset_range_le_two_pow {ι : Type u_1} [Fintype ι] [DecidableEq ι] (r : ι → ℕ) : (Fintype.piFinset fun (i : ι) => Finset.range (r i + 1)).card ≤ 2 ^ ∑ i : ι, r i

The box ∏ i, {0, …, r i} has at most 2 ^ (∑ i, r i) points.

theorem TauCeti.sum_range_exp_mul_div_sub_half_le {r : ℕ} (hr : r ≠ 0) (t : ℝ) : ∑ k ∈ Finset.range (r + 1), Real.exp (t * (↑k / ↑r - 1 / 2)) ≤ (↑r + 1) * Real.exp (t ^ 2 / 8)

Hoeffding's lemma on the grid {0, 1 / r, …, 1}. For r ≠ 0 and every real t, the exponential moment of the uniformly distributed centred point k / r - 1 / 2 satisfies ∑ k ∈ range (r + 1), exp (t (k / r - 1 / 2)) ≤ (r + 1) exp (t² / 8).

theorem TauCeti.card_filter_sum_div_le_mul_one_sub_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ι → ℕ} (hr : ∀ (i : ι), r i ≠ 0) {ε : ℝ} (hε : 0 ≤ ε) : ↑{d ∈ Fintype.piFinset fun (i : ι) => Finset.range (r i + 1) | ∑ i : ι, ↑(d i) / ↑(r i) ≤ ↑(Fintype.card ι) / 2 * (1 - ε)}.card ≤ (∏ i : ι, (↑(r i) + 1)) * Real.exp (-(ε ^ 2 * ↑(Fintype.card ι) / 2))

Few points of a box lie far below its centre (Pottmeyer, Lemma 2.6.4). Let r i ≠ 0 for i : ι and n = #ι. Among the ∏ i, (r i + 1) points d of the box ∏ i, {0, …, r i}, at most (∏ i, (r i + 1)) exp (-ε² n / 2) satisfy ∑ i, d i / r i ≤ (n / 2) (1 - ε), for every ε ≥ 0.

theorem TauCeti.two_mul_mul_card_filter_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ι → ℕ} (hr : ∀ (i : ι), r i ≠ 0) {ε : ℝ} (hε : 0 ≤ ε) {D : ℕ} (hDε : 2 * ↑D ≤ Real.exp (ε ^ 2 * ↑(Fintype.card ι) / 2)) : 2 * (D * {d ∈ Fintype.piFinset fun (i : ι) => Finset.range (r i + 1) | ∑ i : ι, ↑(d i) / ↑(r i) ≤ ↑(Fintype.card ι) / 2 * (1 - ε)}.card) ≤ (Fintype.piFinset fun (i : ι) => Finset.range (r i + 1)).card

Counting the equations: if 2 D ≤ exp (ε² n / 2), then 2 D times the number of points d of the box ∏ᵢ {0, …, rᵢ} with ∑ᵢ dᵢ / rᵢ ≤ (n / 2) (1 - ε) is at most the number ∏ᵢ (rᵢ + 1) of all points of the box.

theorem TauCeti.one_le_sum_of_le_exp {ι : Type u_1} [Fintype ι] {r : ι → ℕ} (hr : ∀ (i : ι), r i ≠ 0) {ε : ℝ} {D : ℕ} (hD : 0 < D) (hDε : 2 * ↑D ≤ Real.exp (ε ^ 2 * ↑(Fintype.card ι) / 2)) : 1 ≤ ∑ i : ι, r i

If the number n of variables satisfies 2 D ≤ exp (ε² n / 2) for some D > 0, then n is positive, so the total degree ∑ᵢ rᵢ is at least one when every rᵢ is nonzero.