theorem Eq21FiniteLogDerivative.norm_primitive_logDeriv_le_of_zeroFree_rectangle {q : ℕ} (hq : 1 < q) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) {δ T : ℝ} (hδ : 0 < δ) (hδ1 : δ ≤ 1 / 4) (hT : 0 ≤ T) (hzero : ∀ (z : ℂ), 1 - δ ≤ z.re → z.re ≤ 2 → |z.im| ≤ T + 1 → AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue q z χ ≠ 0) (s : ℂ) (ht : |s.im| ≤ T) (hslo : 1 - δ / 2 ≤ s.re) (hshi : s.re ≤ 1 + δ) : ‖AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLDeriv q s χ / AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue q s χ‖ ≤ 40 / δ * Real.log (32 * ↑q * (1 + |s.im|) / δ)

The finite bound for the literal totalized primitive value/derivative pair.

theorem Eq21FiniteLogDerivative.norm_primitive_logDeriv_le_sqrt_budget {q : ℕ} (hq : 1 < q) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) {u : ℝ} (hu64 : 64 ≤ u) (hzero : ∀ (z : ℂ), 1 - 2 / √u ≤ z.re → z.re ≤ 2 → |z.im| ≤ u ^ 2 + 1 → AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue q z χ ≠ 0) (s : ℂ) (hslo : 1 - 1 / √u ≤ s.re) (hshi : s.re ≤ 1 + 1 / u) (ht : |s.im| ≤ u ^ 2) : ‖AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLDeriv q s χ / AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue q s χ‖ ≤ 20 * √u * Real.log (16 * ↑q * (1 + u ^ 2) * √u)

W4 with a real parameter u, width 2/sqrt u and finite height u².

theorem Eq21FiniteLogDerivative.chen1973Lemma6_eq21_logDeriv_on_finiteRectangle_of_zeroFree {x q : ℕ} (hq : 1 < q) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (hu64 : 64 ≤ Real.log ↑x) (hzero : ∀ (z : ℂ), 1 - 2 / √(Real.log ↑x) ≤ z.re → z.re ≤ 2 → |z.im| ≤ Real.log ↑x ^ 2 + 1 → AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue q z χ ≠ 0) (s : ℂ) (hslo : AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21Sigma x ≤ s.re) (hshi : s.re ≤ AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) (ht : |s.im| ≤ Real.log ↑x ^ 2) : ‖AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLDeriv q s χ / AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue q s χ‖ ≤ 20 * √(Real.log ↑x) * Real.log (16 * ↑q * (1 + Real.log ↑x ^ 2) * √(Real.log ↑x))

W4 at the actual Chen source parameters and the actual primitive quotient. The nonvanishing hypothesis is explicitly finite and has no shared input record.

theorem Eq21FiniteLogDerivative.sqrt_budget_le_uniform {q : ℕ} (hq : 1 < q) {u : ℝ} (hu : 1 ≤ u) (hqu : ↑q ≤ u ^ 100) : 20 * √u * Real.log (16 * ↑q * (1 + u ^ 2) * √u) ≤ 20 * √u * (Real.log 32 + 205 / 2 * Real.log u)

Uniform conductor payment; this is a scalar consequence, not a new analytic hypothesis.

theorem Eq21FiniteLogDerivative.norm_primitive_logDeriv_le_uniform {q : ℕ} (hq : 1 < q) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) {u : ℝ} (hu64 : 64 ≤ u) (hqu : ↑q ≤ u ^ 100) (hzero : ∀ (z : ℂ), 1 - 2 / √u ≤ z.re → z.re ≤ 2 → |z.im| ≤ u ^ 2 + 1 → AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue q z χ ≠ 0) (s : ℂ) (hslo : 1 - 1 / √u ≤ s.re) (hshi : s.re ≤ 1 + 1 / u) (ht : |s.im| ≤ u ^ 2) : ‖AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLDeriv q s χ / AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue q s χ‖ ≤ 20 * √u * (Real.log 32 + 205 / 2 * Real.log u)

The finite-rectangle actual primitive bound, uniform for q ≤ u^100.