A common moving product cutoff

The profile depends on the source coordinate, but not on the conductor or character. Its Mellin coefficient is an entire function of the spectral parameter; it is not treated as a constant when shifting a contour.

noncomputable def Wu2004MeanValue.movingCoefficient (f : ℕ → ℂ) (v : ℕ → ℕ) (x : ℕ) (s : ℂ) (a : ℕ) : ℂ

Equations

• Wu2004MeanValue.movingCoefficient f v x s a = f a * ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep (v a) / MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep x) ^ s

theorem Wu2004MeanValue.movingCoefficient_norm_le (f : ℕ → ℂ) (v : ℕ → ℕ) (x : ℕ) (hf : ∀ (a : ℕ), ‖f a‖ ≤ 1) (hv : ∀ (a : ℕ), v a ≤ x) {s : ℂ} (hs : 0 ≤ s.re) (a : ℕ) : ‖movingCoefficient f v x s a‖ ≤ 1

theorem Wu2004MeanValue.movingCoefficient_differentiable (f : ℕ → ℂ) (v : ℕ → ℕ) (x a : ℕ) : Differentiable ℂ fun (s : ℂ) => movingCoefficient f v x s a

theorem Wu2004MeanValue.movingCoefficient_power (f : ℕ → ℂ) (v : ℕ → ℕ) (x a : ℕ) (s : ℂ) : movingCoefficient f v x s a * ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep x) ^ s = f a * ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep (v a)) ^ s

noncomputable def Wu2004MeanValue.movingAmplitude {q : ℕ} (A B : ℕ → ℂ) (v : ℕ → ℕ) (L U : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) : ℂ

Equations

• Wu2004MeanValue.movingAmplitude A B v L U χ = ∑ a ∈ Finset.Ioc L U, A a * ↑χ ↑a * ∑ n ∈ Finset.Icc 1 (v a / a), B n * ↑χ ↑n

noncomputable def Wu2004MeanValue.movingPerronIntegral {q : ℕ} (S V : Finset ℕ) (A B : ℕ → ℂ) (v : ℕ → ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (σ T : ℝ) : ℂ

Equations

• Wu2004MeanValue.movingPerronIntegral S V A B v χ σ T = ∑ a ∈ S, MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronIntegral {a} V A B (↑χ) σ T (v a)

theorem Wu2004MeanValue.movingAmplitude_eq_hyperbolas {q : ℕ} (A B : ℕ → ℂ) (v : ℕ → ℕ) (L U M : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (hv : ∀ a ∈ Finset.Ioc L U, v a ≤ M) : movingAmplitude A B v L U χ = ∑ a ∈ Finset.Ioc L U, MathlibNt.SieveTheory.LiuWeight.liuPanPerronHyperbolaSum {a} (Finset.Icc 1 M) A B (↑χ) (v a)

theorem Wu2004MeanValue.moving_error_le_harmonic {q x : ℕ} {T : ℝ} (S V : Finset ℕ) (A B : ℕ → ℂ) (v : ℕ → ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (hS : ∀ a ∈ S, 0 < a) (hV : ∀ n ∈ V, 0 < n) (hA : ∀ a ∈ S, ‖A a‖ ≤ 1) (hB : ∀ n ∈ V, ‖B n‖ ≤ 1) (hx : 1 ≤ Real.log ↑x) (hv : ∀ a ∈ S, 1 ≤ v a ∧ v a ≤ x) (hT : 0 < T) : ‖∑ a ∈ S, MathlibNt.SieveTheory.LiuWeight.liuPanPerronHyperbolaSum {a} V A B (↑χ) (v a) - movingPerronIntegral S V A B v χ (AnalyticNumberTheory.LargeSieve.panSourceSigma x) T‖ ≤ (108 * ↑x ^ 3 / T * ∑ a ∈ S, (↑a)⁻¹) * ∑ n ∈ V, (↑n)⁻¹

Only the truncation remainder is estimated rowwise; reciprocal product weights are retained even at the exponential prime cutoff.

theorem Wu2004MeanValue.moving_amplitude_perron {q x : ℕ} (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (v : ℕ → ℕ) (m L U : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (hx : 4 ≤ Real.log ↑x) (hv : ∀ a ∈ Finset.Ioc L U, 1 ≤ v a ∧ v a ≤ x) (hUx : U ≤ x) : ‖movingAmplitude (AnalyticNumberTheory.LargeSieve.panSourceG f m) (AnalyticNumberTheory.LargeSieve.panSourceD m) v L U χ - movingPerronIntegral (Finset.Ioc L U) (Finset.Icc 1 ⌊AnalyticNumberTheory.LargeSieve.panSourceHeight x⌋₊) (AnalyticNumberTheory.LargeSieve.panSourceG f m) (AnalyticNumberTheory.LargeSieve.panSourceD m) v χ (AnalyticNumberTheory.LargeSieve.panSourceSigma x) (AnalyticNumberTheory.LargeSieve.panSourceHeight x)‖ ≤ 324 * (↑x ^ 2)⁻¹

Genuine Perron truncation for arbitrary source-coordinate cutoffs, with the same inverse-square error as the fixed-cutoff producer.

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

Equations

• Wu2004MeanValue.movingG f v x m A₁ A₂ k χ s = AnalyticNumberTheory.LargeSieve.panDyadicG (Wu2004MeanValue.movingCoefficient f v x s) m A₁ A₂ k χ s

theorem Wu2004MeanValue.movingG_differentiable {q : ℕ} (f : ℕ → ℂ) (v : ℕ → ℕ) (x m A₁ A₂ k : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) : Differentiable ℂ (movingG f v x m A₁ A₂ k χ)

The actual moving source polynomial is entire. In particular, its spectral coefficient is differentiated rather than frozen.