The short moving kernel is shifted as a genuinely holomorphic function. Only its pointwise norm estimate uses the frozen-coefficient bound.

theorem Wu2004MeanValue.moving_short_finite_shift_bound {q x : ℕ} (f : ℕ → ℂ) (v : ℕ → ℕ) (hf : ∀ (a : ℕ), ‖f a‖ ≤ 1) (hv : ∀ (a : ℕ), v a ≤ x) (m H A₁ A₂ k : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (hx : 1 ≤ x) {α T : ℝ} (hα : 1 / 2 ≤ α) (hT : 0 < T) : ‖(∫ (t : ℝ) in -T..T, movingShortKernel f v x m H A₁ A₂ k χ (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine α t)) - ∫ (t : ℝ) in -T..T, movingShortKernel f v x m H A₁ A₂ k χ (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine (1 / 2) t)‖ ≤ 2 * (α - 1 / 2) * MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep x ^ α / T * AnalyticNumberTheory.LargeSieve.panHalfSum H * AnalyticNumberTheory.LargeSieve.panHalfSum A₂

Finite-height contour bound, uniform in a common moving profile.

theorem Wu2004MeanValue.moving_source_cell_perron_shift {q x : ℕ} (f : ℕ → ℂ) (v : ℕ → ℕ) (hf : ∀ (a : ℕ), ‖f a‖ ≤ 1) (hv : ∀ (a : ℕ), 1 ≤ v a ∧ v a ≤ x) (m H A₁ A₂ k : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (hx : 4 ≤ Real.log ↑x) (hAx : A₂ ≤ x) (hHx : H ≤ x) : ‖movingAmplitude (AnalyticNumberTheory.LargeSieve.panSourceG f m) (AnalyticNumberTheory.LargeSieve.panSourceD m) v (2 ^ k * A₁) (min (2 ^ (k + 1) * A₁) A₂) χ - (movingShortIntegral f v x m H A₁ A₂ k χ (1 / 2) (AnalyticNumberTheory.LargeSieve.panSourceHeight x) + movingLongIntegral f v x m H A₁ A₂ k χ (AnalyticNumberTheory.LargeSieve.panSourceSigma x) (AnalyticNumberTheory.LargeSieve.panSourceHeight x))‖ ≤ 388 / ↑x ^ 2

The complete moving source cell, with both Perron polynomials retained, has error 388/x² after shifting only the short kernel.