Chen 1973, Lemma 6, equation (21): analytic payments

This disjoint leaf pays the finite low-conductor bookkeeping in the literal (log x)^200 contour estimate and isolates the genuinely analytic input at the primitive-character, prime-pair level. It also records a source-region prime sum decay with the exponential factor produced by the line Re s = 1 - 1 / sqrt(log x).

def AnalyticNumberTheory.LargeSieve.Chen1973Lemma6Eq21PrimitiveVerticalEstimate (Cvert : ℝ) (x L B k m : ℕ) : Prop

The remaining external analytic input for equation (21), stated at the primitive-character and individual prime-pair level. Its left side is the actual vertical integral, including the corrected high-power Mellin kernel. This is deliberately not an equation-(21) terminal bound.

Equations

• AnalyticNumberTheory.LargeSieve.Chen1973Lemma6Eq21PrimitiveVerticalEstimate Cvert x L B k m = (0 ≤ Cvert ∧ ∀ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L 0, ∀ (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d), ∀ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell x B k m, ‖↑(Real.log (↑x / (↑pp.1 * ↑pp.2)))⁻¹ * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21VerticalIntegral x d χ pp‖ ≤ Cvert * (↑x / (↑pp.1 * ↑pp.2)) ^ AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21Sigma x)

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21ConductorMass (x L : ℕ) : ℝ

Low-conductor weighted primitive-character mass.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21ConductorMass x L = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L 0, |↑(ArithmeticFunction.moebius d)| * 3 ^ d.primeFactors.card / ↑d * ↑(Fintype.card (AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d))

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_conductorMass_le (x L : ℕ) : chen1973Lemma6Eq21ConductorMass x L ≤ 2 * ↑L ^ 2

The literal level-zero conductor carrier costs at most 2 L². This uses both squarefreeness of the actual carrier and the finite count # primitive characters mod d ≤ φ(d) ≤ d.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_conductorMass_le_log200 {x L B k m l₂ : ℕ} (P : Chen1973Lemma6Eq21SourceParameters x L B k m l₂) : chen1973Lemma6Eq21ConductorMass x L ≤ 2 * Real.log ↑x ^ 200

The finite low-conductor mass is paid by the source's (log x)^200 once L ≤ (log x)^100.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_contour_le_log200_primeSum (Cvert : ℝ) {x L B k m l₂ : ℕ} (P : Chen1973Lemma6Eq21SourceParameters x L B k m l₂) (hregion : chen1973Lemma6PrimePairShell x B k m ⊆ chen1973Lemma6Eq21PrimeRegion x) (hvert : Chen1973Lemma6Eq21PrimitiveVerticalEstimate Cvert x L B k m) : chen1973Lemma6Eq21ContourMajorant x L B k m ≤ 2 * Cvert * Real.log ↑x ^ 200 * chen1973Lemma6Eq21PrimeSum x

The actual contour majorant is bounded by the actual prime-region sum. The only analytic premise is the narrow primitive vertical estimate above; all conductor and character counting is discharged in this theorem.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21PrimeReciprocalMass (x : ℕ) : ℝ

Reciprocal mass on the exact equation-(21) prime-pair region.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21PrimeReciprocalMass x = ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21PrimeRegion x, 1 / (↑pp.1 * ↑pp.2)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_primeReciprocalMass_bounded : ∃ (Cpair : ℝ), 0 ≤ Cpair ∧ ∀ (x : ℕ), 3 ≤ x → chen1973Lemma6Eq21PrimeReciprocalMass x ≤ Cpair

Mertens' theorem gives one absolute bound for the reciprocal mass of the actual equation-(21) pair region. The constraints coupling p₁ and p₂ are only discarded after embedding the actual region into its two source exponent rectangles.

def AnalyticNumberTheory.LargeSieve.Chen1973Lemma6Eq21PrimePointwiseDecay (x : ℕ) : Prop

Exact pointwise suppression required from the geometry of the printed prime region. It contains no characters and no contour integral.

Equations

• AnalyticNumberTheory.LargeSieve.Chen1973Lemma6Eq21PrimePointwiseDecay x = ∀ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21PrimeRegion x, (↑x / (↑pp.1 * ↑pp.2)) ^ AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21Sigma x ≤ ↑x * Real.exp (-√(Real.log ↑x) / 3) / (↑pp.1 * ↑pp.2)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_primePointwiseDecay {x : ℕ} (hx : 3 ≤ x) : Chen1973Lemma6Eq21PrimePointwiseDecay x

The literal prime region itself supplies the pointwise exponential suppression; no analytic estimate or conclusion-shaped premise is needed.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_primeSum_exponential_decay (Cpair : ℝ) (hmertens : ∀ (x : ℕ), 3 ≤ x → chen1973Lemma6Eq21PrimeReciprocalMass x ≤ Cpair) {x : ℕ} (hx : 3 ≤ x) : chen1973Lemma6Eq21PrimeSum x ≤ Cpair * ↑x * Real.exp (-√(Real.log ↑x) / 3)

Explicit exponential decay of the actual prime-pair sum. The reciprocal mass bound is supplied by Mertens; the pointwise decay is proved internally from the geometry of the literal source region.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_primeSum_log220_decay (Cpair : ℝ) (hmertens : ∀ (x : ℕ), 3 ≤ x → chen1973Lemma6Eq21PrimeReciprocalMass x ≤ Cpair) {x : ℕ} (hx : 3 ≤ x) (hlarge : Cpair * Real.exp (-√(Real.log ↑x) / 3) * Real.log ↑x ^ 220 ≤ 1) : chen1973Lemma6Eq21PrimeSum x ≤ ↑x / Real.log ↑x ^ 220

The explicit large-x scalar inequality that converts exponential suppression into the printed log^{-220} payment.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_eventually_exp_log220_le_one (Cpair : ℝ) : ∀ᶠ (x : ℕ) in Filter.atTop, Cpair * Real.exp (-√(Real.log ↑x) / 3) * Real.log ↑x ^ 220 ≤ 1

Exponential decay dominates the exact log^220 payment for every fixed constant. This theorem supplies the large-x threshold that was previously a pointwise scalar premise.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_primeSum_log220_decay_eventually (Cpair : ℝ) (hmertens : ∀ (x : ℕ), 3 ≤ x → chen1973Lemma6Eq21PrimeReciprocalMass x ≤ Cpair) : ∃ (x₀ : ℕ), ∀ x ≥ x₀, chen1973Lemma6Eq21PrimeSum x ≤ ↑x / Real.log ↑x ^ 220

Eventual equation-(21) prime-sum payment, with the scalar hlarge completely discharged and the cutoff quantified before x.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_contour_log20_decay_eventually (Cvert : ℝ) : ∃ (x₀ : ℕ), ∀ x ≥ x₀, ∀ (L B k m l₂ : ℕ), Chen1973Lemma6Eq21SourceParameters x L B k m l₂ → chen1973Lemma6PrimePairShell x B k m ⊆ chen1973Lemma6Eq21PrimeRegion x → Chen1973Lemma6Eq21PrimitiveVerticalEstimate Cvert x L B k m → chen1973Lemma6Eq21ContourMajorant x L B k m ≤ ↑x / Real.log ↑x ^ 20

Production analytic payment for equation (21). For a fixed constant in the primitive vertical estimate, one cutoff works for every later source cell; the finite conductor mass, prime reciprocal mass, and the entire log^220 scalar payment are internal.