Source coefficients and the literal kernel

def AnalyticNumberTheory.LargeSieve.panSourceG (f : ℕ → ℂ) (m n : ℕ) : ℂ

Equation (2.8), with the original coprimality restriction.

Equations

• AnalyticNumberTheory.LargeSieve.panSourceG f m n = if n.Coprime m then f n else 0

def AnalyticNumberTheory.LargeSieve.panSourceD (m n : ℕ) : ℂ

Equations (2.2), (2.8): the prime indicator restricted by (n,m)=1.

Equations

• AnalyticNumberTheory.LargeSieve.panSourceD m n = if n.Coprime m ∧ Nat.Prime n then 1 else 0

noncomputable def AnalyticNumberTheory.LargeSieve.panShortF₁ {q : ℕ} (m H : ℕ) (χ : PrimitiveCharacter q) (s : ℂ) : ℂ

The literal short polynomial (2.19).

Equations

• AnalyticNumberTheory.LargeSieve.panShortF₁ m H χ s = ∑ n ∈ Finset.Icc 1 H, AnalyticNumberTheory.LargeSieve.panSourceD m n * ↑χ ↑n / ↑n ^ s

noncomputable def AnalyticNumberTheory.LargeSieve.panDyadicG {q : ℕ} (f : ℕ → ℂ) (m A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (s : ℂ) : ℂ

Equation (2.21), including the clipped last dyadic cell.

Equations

• AnalyticNumberTheory.LargeSieve.panDyadicG f m A₁ A₂ k χ s = ∑ a ∈ Finset.Ioc (2 ^ k * A₁) (min (2 ^ (k + 1) * A₁) A₂), AnalyticNumberTheory.LargeSieve.panSourceG f m a * ↑χ ↑a / ↑a ^ s

noncomputable def AnalyticNumberTheory.LargeSieve.pan223Kernel {q : ℕ} (f : ℕ → ℂ) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (s : ℂ) : ℂ

The complete kernel in (2.23), not an abstract holomorphic input.

Equations

• AnalyticNumberTheory.LargeSieve.pan223Kernel f m H y A₁ A₂ k χ s = AnalyticNumberTheory.LargeSieve.panDyadicG f m A₁ A₂ k χ s * AnalyticNumberTheory.LargeSieve.panShortF₁ m H χ s * ↑y ^ s / s

Analyticity and the oriented rectangle identity

theorem AnalyticNumberTheory.LargeSieve.panFinitePolynomial_differentiable (S : Finset ℕ) (c : ℕ → ℂ) (hS : ∀ n ∈ S, 0 < n) : Differentiable ℂ fun (s : ℂ) => ∑ n ∈ S, c n / ↑n ^ s

theorem AnalyticNumberTheory.LargeSieve.panShortF₁_differentiable {q : ℕ} (m H : ℕ) (χ : PrimitiveCharacter q) : Differentiable ℂ (panShortF₁ m H χ)

theorem AnalyticNumberTheory.LargeSieve.panDyadicG_differentiable {q : ℕ} (f : ℕ → ℂ) (m A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) : Differentiable ℂ (panDyadicG f m A₁ A₂ k χ)

theorem AnalyticNumberTheory.LargeSieve.pan223Kernel_differentiableOn {q : ℕ} (f : ℕ → ℂ) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (hy : 0 < y) : DifferentiableOn ℂ (pan223Kernel f m H y A₁ A₂ k χ) {s : ℂ | 0 < s.re}

theorem AnalyticNumberTheory.LargeSieve.pan223_oriented_rectangle {q : ℕ} (f : ℕ → ℂ) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (hy : 0 < y) {α T : ℝ} (hα : 1 / 2 ≤ α) (hT : 0 ≤ T) : (Complex.I * ∫ (t : ℝ) in -T..T, chen1973VerticalSection (pan223Kernel f m H y A₁ A₂ k χ) α t) - Complex.I * ∫ (t : ℝ) in -T..T, chen1973VerticalSection (pan223Kernel f m H y A₁ A₂ k χ) (1 / 2) t = (∫ (u : ℝ) in 1 / 2..α, pan223Kernel f m H y A₁ A₂ k χ (↑u + ↑T * Complex.I)) - ∫ (u : ℝ) in 1 / 2..α, pan223Kernel f m H y A₁ A₂ k χ (↑u + -↑T * Complex.I)

Exact finite shift with actual ds = i dt. The top edge is traversed left-to-right and the bottom edge right-to-left in the difference.

Coefficient, half-sum, and horizontal pointwise bounds

theorem AnalyticNumberTheory.LargeSieve.panSourceG_norm_le (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m n : ℕ) : ‖panSourceG f m n‖ ≤ 1

theorem AnalyticNumberTheory.LargeSieve.panSourceD_norm_le (m n : ℕ) : ‖panSourceD m n‖ ≤ 1

noncomputable def AnalyticNumberTheory.LargeSieve.panHalfSum (N : ℕ) : ℝ

The precise reciprocal-square-root sum in (2.23).

Equations

• AnalyticNumberTheory.LargeSieve.panHalfSum N = ∑ n ∈ Finset.Icc 1 N, (√↑n)⁻¹

theorem AnalyticNumberTheory.LargeSieve.panHalfSum_eq_rpow (N : ℕ) : panHalfSum N = ∑ n ∈ Finset.Icc 1 N, ↑n ^ (-(1 / 2))

theorem AnalyticNumberTheory.LargeSieve.panHalfSum_nonneg (N : ℕ) : 0 ≤ panHalfSum N

theorem AnalyticNumberTheory.LargeSieve.panFinitePolynomial_norm_le (S : Finset ℕ) (c : ℕ → ℂ) (N : ℕ) (hS : S ⊆ Finset.Icc 1 N) (hc : ∀ n ∈ S, ‖c n‖ ≤ 1) (s : ℂ) (hs : 1 / 2 ≤ s.re) : ‖∑ n ∈ S, c n / ↑n ^ s‖ ≤ panHalfSum N

theorem AnalyticNumberTheory.LargeSieve.panShortF₁_norm_le {q : ℕ} (m H : ℕ) (χ : PrimitiveCharacter q) (s : ℂ) (hs : 1 / 2 ≤ s.re) : ‖panShortF₁ m H χ s‖ ≤ panHalfSum H

theorem AnalyticNumberTheory.LargeSieve.panDyadicG_norm_le {q : ℕ} (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (s : ℂ) (hs : 1 / 2 ≤ s.re) : ‖panDyadicG f m A₁ A₂ k χ s‖ ≤ panHalfSum A₂

theorem AnalyticNumberTheory.LargeSieve.pan223_horizontal_pointwise {q : ℕ} (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (hy : 1 ≤ y) {α T u t : ℝ} (hu : 1 / 2 ≤ u) (huα : u ≤ α) (hT : 0 < T) (ht : |t| = T) : ‖pan223Kernel f m H y A₁ A₂ k χ (↑u + ↑t * Complex.I)‖ ≤ ↑y ^ α / T * panHalfSum H * panHalfSum A₂

Pointwise estimate on either horizontal edge, uniform in all characters and dyadic cells.

Integrability and the finite-shift estimate

theorem AnalyticNumberTheory.LargeSieve.pan223_vertical_integrable {q : ℕ} (f : ℕ → ℂ) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (hy : 0 < y) {α T v : ℝ} (hT : 0 ≤ T) (hv : v ∈ Set.Icc (1 / 2) α) : IntervalIntegrable (chen1973VerticalSection (pan223Kernel f m H y A₁ A₂ k χ) v) MeasureTheory.volume (-T) T

Both vertical sections are genuine finite integrals.

theorem AnalyticNumberTheory.LargeSieve.pan223_horizontal_integrable {q : ℕ} (f : ℕ → ℂ) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (hy : 0 < y) {α t : ℝ} (hα : 1 / 2 ≤ α) : IntervalIntegrable (fun (u : ℝ) => pan223Kernel f m H y A₁ A₂ k χ (↑u + ↑t * Complex.I)) MeasureTheory.volume (1 / 2) α

Both horizontal integrals exist independently of the contour identity.

theorem AnalyticNumberTheory.LargeSieve.pan223_horizontal_integral_bound {q : ℕ} (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (hy : 1 ≤ y) {α T t : ℝ} (hα : 1 / 2 ≤ α) (hT : 0 < T) (ht : |t| = T) : ‖∫ (u : ℝ) in 1 / 2..α, pan223Kernel f m H y A₁ A₂ k χ (↑u + ↑t * Complex.I)‖ ≤ ↑y ^ α / T * panHalfSum H * panHalfSum A₂ * (α - 1 / 2)

Each horizontal edge separately has the original half-sum bound.

theorem AnalyticNumberTheory.LargeSieve.pan223_finite_shift_bound {q : ℕ} (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (hy : 1 ≤ y) {α T : ℝ} (hα : 1 / 2 ≤ α) (hT : 0 < T) : ‖(Complex.I * ∫ (t : ℝ) in -T..T, chen1973VerticalSection (pan223Kernel f m H y A₁ A₂ k χ) α t) - Complex.I * ∫ (t : ℝ) in -T..T, chen1973VerticalSection (pan223Kernel f m H y A₁ A₂ k χ) (1 / 2) t‖ ≤ 2 * (α - 1 / 2) * ↑y ^ α / T * panHalfSum H * panHalfSum A₂

Finite-shift bound, retaining exactly the half-sums displayed in (2.23).