The short-polynomial primitive mean in Pan (2.25)--(2.27)

The sharp primitive large sieve is applied to the complete source polynomial and the complete prime polynomial. Cauchy--Schwarz is applied across characters, not across the source coefficients. The fixed large-sieve constant is already proved and precedes all coefficients, spectral parameters, and real cutoffs.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.weighted_product_mean_le (S : Finset ℕ) (F G : (q : ℕ) → PrimitiveCharacter q → ℂ) : ∑ q ∈ S, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ‖F q χ * G q χ‖ ≤ √(∑ q ∈ S, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ‖F q χ‖ ^ 2) * √(∑ q ∈ S, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ‖G q χ‖ ^ 2)

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.primitive_square_moment_real_cell (c : ℤ → ℂ) (M : ℤ) (N : ℕ) {R : ℝ} (hR : 1 ≤ R) : ∑ q ∈ conductorCell R, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), c n * ↑χ ↑n‖ ^ 2 ≤ 2 * chen1973Lemma6Eq19SharpConstant * (R + ↑N / R) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖c n‖ ^ 2

Sharp Theorem A on the exact real cell R < q ≤ 2R.

noncomputable def AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.polynomial (S : Finset ℕ) (c : ℕ → ℂ) {q : ℕ} (χ : PrimitiveCharacter q) (s : ℂ) : ℂ

A finite Dirichlet polynomial with its complete coefficient sum intact.

Equations

• AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.polynomial S c χ s = ∑ n ∈ S, c n * ↑χ ↑n / ↑n ^ s

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.polynomial_second_moment_energy (S : Finset ℕ) (c : ℕ → ℂ) (N : ℕ) (hS : S ⊆ Finset.Icc 1 N) {R : ℝ} (hR : 1 ≤ R) (s : ℂ) : ∑ q ∈ conductorCell R, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ‖polynomial S c χ s‖ ^ 2 ≤ 2 * chen1973Lemma6Eq19SharpConstant * (R + ↑N / R) * ∑ n ∈ S, ‖c n / ↑n ^ s‖ ^ 2

The sharp large sieve with the exact finite polynomial energy.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.polynomial_second_moment (S : Finset ℕ) (c : ℕ → ℂ) (N : ℕ) (hS : S ⊆ Finset.Icc 1 N) (hc : ∀ n ∈ S, ‖c n‖ ≤ 1) {R : ℝ} (hR : 1 ≤ R) (s : ℂ) (hs : 1 / 2 ≤ s.re) : ∑ q ∈ conductorCell R, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ‖polynomial S c χ s‖ ^ 2 ≤ 2 * chen1973Lemma6Eq19SharpConstant * (R + ↑N / R) * ∑ n ∈ S, (↑n)⁻¹

Large sieve with the true harmonic coefficient energy on Re s ≥ 1/2.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.harmonic_energy_le_log (S : Finset ℕ) (x : ℕ) (hS : S ⊆ Finset.Icc 1 x) : ∑ n ∈ S, (↑n)⁻¹ ≤ 1 + Real.log ↑x

noncomputable def AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.shortMean (f : ℕ → ℂ) (m A₁ A₂ k : ℕ) (R : ℝ) (s : ℂ) : ℝ

The literal (2.22) short-polynomial mean, on the real conductor cell.

Equations

• AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.shortMean f m A₁ A₂ k R s = ∑ q ∈ AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.conductorCell R, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.panDyadicG f m A₁ A₂ k χ s * AnalyticNumberTheory.LargeSieve.panShortF₁ m (AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.shortCutoff R) χ s‖

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.shortMean_nonneg (f : ℕ → ℂ) (m A₁ A₂ k : ℕ) (R : ℝ) (s : ℂ) : 0 ≤ shortMean f m A₁ A₂ k R s

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.shortMean_le_sqrt_moments (f : ℕ → ℂ) (m A₁ A₂ k : ℕ) (R : ℝ) (s : ℂ) : shortMean f m A₁ A₂ k R s ≤ √(∑ q ∈ conductorCell R, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ‖panDyadicG f m A₁ A₂ k χ s‖ ^ 2) * √(∑ q ∈ conductorCell R, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ‖panShortF₁ m (shortCutoff R) χ s‖ ^ 2)

Equation (2.25), without a triangle inequality inside either polynomial.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.polynomial_product_mean_le (S T : Finset ℕ) (c d : ℕ → ℂ) (N H x : ℕ) (hS : S ⊆ Finset.Icc 1 N) (hT : T ⊆ Finset.Icc 1 H) (hc : ∀ n ∈ S, ‖c n‖ ≤ 1) (hd : ∀ n ∈ T, ‖d n‖ ≤ 1) (hNx : N ≤ x) (hHx : H ≤ x) (hx : 1 ≤ x) {R : ℝ} (hR : 1 ≤ R) (hH : ↑H ≤ R ^ 2) (s : ℂ) (hs : 1 / 2 ≤ s.re) : ∑ q ∈ conductorCell R, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ‖polynomial S c χ s * polynomial T d χ s‖ ≤ 4 * chen1973Lemma6Eq19SharpConstant * √(R ^ 2 + ↑N) * (1 + Real.log ↑x)

A general bounded-coefficient version of the short-polynomial estimate. The square-root saving comes from the conductor mean, not pointwise bounds.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.shortMean_le (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m A₁ A₂ k x : ℕ) (hAx : A₂ ≤ x) (hx : 1 ≤ x) {R : ℝ} (hR : 1 ≤ R) (hHx : shortCutoff R ≤ x) (s : ℂ) (hs : 1 / 2 ≤ s.re) : shortMean f m A₁ A₂ k R s ≤ 4 * chen1973Lemma6Eq19SharpConstant * √(R ^ 2 + ↑(min (2 ^ (k + 1) * A₁) A₂)) * (1 + Real.log ↑x)

Equation (2.27) at the exact cutoff (2.26), uniformly in the whole vertical line and in the bounded source. The clipped source-cell endpoint is retained.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.shortMean_le_log_scale (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m A₁ A₂ k x : ℕ) {B R : ℝ} (hB : 0 ≤ B) (hx : 1 ≤ Real.log ↑x) (hR : 1 ≤ R) (hRD : R ≤ upperConductor x B) (hA : ↑A₂ ≤ upperConductor x B ^ 2) (s : ℂ) (hs : 1 / 2 ≤ s.re) : shortMean f m A₁ A₂ k R s ≤ 16 * chen1973Lemma6Eq19SharpConstant * √↑x * Real.log ↑x ^ (1 - B)

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.eventually_power_le_upperConductor_square (B ε : ℝ) (hε : 0 < ε) : ∀ᶠ (x : ℕ) in Filter.atTop, ↑x ^ (1 - ε) ≤ upperConductor x B ^ 2

The source power cutoff is eventually inside the square of the chosen conductor ceiling. This is proved from logarithmic growth, not assumed.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.chosen_short_mean_uniform : ∃ (C : ℝ), 0 < C ∧ ∀ (B ε : ℝ), 0 ≤ B → 0 < ε → ∃ (X₀ : ℕ), ∀ (x : ℕ), X₀ ≤ x → ∀ (j m A₁ A₂ k : ℕ) (f : ℕ → ℂ) (s : ℂ), conductorRadius x B j ≤ upperConductor x B → ↑A₂ ≤ ↑x ^ (1 - ε) → (∀ (n : ℕ), ‖f n‖ ≤ 1) → 1 / 2 ≤ s.re → shortMean f m A₁ A₂ k (conductorRadius x B j) s ≤ C * √↑x * Real.log ↑x ^ (1 - B)

The source (2.27) saving, with an absolute constant chosen before B, ε, x, every dyadic cell, the source coefficients, and the spectral height.