theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_powerTail {a T : ℝ} (hT : 0 < T) (N : ℕ) (hN : 0 < N) : MeasureTheory.IntegrableOn (fun (t : ℝ) => a ^ N / t ^ (N + 1)) (Set.Ioi T) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Ioi T, a ^ N / t ^ (N + 1) = (a / T) ^ N / ↑N

Exact arbitrary-cutoff tail moment: the cutoff cost is retained.

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_tail_norm_bound {f : ℝ → ℂ} {a T C : ℝ} (hT : 0 < T) (N : ℕ) (hN : 0 < N) (hf : MeasureTheory.IntegrableOn f (Set.Ioi T) MeasureTheory.volume) (hpoint : ∀ t ∈ Set.Ioi T, ‖f t‖ ≤ C * (a ^ N / t ^ (N + 1))) : ‖∫ (t : ℝ) in Set.Ioi T, f t‖ ≤ C * ((a / T) ^ N / ↑N)

A pointwise true-power majorant yields a genuine tail budget.

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_term_norm_le {x d : ℕ} (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hy : 0 < ↑x / (↑pp.1 * ↑pp.2)) {s : ℂ} {M : ℝ} (hderiv : ‖chen1973PrimitiveLDeriv d s χ / chen1973Lemma6PrimitiveLValue d s χ‖ ≤ M) : ‖chen1973Lemma6Eq21TermShiftIntegrand x d χ pp s‖ ≤ (↑x / (↑pp.1 * ↑pp.2)) ^ s.re * ‖chen1973MellinKernel (↑x) s‖ * M

Pointwise norm estimate for the actual character-weighted term.

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_kernel_tail_abs {x : ℕ} (hx : 1 < x) {v t : ℝ} (ht : 0 < |t|) : ‖chen1973MellinKernel (↑x) (↑v + ↑t * Complex.I)‖ ≤ chen1973PerronScale ↑x ^ (chen1973PerronOrder ↑x + 1) / |t| ^ (chen1973PerronOrder ↑x + 2)

Lossless kernel tail on either sign of the imaginary coordinate.

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_alpha_tails {x d : ℕ} (hx : 3 ≤ x) (hd : 1 < d) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hy : 0 < ↑x / (↑pp.1 * ↑pp.2)) {T : ℝ} (hT : 0 < T) : have F := chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Alpha x); have a := chen1973PerronScale ↑x; have N := chen1973PerronOrder ↑x + 1; have C := 6 * Real.log ↑x ^ 2 * (↑x / (↑pp.1 * ↑pp.2)) ^ chen1973Lemma6Alpha x; ‖∫ (t : ℝ) in Set.Iio (-T), F t‖ ≤ C * ((a / T) ^ N / ↑N) ∧ ‖∫ (t : ℝ) in Set.Ioi T, F t‖ ≤ C * ((a / T) ^ N / ↑N)

Both actual alpha tails separately satisfy the sharp arbitrary-cutoff budget.

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_horizontal_bound {x d : ℕ} (hx : 3 ≤ x) (hd : 1 < d) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) (hy : 1 < ↑x / (↑pp.1 * ↑pp.2)) {T M : ℝ} (hT : 0 < T) (hM : 0 ≤ M) (hzero : ∀ (s : ℂ), chen1973Lemma6Eq21Sigma x ≤ s.re → s.re ≤ chen1973Lemma6Alpha x → |s.im| ≤ T → chen1973Lemma6PrimitiveLValue d s χ ≠ 0) (hderiv : ∀ (s : ℂ), chen1973Lemma6Eq21Sigma x ≤ s.re → s.re ≤ chen1973Lemma6Alpha x → |s.im| ≤ T → ‖chen1973PrimitiveLDeriv d s χ / chen1973Lemma6PrimitiveLValue d s χ‖ ≤ M) : ‖chen1973HorizontalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x) (chen1973Lemma6Alpha x) T‖ ≤ 2 * (chen1973Lemma6Alpha x - chen1973Lemma6Eq21Sigma x) * M * (↑x / (↑pp.1 * ↑pp.2)) ^ chen1973Lemma6Alpha x * (chen1973PerronScale ↑x / T) ^ (chen1973PerronOrder ↑x + 1) / T

Each horizontal edge is paid at the selected height, not via an infinite-height limit.

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_kernel_le_inv {x : ℕ} (hx : 1 < x) {σ t b : ℝ} (hσ : 0 ≤ σ) (hb : 0 < b) (hbs : b ≤ ‖↑σ + ↑t * Complex.I‖) : ‖chen1973MellinKernel (↑x) (↑σ + ↑t * Complex.I)‖ ≤ b⁻¹

Discard only the smoothing factor; this is not a radial replacement.

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_kernel_short {x : ℕ} (hx : 3 ≤ x) {σ T : ℝ} (hσ : 0 < σ) (hT : 1 ≤ T) : ∫ (t : ℝ) in -T..T, ‖chen1973MellinKernel (↑x) (↑σ + ↑t * Complex.I)‖ ≤ 2 * (σ⁻¹ + Real.log T)

The short true kernel costs only twice (inverse real part plus log height).

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_short_term_bound {x d : ℕ} (hx : 3 ≤ x) (hd : 1 < d) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) (hy : 0 < ↑x / (↑pp.1 * ↑pp.2)) {T M : ℝ} (hT : 1 ≤ T) (hM : 0 ≤ M) (hzero : ∀ (s : ℂ), chen1973Lemma6Eq21Sigma x ≤ s.re → s.re ≤ chen1973Lemma6Alpha x → |s.im| ≤ T → chen1973Lemma6PrimitiveLValue d s χ ≠ 0) (hderiv : ∀ (s : ℂ), chen1973Lemma6Eq21Sigma x ≤ s.re → s.re ≤ chen1973Lemma6Alpha x → |s.im| ≤ T → ‖chen1973PrimitiveLDeriv d s χ / chen1973Lemma6PrimitiveLValue d s χ‖ ≤ M) : ‖∫ (t : ℝ) in -T..T, chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x) t‖ ≤ 2 * (↑x / (↑pp.1 * ↑pp.2)) ^ chen1973Lemma6Eq21Sigma x * M * ((chen1973Lemma6Eq21Sigma x)⁻¹ + Real.log T)

Actual short sigma edge, requiring the log derivative only in the finite rectangle.

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_truncated_term_bound {x d : ℕ} (hx : 3 ≤ x) (hd : 1 < d) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) (hy : 1 < ↑x / (↑pp.1 * ↑pp.2)) {T M : ℝ} (hT : 1 ≤ T) (hM : 0 ≤ M) (hzero : ∀ (s : ℂ), chen1973Lemma6Eq21Sigma x ≤ s.re → s.re ≤ chen1973Lemma6Alpha x → |s.im| ≤ T → chen1973Lemma6PrimitiveLValue d s χ ≠ 0) (hderiv : ∀ (s : ℂ), chen1973Lemma6Eq21Sigma x ≤ s.re → s.re ≤ chen1973Lemma6Alpha x → |s.im| ≤ T → ‖chen1973PrimitiveLDeriv d s χ / chen1973Lemma6PrimitiveLValue d s χ‖ ≤ M) : have y := ↑x / (↑pp.1 * ↑pp.2); have σ := chen1973Lemma6Eq21Sigma x; have α := chen1973Lemma6Alpha x; have a := chen1973PerronScale ↑x; have N := chen1973PerronOrder ↑x + 1; ‖chen1973Lemma6ActualPhi x d χ pp * ↑χ ↑(pp.1 * pp.2)‖ / Real.log y ≤ y ^ σ * M * (σ⁻¹ + Real.log T) / (Real.pi * Real.log y) + y ^ α / (Real.pi * Real.log y) * (a / T) ^ N * (6 * Real.log ↑x ^ 2 / ↑N + (α - σ) * M / T)

W3 (star): complete finite-contour bound on the actual Phi term. The only analytic inputs concern the finite rectangle. The alpha tails are unconditional and retain the complete production smoothing order.