Pan's long-polynomial primitive mean

On Re s ≥ 1, bounded coefficients have inverse-square energy. Apply the sharp primitive large sieve to complete dyadic polynomials, then sum the long-polynomial blocks. The source polynomial is never split into absolute values of individual source coefficients.

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

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.long_block_mean_le (S T : Finset ℕ) (c d : ℕ → ℂ) (A L V : ℕ) (hA : 0 < A) (hAL : A ≤ L) (hS : S ⊆ Finset.Ioc L (2 * L)) (hT : T ⊆ Finset.Ioc V (2 * V)) (hc : ∀ n ∈ S, ‖c n‖ ≤ 1) (hd : ∀ n ∈ T, ‖d n‖ ≤ 1) {R : ℝ} (hR : 1 ≤ R) (hHV : shortCutoff R ≤ V) (s : ℂ) (hs : 1 ≤ s.re) : ∑ q ∈ conductorCell R, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ‖polynomial S c χ s * polynomial T d χ s‖ ≤ 8 * chen1973Lemma6Eq19SharpConstant * √(1 / ↑A + 1 / ↑(shortCutoff R))

Each complete long dyadic block has the paper's square-root reciprocal scale, including the factor needed to account for H = floor(R²).

noncomputable def AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.longF₂ {q : ℕ} (m H : ℕ) (T : ℝ) (χ : PrimitiveCharacter q) (s : ℂ) : ℂ

Equations

• AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.longF₂ m H T χ s = AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.polynomial (Finset.Ioc H ⌊T⌋₊) (AnalyticNumberTheory.LargeSieve.panSourceD m) χ s

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

Equations

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

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.mem_long_interval_iff (R : ℝ) {T : ℝ} (hT : 0 ≤ T) (n : ℕ) : n ∈ Finset.Ioc (shortCutoff R) ⌊T⌋₊ ↔ R ^ 2 < ↑n ∧ ↑n ≤ T

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.polynomial_eq_sum_dyadic (c : ℕ → ℂ) (H K : ℕ) (hH : 0 < H) {q : ℕ} (χ : PrimitiveCharacter q) (s : ℂ) : polynomial (Finset.Ioc H K) c χ s = ∑ r ∈ Finset.range (panDyadicDepth H K), polynomial (panDyadicCell H K r) c χ s

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.longMean_le (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m A₁ A₂ k : ℕ) (hA : 0 < A₁) {R : ℝ} (hR : 1 ≤ R) (T : ℝ) (s : ℂ) (hs : 1 ≤ s.re) : longMean f m A₁ A₂ k R T s ≤ ↑(panDyadicDepth (shortCutoff R) ⌊T⌋₊) * (8 * chen1973Lemma6Eq19SharpConstant * √(1 / ↑A₁ + 1 / ↑(shortCutoff R)))

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.depth_at_source_height_le (H x : ℕ) (hx : 1 ≤ Real.log ↑x) : ↑(panDyadicDepth H ⌊panSourceHeight x⌋₊) ≤ (1 + 2 / Real.log 2) * Real.log ↑x ^ 2

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.longMean_at_source_height_le (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m A₁ A₂ k x : ℕ) (hA : 0 < A₁) (hx : 1 ≤ Real.log ↑x) {R : ℝ} (hR : 1 ≤ R) (s : ℂ) (hs : 1 ≤ s.re) : longMean f m A₁ A₂ k R (panSourceHeight x) s ≤ 8 * chen1973Lemma6Eq19SharpConstant * (1 + 2 / Real.log 2) * Real.log ↑x ^ 2 * √(1 / ↑A₁ + 1 / ↑(shortCutoff R))

The dyadic block count through the literal height exp(2 log² x) costs only O(log² x), with no source- or conductor-dependent constant.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.source_reciprocal_scale_le (x y A₁ j : ℕ) {B : ℝ} (hB : 0 ≤ B) (hy : 1 ≤ Real.log ↑y) (hyx : y ≤ x) (hA : Real.log ↑y ^ (2 * B) ≤ ↑A₁) : √(1 / ↑A₁ + 1 / ↑(shortCutoff (conductorRadius x B j))) ≤ 2 / Real.log ↑y ^ B

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.chosen_long_mean_uniform : ∃ (C : ℝ), 0 < C ∧ ∀ (B : ℝ) (x y j m A₁ A₂ k : ℕ) (f : ℕ → ℂ) (s : ℂ), 0 ≤ B → 1 ≤ Real.log ↑y → y ≤ x → Real.log ↑y ^ (2 * B) ≤ ↑A₁ → (∀ (n : ℕ), ‖f n‖ ≤ 1) → 1 ≤ s.re → longMean f m A₁ A₂ k (conductorRadius x B j) (panSourceHeight x) s ≤ C * Real.log ↑x ^ 2 / Real.log ↑y ^ B

The long-polynomial estimate (2.28), retaining the original log y lower source cutoff and the log² x cost of the literal height.