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
Instances For
theorem
AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.perronLine_verticalSection
(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_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_height_ge_fifth
{x : ℕ}
(hx : 4 ≤ Real.log ↑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)
Instances For
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.