theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_one_le_perronScale {x : ℕ} (hx : 3 ≤ x) : 1 ≤ chen1973PerronScale ↑x

The literal scale is at least one at the explicit cutoff.

theorem AnalyticNumberTheory.LargeSieve.eq21_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⁻¹

Discarding only the smoothing factor, not changing the actual kernel.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_weightedKernel_head_middle {x : ℕ} (hx : 3 ≤ x) {d σ : ℝ} (hd : 1 ≤ d) (hσ : 0 < σ) (r : ℕ) : have a := chen1973PerronScale ↑x; have D := 1 + Real.log (d * (1 + a)); have f := fun (t : ℝ) => ‖chen1973MellinKernel (↑x) (↑σ + ↑t * Complex.I)‖ * (1 + Real.log (d * (1 + t))) ^ r; MeasureTheory.IntegrableOn f (Set.Ioc 0 1) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn f (Set.Ioc 1 a) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Ioc 0 1, f t ≤ σ⁻¹ * D ^ r ∧ ∫ (t : ℝ) in Set.Ioc 1 a, f t ≤ Real.log a * D ^ r

Head and middle intervals, with their separate sharp elementary budgets.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_mellinKernel_norm_neg (x σ t : ℝ) : ‖chen1973MellinKernel x (↑σ + -↑t * Complex.I)‖ = ‖chen1973MellinKernel x (↑σ + ↑t * Complex.I)‖

Complex conjugation proves the norm is even on a vertical line.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_weightedKernel_positive_integrable_and_bound {x : ℕ} (hx : 3 ≤ x) {d σ : ℝ} (hd : 1 ≤ d) (hσ : 0 < σ) (r : ℕ) : have a := chen1973PerronScale ↑x; have N := chen1973PerronOrder ↑x + 1; have D := 1 + Real.log (d * (1 + a)); have f := fun (t : ℝ) => ‖chen1973MellinKernel (↑x) (↑σ + ↑t * Complex.I)‖ * (1 + Real.log (d * (1 + t))) ^ r; MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Ioi 0, f t ≤ (σ⁻¹ + Real.log a) * D ^ r + ∑ j ∈ Finset.range (r + 1), ↑(r.choose j) * D ^ (r - j) * (↑j.factorial / ↑N ^ (j + 1))

Positive ray assembled from head, middle and the already-proved exact tail.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_weightedKernel_full_integrable_and_bound {x : ℕ} (hx : 3 ≤ x) {d σ : ℝ} (hd : 1 ≤ d) (hσ : 0 < σ) (r : ℕ) : have a := chen1973PerronScale ↑x; have N := chen1973PerronOrder ↑x + 1; have D := 1 + Real.log (d * (1 + a)); have f := fun (t : ℝ) => ‖chen1973MellinKernel (↑x) (↑σ + ↑t * Complex.I)‖ * (1 + Real.log (d * (1 + |t|))) ^ r; MeasureTheory.Integrable f MeasureTheory.volume ∧ ∫ (t : ℝ), f t ≤ 2 * ((σ⁻¹ + Real.log a) * D ^ r + ∑ j ∈ Finset.range (r + 1), ↑(r.choose j) * D ^ (r - j) * (↑j.factorial / ↑N ^ (j + 1)))

Full real-line weighted norm budget for the actual Mellin kernel. This is a kernel estimate only, not a logarithmic-derivative estimate or an unconditional version of equation (21).