The half-step variant of the finite shift in Pan (2.23)

The cutoff is y + 1/2, while both finite polynomials retain their complete source coefficients. This is a boundary-safe variant, not a transcription of the natural-cutoff integral. No Perron truncation estimate is assumed here.

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

The complete short-polynomial kernel at the real half-step cutoff.

Equations

• AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepShortKernel f m H y A₁ A₂ k χ s = AnalyticNumberTheory.LargeSieve.panDyadicG f m A₁ A₂ k χ s * AnalyticNumberTheory.LargeSieve.panShortF₁ m H χ s * ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep y) ^ s / s

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStep_pos (y : ℕ) : 0 < MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep y

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.perronLine_verticalSection (F : ℂ → ℂ) (σ t : ℝ) : F (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t) = chen1973VerticalSection F σ t

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

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepShortKernel_oriented_rectangle {q : ℕ} (f : ℕ → ℂ) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) {α T : ℝ} (hα : 1 / 2 ≤ α) (hT : 0 ≤ T) : (Complex.I * ∫ (t : ℝ) in -T..T, halfStepShortKernel f m H y A₁ A₂ k χ (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine α t)) - Complex.I * ∫ (t : ℝ) in -T..T, halfStepShortKernel f m H y A₁ A₂ k χ (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine (1 / 2) t) = (∫ (u : ℝ) in 1 / 2..α, halfStepShortKernel f m H y A₁ A₂ k χ (↑u + ↑T * Complex.I)) - ∫ (u : ℝ) in 1 / 2..α, halfStepShortKernel f m H y A₁ A₂ k χ (↑u + -↑T * Complex.I)

Exact rectangle identity, with the actual differential ds = i dt.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepShortKernel_vertical_integrable {q : ℕ} (f : ℕ → ℂ) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) {α T v : ℝ} (hT : 0 ≤ T) (hv : v ∈ Set.Icc (1 / 2) α) : IntervalIntegrable (fun (t : ℝ) => halfStepShortKernel f m H y A₁ A₂ k χ (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine v t)) MeasureTheory.volume (-T) T

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

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepShortKernel_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) : ‖halfStepShortKernel f m H y A₁ A₂ k χ (↑u + ↑t * Complex.I)‖ ≤ MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep y ^ α / T * panHalfSum H * panHalfSum A₂

Pointwise bounds use the actual source and prime polynomials.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepShortKernel_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..α, halfStepShortKernel f m H y A₁ A₂ k χ (↑u + ↑t * Complex.I)‖ ≤ MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep y ^ α / T * panHalfSum H * panHalfSum A₂ * (α - 1 / 2)

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepShortKernel_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) : ‖(∫ (t : ℝ) in -T..T, halfStepShortKernel f m H y A₁ A₂ k χ (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine α t)) - ∫ (t : ℝ) in -T..T, halfStepShortKernel f m H y A₁ A₂ k χ (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine (1 / 2) t)‖ ≤ 2 * (α - 1 / 2) * MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep y ^ α / T * panHalfSum H * panHalfSum A₂

The finite shift before any specialization of the height.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStep_source_power_le {x y : ℕ} (hx : 1 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) : MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep y ^ panSourceSigma x ≤ 4 * ↑x ^ 2

A deliberately crude power bound sufficient at the exponential height.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStep_source_height_ge_fifth {x : ℕ} (hx : 4 ≤ Real.log ↑x) : ↑x ^ 5 ≤ panSourceHeight x

This retains exactly exp (2 log² x); the fifth power merely bounds it.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepShortKernel_source_inverse_square {q x : ℕ} (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (hx : 4 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) (hAy : A₂ ≤ y) (hHx : H ≤ x) : ‖(∫ (t : ℝ) in -panSourceHeight x..panSourceHeight x, halfStepShortKernel f m H y A₁ A₂ k χ (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine (panSourceSigma x) t)) - ∫ (t : ℝ) in -panSourceHeight x..panSourceHeight x, halfStepShortKernel f m H y A₁ A₂ k χ (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine (1 / 2) t)‖ ≤ 64 / ↑x ^ 2

Uniform unnormalized error for the actual full-polynomial contour shift.

noncomputable def AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepShortIntegral {q : ℕ} (f : ℕ → ℂ) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (σ T : ℝ) : ℂ

The normalized dt integral, equivalently (2πi)⁻¹ ∫ kernel(s) ds.

Equations

• AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepShortIntegral f m H y A₁ A₂ k χ σ T = (↑(2 * Real.pi))⁻¹ * ∫ (t : ℝ) in -T..T, AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepShortKernel f m H y A₁ A₂ k χ (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t)

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStepShortIntegral_source_inverse_square {q x : ℕ} (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m H y A₁ A₂ k : ℕ) (χ : PrimitiveCharacter q) (hx : 4 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) (hAy : A₂ ≤ y) (hHx : H ≤ x) : ‖halfStepShortIntegral f m H y A₁ A₂ k χ (panSourceSigma x) (panSourceHeight x) - halfStepShortIntegral f m H y A₁ A₂ k χ (1 / 2) (panSourceHeight x)‖ ≤ 64 / ↑x ^ 2

The normalized half-step shift has the same absolute constant 64.