AnalyticNumberTheory.LargeSieve.WellSpaced

Well-spaced points and the Schur test

This module combines the dual quadratic-form identity (dualQuadraticIdentity_Icc, Duality.lean) with the interval geometric-sum bound (geomSum_exp_bound_Icc, GeomSum.lean) to prove an additive large-sieve inequality with an explicit weaker constant.

The spacing condition is parametrized by ℝ: a set X ⊆ ℝ is δ-well-spaced modulo 1 if any two distinct points have distance distToInt at least δ. This corresponds to wellSpaced on AddCircle 1 in Additive.lean, while keeping the counting geometry in the real numbers and their fractional parts. The circle formulation requires a separate bridge.

Proof structure (the classical Montgomery framework, with a weaker constant):

1. Counting: a set in [a, a+L] with pairwise real distances at least δ has at most L/δ + 1 points (sepCard_le_interval, by induction on the largest point). Splitting fractional parts into [0,r] and [1−r,1] gives the ball count #{y : distToInt(x−y) ≤ r} ≤ 2r/δ + 2 (wellSpaced_ball_card_le).
2. Dyadic-shell row sum: for fixed x, group Σ_y |K(x,y)| by dyadic shells of distToInt(x−y). Each shell has at most 2·2^{-j}/δ + 2 points; the geometric bound ≤ 1/(2ρ) gives Σ_{y∈X} |Σ_{M<n≤M+N} e(n(x−y))| ≤ N + (2K+12)/δ, where K = ⌈log₂(1/δ)⌉ (wellSpacedRowSum).
3. Schur/Cauchy--Schwarz test (quadraticFormBound): for a kernel with symmetric norms (|K xy| = |K yx|), as for a Hermitian kernel, row sums at most C imply |Σ_x Σ_y b_x·conj(b_y)·K_xy| ≤ C·Σ_x |b_x|².
4. Assembly: the dual identity, row-sum bound, and Schur test give largeSieveDual_wellSpaced; largeSieveDuality then gives largeSievePrimal_wellSpaced.

The explicit weaker constant is C(N,δ) = N + (2⌈log₂(1/δ)⌉+12)/δ, with the ceiling taken in ℕ. The classical sharp constant N + 1/δ requires Montgomery's positive-kernel/Parseval method (a Fejér-kernel majorant or a Hilbert-type quadratic-form estimate). It is not proved here: naive dyadic-shell counting and the Schur test incur a log(1/δ) factor.

References: Montgomery, "Topics in Multiplicative Number Theory" (1971), Ch. 1; Iwaniec & Kowalski, "Analytic Number Theory" (2004), Ch. 7.

1. Real-parametrized well-spaced sets and basic distance properties

def AnalyticNumberTheory.LargeSieve.wellSpacedReal (X : Finset ℝ) (δ : ℝ) : Prop

X ⊆ ℝ is δ-well-spaced modulo 1: any two distinct points have distance modulo 1 at least δ. This corresponds to wellSpaced on AddCircle 1 in Additive.lean.

Equations

• AnalyticNumberTheory.LargeSieve.wellSpacedReal X δ = ∀ ⦃x : ℝ⦄, x ∈ X → ∀ ⦃y : ℝ⦄, y ∈ X → x ≠ y → δ ≤ AnalyticNumberTheory.LargeSieve.distToInt (x - y)

theorem AnalyticNumberTheory.LargeSieve.distToInt_le_sub (z : ℝ) (k : ℤ) : distToInt z ≤ |z - ↑k|

Distance modulo 1 is bounded by every integer translate: ‖z‖ ≤ |z − k| (k : ℤ).

theorem AnalyticNumberTheory.LargeSieve.distToInt_le_fract (a b : ℝ) : distToInt (a - b) ≤ |Int.fract a - Int.fract b|

Distance modulo 1 is bounded by the difference of fractional parts: ‖a−b‖ ≤ |fract a − fract b|, using the integer translate ⌊a⌋ − ⌊b⌋.

theorem AnalyticNumberTheory.LargeSieve.distToInt_neg (w : ℝ) : distToInt (-w) = distToInt w

Distance modulo 1 is even: ‖−w‖ = ‖w‖.

theorem AnalyticNumberTheory.LargeSieve.distToInt_sub_comm (a b : ℝ) : distToInt (a - b) = distToInt (b - a)

Symmetry of distance modulo 1: ‖a−b‖ = ‖b−a‖.

theorem AnalyticNumberTheory.LargeSieve.distToInt_eq_zero_iff (z : ℝ) : distToInt z = 0 ↔ ∃ (k : ℤ), ↑k = z

distToInt z = 0 if and only if z ∈ ℤ.

theorem AnalyticNumberTheory.LargeSieve.wellSpacedReal_abs_le {X : Finset ℝ} {δ : ℝ} (hws : wellSpacedReal X δ) {x y : ℝ} (hx : x ∈ X) (hy : y ∈ X) (hxy : x ≠ y) : δ ≤ |x - y|

Distinct points of a well-spaced set have real distance at least δ: separation modulo 1 implies separation on the real line.

2. Counting lemmas

theorem AnalyticNumberTheory.LargeSieve.sepCard_le_interval (a L : ℝ) {δ : ℝ} (hδ : 0 < δ) (hL : 0 ≤ L) (S : Finset ℝ) (hS : ∀ x ∈ S, a ≤ x ∧ x ≤ a + L) (hsep : ∀ ⦃x : ℝ⦄, x ∈ S → ∀ ⦃y : ℝ⦄, y ∈ S → x ≠ y → δ ≤ |x - y|) : ↑S.card ≤ L / δ + 1

Interval count: a set in [a, a+L] with pairwise distances at least δ has at most L/δ + 1 points. Choose its largest point m; the remaining points lie in [a, m−δ], so induction applies.

theorem AnalyticNumberTheory.LargeSieve.wellSpaced_fract_left_card_le (X : Finset ℝ) {δ : ℝ} (hδ : 0 < δ) (hws : wellSpacedReal X δ) (x : ℝ) {r : ℝ} (hr : 0 ≤ r) : ↑{y ∈ X | Int.fract (x - y) ≤ r}.card ≤ r / δ + 1

Left-arc count: at most r/δ + 1 well-spaced points satisfy fract(x−y) ≤ r.

theorem AnalyticNumberTheory.LargeSieve.wellSpaced_fract_right_card_le (X : Finset ℝ) {δ : ℝ} (hδ : 0 < δ) (hws : wellSpacedReal X δ) (x : ℝ) {r : ℝ} (hr : 0 ≤ r) : ↑{y ∈ X | 1 - Int.fract (x - y) ≤ r}.card ≤ r / δ + 1

Right-arc count: at most r/δ + 1 well-spaced points satisfy 1 − fract(x−y) ≤ r.

theorem AnalyticNumberTheory.LargeSieve.wellSpaced_ball_card_le (X : Finset ℝ) {δ : ℝ} (hδ : 0 < δ) (hws : wellSpacedReal X δ) (x : ℝ) {r : ℝ} (hr0 : 0 ≤ r) (_hr1 : r ≤ 1 / 2) : ↑{y ∈ X | distToInt (x - y) ≤ r}.card ≤ 2 * r / δ + 2

Ball count modulo 1: a ball of radius r ≤ 1/2 contains at most 2r/δ + 2 well-spaced points. Split fractional parts into left and right intervals, each containing at most r/δ + 1 points.

3. Interval-kernel properties and dyadic-shell row sums

theorem AnalyticNumberTheory.LargeSieve.charReal_zero : charReal 0 = 1

e(0) = 1.

theorem AnalyticNumberTheory.LargeSieve.charRealSubIcc_zero (M : ℤ) (N : ℕ) : charRealSubIcc M N 0 = ↑N

The interval exponential sum at zero: Σ_{M<n≤M+N} e(n·0) = N.

theorem AnalyticNumberTheory.LargeSieve.charRealSubIcc_neg (M : ℤ) (N : ℕ) (z : ℝ) : charRealSubIcc M N (-z) = star (charRealSubIcc M N z)

Conjugation of the interval kernel: Σ_n e(n·(−z)) = conj(Σ_n e(nz)).

theorem AnalyticNumberTheory.LargeSieve.charRealSubIcc_norm_sym (M : ℤ) (N : ℕ) (x y : ℝ) : ‖charRealSubIcc M N (x - y)‖ = ‖charRealSubIcc M N (y - x)‖

Kernel norm symmetry: |Σ_n e(n(x−y))| = |Σ_n e(n(y−x))|.

theorem AnalyticNumberTheory.LargeSieve.shell_geom_bound {ρ : ℝ} (hρ0 : 0 < ρ) (hρ : ρ ≤ 1 / 2) {J : ℕ} (hJ : (1 / 2) ^ J < ρ) : 1 / (2 * ρ) ≤ ∑ j ∈ Finset.Icc 2 J, 2 ^ (j - 1) * if ρ ≤ (1 / 2) ^ (j - 1) then 1 else 0

Pointwise shell bound: if 0 < ρ ≤ 1/2 and (1/2)^J < ρ, then 1/(2ρ) ≤ Σ_{2≤j≤J} 2^{j-1}·1_{ρ ≤ (1/2)^{j-1}}. Choose the least k with (1/2)^k < ρ. Then 2 ≤ k ≤ J, 1/(2ρ) < 2^{k-1}, and every shell index j ∈ [2,k] contributes.

theorem AnalyticNumberTheory.LargeSieve.half_pow_mul_two_pow (m : ℕ) : (1 / 2) ^ m * 2 ^ m = 1

(1/2)^m · 2^m = 1.

theorem AnalyticNumberTheory.LargeSieve.half_pow_le_half {m : ℕ} (hm : 1 ≤ m) : (1 / 2) ^ m ≤ 1 / 2

(1/2)^m ≤ 1/2 for 1 ≤ m.

3½. The weaker constant and log₂ lemmas

noncomputable def AnalyticNumberTheory.LargeSieve.largeSieveBound (N : ℕ) (δ : ℝ) : ℝ

Weaker additive large-sieve constant: C(N,δ) = N + (2⌈log₂(1/δ)⌉+12)/δ, with a natural-number ceiling. This is explicit; the logarithmic factor is the cost of naive dyadic-shell counting and the Schur test. The sharp N + 1/δ requires a positive-kernel argument not supplied here.

Equations

• AnalyticNumberTheory.LargeSieve.largeSieveBound N δ = ↑N + (2 * ↑⌈Real.log (1 / δ) / Real.log 2⌉₊ + 12) / δ

theorem AnalyticNumberTheory.LargeSieve.largeSieveBound_nonneg (N : ℕ) {δ : ℝ} (hδ : 0 < δ) : 0 ≤ largeSieveBound N δ

theorem AnalyticNumberTheory.LargeSieve.log2_ceil_half_lt {δ : ℝ} (hδ : 0 < δ) (_hδ1 : δ ≤ 1) : (1 / 2) ^ (⌈Real.log (1 / δ) / Real.log 2⌉₊ + 1) < δ

K := ⌈log₂(1/δ)⌉ satisfies (1/2)^{K+1} < δ for 0 < δ ≤ 1.

theorem AnalyticNumberTheory.LargeSieve.log2_ceil_two_pow_lt {δ : ℝ} (hδ : 0 < δ) (hδ1 : δ ≤ 1) : 2 ^ ⌈Real.log (1 / δ) / Real.log 2⌉₊ < 2 / δ

K := ⌈log₂(1/δ)⌉ satisfies 2^K < 2/δ for 0 < δ ≤ 1.

theorem AnalyticNumberTheory.LargeSieve.wellSpacedRowSum (M : ℤ) (N : ℕ) {δ : ℝ} (hδ : 0 < δ) (X : Finset ℝ) (hws : wellSpacedReal X δ) (x : ℝ) (hx : x ∈ X) : ∑ y ∈ X, ‖charRealSubIcc M N (x - y)‖ ≤ largeSieveBound N δ

Dyadic-shell row sum (weaker constant): for a δ-well-spaced set X modulo 1 and fixed x ∈ X, Σ_{y∈X} |Σ_{M<n≤M+N} e(n(x−y))| ≤ N + (2K+12)/δ, where K = ⌈log₂(1/δ)⌉. The logarithmic factor is the cost of the naive Schur test.

4. The Schur test and the additive large sieve

theorem AnalyticNumberTheory.LargeSieve.quadraticFormBound {ι : Type u_1} (s : Finset ι) (K : ι → ι → ℂ) (b : ι → ℂ) {C : ℝ} (hC : 0 ≤ C) (hsym : ∀ x ∈ s, ∀ y ∈ s, ‖K x y‖ = ‖K y x‖) (hrow : ∀ x ∈ s, ∑ y ∈ s, ‖K x y‖ ≤ C) : ‖∑ x ∈ s, ∑ y ∈ s, b x * star (b y) * K x y‖ ≤ C * ∑ x ∈ s, ‖b x‖ ^ 2

Schur/Cauchy--Schwarz test: if the kernel has symmetric norms (|K xy| = |K yx|, as for a Hermitian kernel) and row sums at most C, then |Σ_x Σ_y b_x·conj(b_y)·K_xy| ≤ C·Σ_x |b_x|². Use the triangle inequality and Cauchy--Schwarz for the complex bilinear form on the product Finset.

theorem AnalyticNumberTheory.LargeSieve.largeSieveDual_wellSpaced (M : ℤ) (N : ℕ) {δ : ℝ} (hδ : 0 < δ) (X : Finset ℝ) (hws : wellSpacedReal X δ) (b : ℝ → ℂ) : ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖∑ x ∈ X, star (charReal (↑n * x)) * b x‖ ^ 2 ≤ largeSieveBound N δ * ∑ x ∈ X, ‖b x‖ ^ 2

Dual additive large sieve (real version, weaker constant): for a δ-well-spaced set X modulo 1, Σ_{M<n≤M+N} |Σ_{x∈X} conj(e(nx))·b_x|² ≤ C(N,δ)·Σ_{x∈X} |b_x|².

theorem AnalyticNumberTheory.LargeSieve.largeSievePrimal_wellSpaced (M : ℤ) (N : ℕ) {δ : ℝ} (hδ : 0 < δ) (X : Finset ℝ) (hws : wellSpacedReal X δ) (a : ℤ → ℂ) : ∑ x ∈ X, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), charReal (↑n * x) * a n‖ ^ 2 ≤ largeSieveBound N δ * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖a n‖ ^ 2

Additive large sieve (real version, weaker constant): for a δ-well-spaced set X modulo 1 and any finitely supported complex sequence a, the primal bound is Σ_{x∈X} |Σ_{M<n≤M+N} a_n·e(nx)|² ≤ C(N,δ)·Σ_n |a_n|². It follows from the dual bound by largeSieveDuality.