noncomputable def AnalyticNumberTheory.LargeSieve.panSourceSigma (x : ℕ) : ℝ

Literal (2.15) abscissa.

Equations

• AnalyticNumberTheory.LargeSieve.panSourceSigma x = 1 + 1 / Real.log ↑x

noncomputable def AnalyticNumberTheory.LargeSieve.panSourceHeight (x : ℕ) : ℝ

Literal (2.16) height.

Equations

• AnalyticNumberTheory.LargeSieve.panSourceHeight x = Real.exp (2 * Real.log ↑x ^ 2)

theorem AnalyticNumberTheory.LargeSieve.panHalfSum_le (N : ℕ) : panHalfSum N ≤ 2 * √↑N

Elementary telescoping majorant for the sum appearing in (2.23).

theorem AnalyticNumberTheory.LargeSieve.panSourceSigma_bounds {x : ℕ} (hx : 1 ≤ Real.log ↑x) : 1 / 2 ≤ panSourceSigma x ∧ panSourceSigma x ≤ 2

theorem AnalyticNumberTheory.LargeSieve.panSourceSigma_power_le {x y : ℕ} (hx : 1 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) : ↑y ^ panSourceSigma x ≤ Real.exp 1 * ↑y

theorem AnalyticNumberTheory.LargeSieve.panSourceHeight_ge_fourth {x : ℕ} (hx : 2 ≤ Real.log ↑x) : ↑x ^ 4 ≤ panSourceHeight x

The original height dominates x^4 once log x ≥ 2; no change of T.

theorem AnalyticNumberTheory.LargeSieve.pan223_source_halfsum_bound {q x : ℕ} (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (hx : 1 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) : ‖(Complex.I * ∫ (t : ℝ) in -panSourceHeight x..panSourceHeight x, chen1973VerticalSection (pan223Kernel f m H y A₁ A₂ k χ) (panSourceSigma x) t) - Complex.I * ∫ (t : ℝ) in -panSourceHeight x..panSourceHeight x, chen1973VerticalSection (pan223Kernel f m H y A₁ A₂ k χ) (1 / 2) t‖ ≤ 4 * Real.exp 1 * ↑y / panSourceHeight x * panHalfSum H * panHalfSum A₂

First displayed O-term in (2.23), with one absolute constant.

theorem AnalyticNumberTheory.LargeSieve.pan223_source_sqrt_bound {q x : ℕ} (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (hx : 1 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) (hAy : A₂ ≤ y) : ‖(Complex.I * ∫ (t : ℝ) in -panSourceHeight x..panSourceHeight x, chen1973VerticalSection (pan223Kernel f m H y A₁ A₂ k χ) (panSourceSigma x) t) - Complex.I * ∫ (t : ℝ) in -panSourceHeight x..panSourceHeight x, chen1973VerticalSection (pan223Kernel f m H y A₁ A₂ k χ) (1 / 2) t‖ ≤ 16 * Real.exp 1 * (↑y * √↑y) * √↑H / panSourceHeight x

Second displayed O-term of (2.23); y * sqrt y is y^(3/2).

theorem AnalyticNumberTheory.LargeSieve.pan_y_mul_sqrt (y : ℕ) (hy : 0 < y) : ↑y * √↑y = ↑y ^ (3 / 2)

y * sqrt y is precisely the source exponent, not a weaker surrogate.

theorem AnalyticNumberTheory.LargeSieve.pan223_source_inverse_square {q x : ℕ} (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (hx : 2 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) (hAy : A₂ ≤ y) (hHx : H ≤ x) : ‖(Complex.I * ∫ (t : ℝ) in -panSourceHeight x..panSourceHeight x, chen1973VerticalSection (pan223Kernel f m H y A₁ A₂ k χ) (panSourceSigma x) t) - Complex.I * ∫ (t : ℝ) in -panSourceHeight x..panSourceHeight x, chen1973VerticalSection (pan223Kernel f m H y A₁ A₂ k χ) (1 / 2) t‖ ≤ 16 * Real.exp 1 * (↑x ^ 2)⁻¹

Last O-term in (2.23). The hypothesis H ≤ x is explicit; this does not claim to have substituted the later choice H=(2^j log^B x)^2.

theorem AnalyticNumberTheory.LargeSieve.pan223_source_three_halves_bound {q x : ℕ} (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (hx : 1 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) (hAy : A₂ ≤ y) : ‖(Complex.I * ∫ (t : ℝ) in -panSourceHeight x..panSourceHeight x, chen1973VerticalSection (pan223Kernel f m H y A₁ A₂ k χ) (panSourceSigma x) t) - Complex.I * ∫ (t : ℝ) in -panSourceHeight x..panSourceHeight x, chen1973VerticalSection (pan223Kernel f m H y A₁ A₂ k χ) (1 / 2) t‖ ≤ 16 * Real.exp 1 * ↑y ^ (3 / 2) * √↑H / panSourceHeight x

Literal y^(3/2) sqrt(H)/T rendering of the second bound.

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

Equation (2.23), uniform eventual form. The absolute constant and threshold precede q, the character, m, every cell, and the bounded coefficients. The bound in fact does not need the source's extra restriction 1 ≤ A₁.