A lower bound for a sum of truncated linear terms #
For k m : ℕ with m ≤ k + 1 and δ : ℝ we prove
m * min (δ / 2) (δ ^ 2 / 2) ≤ ∑ i ∈ Finset.range m, max (δ - i / k) 0,
where i / k is real division, so that i / 0 = 0. The left-hand side is m δ / 2 for
δ ≥ 1 and m δ² / 2 for 0 ≤ δ ≤ 1.
This is the numerical estimate in the inductive step of Roth's lemma, which bounds the index
of a multivariate polynomial at a point of large height. A Hasse derivative of order l in a
variable of weight k lowers the index by at most l / k, so it keeps index at least
max (δ - l / k) 0 when the polynomial has index δ. The estimate bounds the sum of these
lower bounds over l = 0, …, m - 1 from below by a quantity that is quadratic in δ for small
δ. The number m of derivatives is one more than the degree of the polynomial in the
variable, so it can be smaller than k + 1.
Main results #
TauCeti.mul_min_le_sum_max_sub_div: the lower bound above.
Implementation notes #
The case m = k + 1 is Pottmeyer's computation. Since the terms decrease in i, Chebyshev's
sum inequality MonovaryOn.sum_mul_sum_le_card_mul_sum shows that the average of the first m
terms is at least the average of all k + 1 terms, which gives the general case.
References #
- L. Pottmeyer, Diophantine Approximation (2022), §3.4, Lemma 3.4.8 and Exercise 3.7.
Pottmeyer, Lemma 3.4.8. For k : ℕ, m ≤ k + 1 and δ : ℝ, the positive parts of
δ - i / k for i = 0, …, m - 1 sum to at least m * min (δ / 2) (δ ^ 2 / 2). Here i / k is
real division, so for k = 0 the sum is m * max δ 0.