theorem AnalyticNumberTheory.LargeSieve.totient_block_sum_le_weighted (D Q : ℕ) (hD : 0 < D) (A : ℕ → ℝ) (hA : ∀ (q : ℕ), 0 ≤ A q) : ∑ q ∈ Finset.Ioc D Q, 1 / ↑q.totient * A q ≤ (∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * A q) / ↑D

theorem AnalyticNumberTheory.LargeSieve.primitiveLValue_differentiable (q : ℕ) (χ : PrimitiveCharacter q) : Differentiable ℂ fun (z : ℂ) => chen1973PrimitiveLValue q z χ

theorem AnalyticNumberTheory.LargeSieve.primitiveLValue_deriv (q : ℕ) (χ : PrimitiveCharacter q) (s : ℂ) : deriv (fun (z : ℂ) => chen1973PrimitiveLValue q z χ) s = chen1973PrimitiveLDeriv q s χ

theorem AnalyticNumberTheory.LargeSieve.primitive_LDeriv_fourth_block_cauchy (D Q : ℕ) (s : ℂ) (r M : ℝ) (hD : 0 < D) (hQ : 2 ≤ Q) (hr : 0 < r) (hsphere : ∀ z ∈ Metric.sphere s r, Chen1973Lemma3Domain z z.re z.im) (hnorm : ∀ z ∈ Metric.sphere s r, ‖z‖ ≤ M) : ∑ q ∈ Finset.Ioc D Q, 1 / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖chen1973PrimitiveLDeriv q s χ‖ ^ 4 ≤ 21000000 * ↑Q ^ 2 * M ^ 2 * (1 + Real.log (↑Q * (1 + M))) ^ 4 / ↑D / r ^ 4

Actual primitive L-functions: the reciprocal-totient block fourth moment on a circle is controlled before applying Cauchy to the whole finite ℓ⁴ family.

theorem AnalyticNumberTheory.LargeSieve.primitive_LDeriv_fourth_block_vertical (D Q : ℕ) (σ t r : ℝ) (hD : 0 < D) (hQ : 2 ≤ Q) (hr : 0 < r) (hband : 1 / 2 ≤ σ - r) : ∑ q ∈ Finset.Ioc D Q, 1 / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖chen1973PrimitiveLDeriv q (↑σ + ↑t * Complex.I) χ‖ ^ 4 ≤ 21000000 * ↑Q ^ 2 * (|σ| + |t| + r) ^ 2 * (1 + Real.log (↑Q * (1 + (|σ| + |t| + r)))) ^ 4 / ↑D / r ^ 4

All heights, with the circle hypotheses derived from the actual band. The conductor cost is Q²/D, not an extra count of individual characters.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_LDeriv_fourth_aggregate (x L level D Q : ℕ) (σ t r : ℝ) (hD : 0 < D) (hQ : 2 ≤ Q) (hr : 0 < r) (hband : 1 / 2 ≤ σ - r) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : chen1973Lemma6Eq19LDerivFourthMoment x L level (↑σ + ↑t * Complex.I) ≤ chen1973Lemma6Eq19I x L level * (21000000 * ↑Q ^ 2 * (|σ| + |t| + r) ^ 2 * (1 + Real.log (↑Q * (1 + (|σ| + |t| + r)))) ^ 4 / ↑D / r ^ 4)

Actual equation-(19) conductor weights applied only after the aggregate reciprocal-totient bound. The logarithm is kept, not enlarged to a conductor power.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_LDeriv_fourth_beta (x L level D Q : ℕ) (hx : 3 ≤ x) (hD : 0 < D) (hQ : 2 ≤ Q) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) (t : ℝ) : have β := chen1973Lemma6Beta x; have r := 1 / (2 * Real.log ↑x); chen1973Lemma6Eq19LDerivFourthMoment x L level (↑β + ↑t * Complex.I) ≤ chen1973Lemma6Eq19I x L level * (21000000 * ↑Q ^ 2 * (|β| + |t| + r) ^ 2 * (1 + Real.log (↑Q * (1 + (|β| + |t| + r)))) ^ 4 / ↑D / r ^ 4)

Chen's actual beta line, with the Cauchy radius and band paid internally.