Chen 1973, Lemma 2: primitive-character large sieve

This is a source module for the lemma printed on pp. 113--114 of Chen's 1973 paper. The definitions and theorem statements below retain the paper's exact objects: the interval M < n ≤ M + N, primitive characters, the weights q / φ(q) and 1 / φ(q), and the constant X² + π N in equation (2).

The proof on pp. 113--114 has two layers. First, disjoint intervals around the reduced Farey fractions give equation (4), the sharp additive estimate with constant X² + π N. Gauss inversion and character orthogonality then give (2). Finally the source partitions D < q ≤ Q into the cells 2^i D < q ≤ 2^(i+1) D and obtains (3).

The already-proved Gauss/Farey orthogonality layer is reused literally. The remaining source-calculus sentence (equation (4), whose sharp constant is not provided by the repository's weaker logarithmic largeSieveBound) is exposed as Chen1973FareyEquationFour; it is not replaced by the weaker bound.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973ExponentialSum (a : ℤ → ℝ) (M : ℤ) (N : ℕ) (α : ℝ) : ℂ

Chen p. 113: S(α) = ∑_{n=M+1}^{M+N} a_n e(nα).

Equations

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

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973CoefficientEnergy (a : ℤ → ℝ) (M : ℤ) (N : ℕ) : ℝ

Chen p. 113: Z = ∑_{n=M+1}^{M+N} |a_n|².

Equations

• AnalyticNumberTheory.LargeSieve.chen1973CoefficientEnergy a M N = ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), |a n| ^ 2

theorem AnalyticNumberTheory.LargeSieve.charReal_intervalIntegral_int (k : ℤ) (u : ℝ) : ∫ (x : ℝ) in u..u + 1, charReal (↑k * x) = if k = 0 then 1 else 0

theorem AnalyticNumberTheory.LargeSieve.chen1973_fourier_parseval (s : Finset ℤ) (b : ℤ → ℂ) (u : ℝ) : ∫ (x : ℝ) in u..u + 1, ‖∑ n ∈ s, b n * charReal (↑n * x)‖ ^ 2 = ∑ n ∈ s, ‖b n‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.chen1973_fourier_parseval_shift (s : Finset ℤ) (b : ℤ → ℂ) (τ u : ℝ) : ∫ (x : ℝ) in u..u + 1, ‖∑ n ∈ s, b n * charReal ((↑n - τ) * x)‖ ^ 2 = ∑ n ∈ s, ‖b n‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973PrimitiveAmplitude (a : ℤ → ℝ) (M : ℤ) (N q : ℕ) (χ : PrimitiveCharacter q) : ℂ

The character amplitude occurring verbatim in equations (2) and (3).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973PrimitiveAmplitude a M N q χ = ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ↑(a n) * ↑χ ↑n

def AnalyticNumberTheory.LargeSieve.Chen1973FareyEquationFour : Prop

Chen pp. 113--114, equation (4): the sharp reduced-Farey additive estimate. This is exactly the analytic sentence between the disjoint-interval argument and primitive Gauss inversion.

Equations

• AnalyticNumberTheory.LargeSieve.Chen1973FareyEquationFour = ∀ (a : ℤ → ℝ) (M : ℤ) (N X : ℕ), ∑ qa ∈ AnalyticNumberTheory.LargeSieve.reducedFareyIndices X, ‖AnalyticNumberTheory.LargeSieve.chen1973ExponentialSum a M N (AnalyticNumberTheory.LargeSieve.reducedFareyPoint qa)‖ ^ 2 ≤ (↑X ^ 2 + Real.pi * ↑N) * AnalyticNumberTheory.LargeSieve.chen1973CoefficientEnergy a M N

theorem AnalyticNumberTheory.LargeSieve.chen1973FareyEquationFour : Chen1973FareyEquationFour

Unconditional closure of Chen's sharp Farey estimate, equation (4).

def AnalyticNumberTheory.LargeSieve.Chen1973Lemma2EquationTwo : Prop

Chen p. 113, equation (2), as one literal proposition.

Equations

• AnalyticNumberTheory.LargeSieve.Chen1973Lemma2EquationTwo = ∀ (a : ℤ → ℝ) (M : ℤ) (N X : ℕ), ∑ q ∈ Finset.Icc 1 X, ↑q / ↑q.totient * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.chen1973PrimitiveAmplitude a M N q χ‖ ^ 2 ≤ (↑X ^ 2 + Real.pi * ↑N) * AnalyticNumberTheory.LargeSieve.chen1973CoefficientEnergy a M N

def AnalyticNumberTheory.LargeSieve.Chen1973Lemma2EquationThree : Prop

Chen p. 113, equation (3), with the Vinogradov constant made explicit and its source dependence preserved: one absolute constant works uniformly for a, M, N, D, Q.

Equations

• AnalyticNumberTheory.LargeSieve.Chen1973Lemma2EquationThree = ∃ (C : ℝ), 0 < C ∧ ∀ (a : ℤ → ℝ) (M : ℤ) (N D Q : ℕ), 0 < D → ∑ q ∈ Finset.Ioc D Q, 1 / ↑q.totient * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.chen1973PrimitiveAmplitude a M N q χ‖ ^ 2 ≤ C * (↑Q + ↑N / ↑D) * AnalyticNumberTheory.LargeSieve.chen1973CoefficientEnergy a M N

@[simp]

theorem AnalyticNumberTheory.LargeSieve.chen1973PrimitiveAmplitude_eq_intervalAmplitude (a : ℤ → ℝ) (M : ℤ) (N q : ℕ) (χ : PrimitiveCharacter q) : chen1973PrimitiveAmplitude a M N q χ = primitiveIntervalAmplitude (fun (n : ℤ) => ↑(a n)) M N χ

@[simp]

theorem AnalyticNumberTheory.LargeSieve.chen1973CoefficientEnergy_eq_norm_energy (a : ℤ → ℝ) (M : ℤ) (N : ℕ) : chen1973CoefficientEnergy a M N = ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖↑(a n)‖ ^ 2

@[simp]

theorem AnalyticNumberTheory.LargeSieve.chen1973ExponentialSum_eq_reducedAdditiveAmplitude (a : ℤ → ℝ) (M : ℤ) (N q r : ℕ) : chen1973ExponentialSum a M N (↑r / ↑q) = reducedAdditiveAmplitude q (fun (n : ℤ) => ↑(a n)) M N r

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma2_equationTwo_of_fareyEquationFour (h4 : Chen1973FareyEquationFour) : Chen1973Lemma2EquationTwo

Source sentence after (4), pp. 113--114: Gauss inversion plus primitive character orthogonality turns the sharp reduced-Farey estimate into (2). The final conclusion is the literal equation-(2) proposition.

The dyadic modulus decomposition used for equation (3)

def AnalyticNumberTheory.LargeSieve.chen1973ModulusCell (D Q k : ℕ) : Finset ℕ

The source cell 2^k D < q ≤ 2^(k+1)D, intersected with (D,Q].

Equations

• AnalyticNumberTheory.LargeSieve.chen1973ModulusCell D Q k = {q ∈ Finset.Ioc D Q | ((q - 1) / D).log2 = k}

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_chen1973ModulusCell {D Q k q : ℕ} : q ∈ chen1973ModulusCell D Q k ↔ D < q ∧ q ≤ Q ∧ ((q - 1) / D).log2 = k

theorem AnalyticNumberTheory.LargeSieve.chen1973ModulusCell_bounds {D Q k q : ℕ} (hD : 0 < D) (hq : q ∈ chen1973ModulusCell D Q k) : 2 ^ k * D < q ∧ q ≤ 2 ^ (k + 1) * D

A modulus in the kth cell lies in the literal source interval 2^k D < q ≤ 2^(k+1)D.

theorem AnalyticNumberTheory.LargeSieve.chen1973ModulusCell_index_lt {D Q k q : ℕ} (hD : 0 < D) (hq : q ∈ chen1973ModulusCell D Q k) : k < ((Q - 1) / D).log2 + 1

The chosen cell index is bounded by the last cell meeting (D,Q].

theorem AnalyticNumberTheory.LargeSieve.sum_chen1973ModulusCell {R : Type u_1} [AddCommMonoid R] (D Q : ℕ) (hD : 0 < D) (f : ℕ → R) : ∑ k ∈ Finset.range (((Q - 1) / D).log2 + 1), ∑ q ∈ chen1973ModulusCell D Q k, f q = ∑ q ∈ Finset.Ioc D Q, f q

The dyadic cells partition the complete source interval (D,Q].

theorem AnalyticNumberTheory.LargeSieve.chen1973EquationThree_cell_le (h2 : Chen1973Lemma2EquationTwo) (a : ℤ → ℝ) (M : ℤ) (N D Q k : ℕ) (hD : 0 < D) : ∑ q ∈ chen1973ModulusCell D Q k, 1 / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖chen1973PrimitiveAmplitude a M N q χ‖ ^ 2 ≤ (4 * ↑(2 ^ k * D) + Real.pi * ↑N / ↑(2 ^ k * D)) * chen1973CoefficientEnergy a M N

One source dyadic cell, obtained from (2) at cutoff 2^(k+1)D and the pointwise inequality 1/q ≤ 1/(2^k D).

theorem AnalyticNumberTheory.LargeSieve.sum_range_two_pow (K : ℕ) : ∑ k ∈ Finset.range K, ↑(2 ^ k) = 2 ^ K - 1

Finite geometric identity used in Chen's dyadic summation.

theorem AnalyticNumberTheory.LargeSieve.sum_range_inv_two_pow_le_two (K : ℕ) : ∑ k ∈ Finset.range K, (1 / 2) ^ k ≤ 2

The reciprocal dyadic tail has total mass at most two.

theorem AnalyticNumberTheory.LargeSieve.chen1973_dyadic_scalar_sum_le (N D Q : ℕ) (hD : 0 < D) (hDQ : D < Q) : have K := ((Q - 1) / D).log2 + 1; ∑ k ∈ Finset.range K, (4 * ↑(2 ^ k * D) + Real.pi * ↑N / ↑(2 ^ k * D)) ≤ 8 * ↑Q + 2 * Real.pi * ↑N / ↑D

The exact geometric payment in the proof of (3). The two source sums are bounded respectively by 8Q and 2πN/D.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma2_equationThree_of_equationTwo (h2 : Chen1973Lemma2EquationTwo) : Chen1973Lemma2EquationThree

Chen p. 114: summing the dyadic cells proves equation (3). We exhibit the absolute constant 8 + 2π; the printed ≪ only records existence of such a constant and has no dependence on a, M, N, D, or Q.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma2_of_fareyEquationFour (h4 : Chen1973FareyEquationFour) : Chen1973Lemma2EquationTwo ∧ Chen1973Lemma2EquationThree

Chen's complete Lemma 2 reduction: the sharp Farey equation (4) gives the literal primitive equation (2), and its dyadic summation gives (3).