AnalyticNumberTheory.LargeSieve.GeomSum

Geometric-sum bound

The first analytic step in Montgomery's additive large-sieve argument: for e(x) = exp(2πix) and ‖x‖, the distance to the nearest integer (expressed using Int.fract), the bound for nonintegral x is

|Σ_{n<N} e(nx)| ≤ min(N, 1/(2‖x‖)).

This module proves the trivial bound ≤ N for every x (each summand has norm 1) and the nontrivial bound ≤ 1/(2‖x‖) for nonintegral x, using the geometric-series formula, |e(x)−1| = 2|sin(πx)|, and |sin(πt)| ≥ 2·min(t,1−t) for t ∈ [0,1].

References: Iwaniec--Kowalski, "Analytic Number Theory" (2004), Ch. 7 Lemma 7.6; Davenport, "Multiplicative Number Theory", Ch. 27.

1. Distance to the nearest integer

theorem AnalyticNumberTheory.LargeSieve.fract_nonneg (x : ℝ) : 0 ≤ Int.fract x

The fractional part x − ⌊x⌋ ∈ [0,1) is nonnegative.

theorem AnalyticNumberTheory.LargeSieve.fract_lt_one (x : ℝ) : Int.fract x < 1

The fractional part is less than 1.

noncomputable def AnalyticNumberTheory.LargeSieve.distToInt (x : ℝ) : ℝ

Distance to the nearest integer: ‖x‖ = min(x − ⌊x⌋, 1 − (x − ⌊x⌋)).

Equations

• AnalyticNumberTheory.LargeSieve.distToInt x = min (Int.fract x) (1 - Int.fract x)

theorem AnalyticNumberTheory.LargeSieve.distToInt_nonneg (x : ℝ) : 0 ≤ distToInt x

theorem AnalyticNumberTheory.LargeSieve.distToInt_le_half (x : ℝ) : distToInt x ≤ 1 / 2

2. Additive characters and geometric series

noncomputable def AnalyticNumberTheory.LargeSieve.charReal (x : ℝ) : ℂ

e(x) = exp(2πix): the additive character parametrized by ℝ.

Equations

• AnalyticNumberTheory.LargeSieve.charReal x = Complex.exp (2 * ↑Real.pi * ↑x * Complex.I)

theorem AnalyticNumberTheory.LargeSieve.charReal_nat_mul (n : ℕ) (x : ℝ) : charReal (↑n * x) = charReal x ^ n

e(nx) = e(x)^n (n : ℕ), by Complex.exp_nsmul.

theorem AnalyticNumberTheory.LargeSieve.charReal_periodic : Function.Periodic charReal 1

e is 1-periodic: e(x+1) = e(x), since exp(2πi) = 1.

theorem AnalyticNumberTheory.LargeSieve.charReal_add (a b : ℝ) : charReal (a + b) = charReal a * charReal b

e(a + b) = e(a)·e(b): the character maps addition in ℝ to multiplication in ℂ.

theorem AnalyticNumberTheory.LargeSieve.mul_charReal_arg (c : ℂ) : 2 * ↑Real.pi * c * Complex.I = c * (2 * ↑Real.pi * Complex.I)

Rearrangement of the argument: (2π·c)·I = c·(2π·I), a polynomial identity for every complex c (in particular, for every real c).

theorem AnalyticNumberTheory.LargeSieve.charReal_eq_charReal_fract (x : ℝ) : charReal x = charReal (Int.fract x)

The character depends only on the class modulo 1: e(x) = e(fract x).

theorem AnalyticNumberTheory.LargeSieve.geomSum_exp_eq_geomSeries (N : ℕ) {x : ℝ} (hz : charReal x ≠ 1) : ∑ n ∈ Finset.range N, charReal (↑n * x) = (charReal (↑N * x) - 1) / (charReal x - 1)

Geometric-series identity: Σ_{n<N} e(nx) = (e(Nx)−1)/(e(x)−1) when e(x) ≠ 1.

theorem AnalyticNumberTheory.LargeSieve.geomSum_exp_bound_trivial (N : ℕ) (x : ℝ) : ‖∑ n ∈ Finset.range N, charReal (↑n * x)‖ ≤ ↑N

Trivial bound: |Σ_{n<N} e(nx)| ≤ N, since every term has norm 1.

3. Trigonometric identities

theorem AnalyticNumberTheory.LargeSieve.abs_charReal_sub_one (x : ℝ) : ‖charReal x - 1‖ = 2 * |Real.sin (Real.pi * x)|

|e(x) − 1| = 2|sin(πx)|, combining e(x) = exp(πix)² and exp(πix) − exp(−πix) = 2i·sin(πx).

theorem AnalyticNumberTheory.LargeSieve.abs_sin_pi_mul_ge_two_min (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : 2 * min t (1 - t) ≤ |Real.sin (Real.pi * t)|

|sin(πt)| ≥ 2·min(t, 1−t) for t ∈ [0,1]: use sin(πt) ≥ 2t on [0,1/2], and reflection sin(πt) = sin(π(1−t)) on [1/2,1].

4. Nontrivial bound

theorem AnalyticNumberTheory.LargeSieve.charReal_ne_one_of_not_int {x : ℝ} (hx : ¬∃ (k : ℤ), ↑k = x) : charReal x ≠ 1

e(x) ≠ 1 for x ∉ ℤ, since |e(x)−1| = 2|sin(π·fract x)| > 0.

theorem AnalyticNumberTheory.LargeSieve.geomSum_exp_bound_far (N : ℕ) {x : ℝ} (hx : ¬∃ (k : ℤ), ↑k = x) : ‖∑ n ∈ Finset.range N, charReal (↑n * x)‖ ≤ 1 / (2 * distToInt x)

Geometric-sum bound (nontrivial part): for x ∉ ℤ, |Σ_{n<N} e(nx)| ≤ 1/(2‖x‖). Combine the geometric-series formula, |e(x)−1| = 2|sin(π·fract x)|, and |sin(πt)| ≥ 2·min(t,1−t).

theorem AnalyticNumberTheory.LargeSieve.geomSum_exp_bound (N : ℕ) (x : ℝ) : ‖∑ n ∈ Finset.range N, charReal (↑n * x)‖ ≤ ↑N ∧ ((¬∃ (k : ℤ), ↑k = x) → ‖∑ n ∈ Finset.range N, charReal (↑n * x)‖ ≤ 1 / (2 * distToInt x))

Geometric-sum bound: the two components of |Σ_{n<N} e(nx)| ≤ min(N, 1/(2‖x‖)). The trivial component holds for all N, x; the nontrivial component requires x ∉ ℤ.

5. Interval geometric-sum bound

theorem AnalyticNumberTheory.LargeSieve.charReal_neg (x : ℝ) : charReal (-x) = star (charReal x)

The character at a negative argument: e(−x) = star(e(x)), by exp(conj z) = conj(exp z).

theorem AnalyticNumberTheory.LargeSieve.charReal_sub (a b : ℝ) : charReal (a - b) = charReal a * star (charReal b)

Character identity: e(a − b) = e(a)·star(e(b)), using the homomorphism property and conjugation.

noncomputable def AnalyticNumberTheory.LargeSieve.charRealSubIcc (M : ℤ) (N : ℕ) (x : ℝ) : ℂ

The exponential sum Σ_{M<n≤M+N} e(nx) over the shifted interval (M, M+N] (n : ℤ).

Equations

• AnalyticNumberTheory.LargeSieve.charRealSubIcc M N x = ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), AnalyticNumberTheory.LargeSieve.charReal (↑n * x)

theorem AnalyticNumberTheory.LargeSieve.charRealSubIcc_succ (M : ℤ) (N : ℕ) (x : ℝ) : charRealSubIcc M (N + 1) x = charRealSubIcc M N x + charReal (↑(M + ↑N + 1) * x)

theorem AnalyticNumberTheory.LargeSieve.charRealSubIcc_eq_shift (M : ℤ) (N : ℕ) (x : ℝ) : charRealSubIcc M N x = charReal (↑(M + 1) * x) * ∑ k ∈ Finset.range N, charReal (↑k * x)

Interval exponential-sum factorization: Σ_{M<n≤M+N} e(nx) = e((M+1)x)·Σ_{k<N} e(kx).

theorem AnalyticNumberTheory.LargeSieve.geomSum_exp_bound_Icc_trivial (M : ℤ) (N : ℕ) (x : ℝ) : ‖charRealSubIcc M N x‖ ≤ ↑N

Interval exponential sum (trivial bound): |Σ_{M<n≤M+N} e(nx)| ≤ N.

theorem AnalyticNumberTheory.LargeSieve.geomSum_exp_bound_Icc_far (M : ℤ) (N : ℕ) {x : ℝ} (hx : ¬∃ (k : ℤ), ↑k = x) : ‖charRealSubIcc M N x‖ ≤ 1 / (2 * distToInt x)

Interval exponential sum (nontrivial bound): for x ∉ ℤ, |Σ_{M<n≤M+N} e(nx)| ≤ 1/(2‖x‖).

theorem AnalyticNumberTheory.LargeSieve.geomSum_exp_bound_Icc (M : ℤ) (N : ℕ) (x : ℝ) : ‖charRealSubIcc M N x‖ ≤ ↑N ∧ ((¬∃ (k : ℤ), ↑k = x) → ‖charRealSubIcc M N x‖ ≤ 1 / (2 * distToInt x))

Interval geometric-sum bound: the two components of |Σ_{M<n≤M+N} e(nx)| ≤ min(N, 1/(2‖x‖)), with the nontrivial component conditional on x ∉ ℤ.