The real cutoff in Pan--Wang--Ding (2.26)

On printed pp. 600 and 603 the parameters are D₁ = log(x)^B, D = sqrt(x)/log(x)^B, and H = (2^j D₁)^2. The integer endpoint of the short polynomial is the floor of the real square, not the square of a rounded conductor. The conductor interval is open on the left and closed on the right, including at integral endpoints.

noncomputable def AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.lowConductor (x : ℕ) (B : ℝ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.lowConductor x B = Real.log ↑x ^ B

noncomputable def AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.upperConductor (x : ℕ) (B : ℝ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.upperConductor x B = √↑x / AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.lowConductor x B

noncomputable def AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.conductorRadius (x : ℕ) (B : ℝ) (j : ℕ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.conductorRadius x B j = 2 ^ j * AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.lowConductor x B

noncomputable def AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.shortCutoff (R : ℝ) : ℕ

Equations

• AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.shortCutoff R = ⌊R ^ 2⌋₊

noncomputable def AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.conductorCell (R : ℝ) : Finset ℕ

Equations

• AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.conductorCell R = Finset.Ioc ⌊R⌋₊ ⌊2 * R⌋₊

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.mem_conductorCell_iff {R : ℝ} (hR : 0 ≤ R) (q : ℕ) : q ∈ conductorCell R ↔ R < ↑q ∧ ↑q ≤ 2 * R

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.le_shortCutoff_iff (R : ℝ) (n : ℕ) : n ≤ shortCutoff R ↔ ↑n ≤ R ^ 2

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.mem_shortCutoff_iff (R : ℝ) (n : ℕ) : n ∈ Finset.Icc 1 (shortCutoff R) ↔ 1 ≤ n ∧ ↑n ≤ R ^ 2

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.shortCutoff_le_square (R : ℝ) : ↑(shortCutoff R) ≤ R ^ 2

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.square_lt_shortCutoff_add_one (R : ℝ) : R ^ 2 < ↑(shortCutoff R) + 1

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.shortCutoff_pos {R : ℝ} (hR : 1 ≤ R) : 1 ≤ shortCutoff R

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.square_le_two_mul_shortCutoff {R : ℝ} (hR : 1 ≤ R) : R ^ 2 ≤ 2 * ↑(shortCutoff R)

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.radius_le_two_mul_floor {R : ℝ} (hR : 1 ≤ R) : R ≤ 2 * ↑⌊R⌋₊

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.lowConductor_ge_one {x : ℕ} {B : ℝ} (hx : 1 ≤ Real.log ↑x) (hB : 0 ≤ B) : 1 ≤ lowConductor x B

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.conductorRadius_ge_one {x : ℕ} {B : ℝ} (j : ℕ) (hx : 1 ≤ Real.log ↑x) (hB : 0 ≤ B) : 1 ≤ conductorRadius x B j

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.upperConductor_square (x : ℕ) (B : ℝ) : upperConductor x B ^ 2 = ↑x / lowConductor x B ^ 2

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.upperConductor_le_sqrt {x : ℕ} {B : ℝ} (hx : 1 ≤ Real.log ↑x) (hB : 0 ≤ B) : upperConductor x B ≤ √↑x

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.shortCutoff_le_x {x : ℕ} {B R : ℝ} (hx : 1 ≤ Real.log ↑x) (hB : 0 ≤ B) (hR : 0 ≤ R) (hRD : R ≤ upperConductor x B) : shortCutoff R ≤ x

The hypothesis required by the proved contour displacement follows from the actual active-cell inequality, uniformly in the cell index.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.shortCutoff_lt_height {x : ℕ} {B R : ℝ} (hx : 2 ≤ Real.log ↑x) (hB : 0 ≤ B) (hR : 0 ≤ R) (hRD : R ≤ upperConductor x B) : ↑(shortCutoff R) < panSourceHeight x

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.panShortF₁_eq_real_cutoff {q : ℕ} (m x : ℕ) (R : ℝ) (hH : shortCutoff R ≤ x) (χ : PrimitiveCharacter q) (s : ℂ) : panShortF₁ m (shortCutoff R) χ s = ∑ n ∈ Finset.Icc 1 x with ↑n ≤ R ^ 2, panSourceD m n * ↑χ ↑n / ↑n ^ s

The literal short polynomial is exactly the sum over n ≤ R². The extra ambient bound is only a finite enumeration device.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.chosen_short_contour_uniform : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℕ), ∀ (x : ℕ), X₀ ≤ x → ∀ (B : ℝ) (j q : ℕ) (χ : PrimitiveCharacter q) (m y A₁ A₂ k : ℕ) (f : ℕ → ℂ), 0 ≤ B → conductorRadius x B j ≤ upperConductor x B → (∀ (n : ℕ), ‖f n‖ ≤ 1) → 1 ≤ y → y ≤ x → A₂ ≤ y → ‖(Complex.I * ∫ (t : ℝ) in -panSourceHeight x..panSourceHeight x, chen1973VerticalSection (pan223Kernel f m (shortCutoff (conductorRadius x B j)) y A₁ A₂ k χ) (panSourceSigma x) t) - Complex.I * ∫ (t : ℝ) in -panSourceHeight x..panSourceHeight x, chen1973VerticalSection (pan223Kernel f m (shortCutoff (conductorRadius x B j)) y A₁ A₂ k χ) (1 / 2) t‖ ≤ C * (↑x ^ 2)⁻¹

The constant and threshold precede the real exponent, conductor cell, character, all source cutoffs, and bounded coefficients.