Chen 1973, Lemma 6, equation (20): unconditional analytic final

This leaf removes the former continuity, growth, scalar-payment, and contour premises. Its two coefficients are explicit fixed-power expressions. The alpha coefficient is obtained from the corrected-kernel 21/10 envelope; the beta coefficient keeps a multiplicative 2,4,4 Hölder estimate and the fourth-power corrected-kernel envelope.

structure AnalyticNumberTheory.LargeSieve.Chen1973Lemma6Eq20ComplementarySourceParameters (x L B lastD level k : ℕ) : Prop

Literal source data for a positive-level complementary equation-(20) cell.

• hx : 3 ≤ x
• horder_four : 4 ≤ chen1973PerronOrder ↑x + 1
• hL : 0 < L
• hB : 0 < B
• hlevel : 1 ≤ level
• hlog_one : 1 ≤ Real.log ↑x
• hL_lower : ↑L ≤ Real.log ↑x ^ 100
• hL_upper : Real.log ↑x ^ 100 < ↑L + 1
• hB_lower : ↑B ≤ ↑x ^ (13 / 30)
• hB_upper : ↑x ^ (13 / 30) < ↑B + 1
• hcell : chen1973Lemma6Eq20Cell x L B lastD level k

def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20SourceD (L level : ℕ) : ℕ

Lower endpoint of the literal positive-level conductor cell.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20SourceD L level = L * 2 ^ (level - 1)

def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20SourceQ (L level : ℕ) : ℕ

Upper endpoint of the literal positive-level conductor cell.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20SourceQ L level = L * 2 ^ level

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20SourceD_pos {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) : 0 < chen1973Lemma6Eq20SourceD L level

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20SourceQ_ge_two {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) : 2 ≤ chen1973Lemma6Eq20SourceQ L level

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20SourceD_lt_Q {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) : chen1973Lemma6Eq20SourceD L level < chen1973Lemma6Eq20SourceQ L level

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_conductorBlock_subset_source_Ioc {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc (chen1973Lemma6Eq20SourceD L level) (chen1973Lemma6Eq20SourceQ L level)

The actual conductor block lies in the source positive-level interval.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_conductorBlock_subset_source_Icc {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Icc 2 (chen1973Lemma6Eq20SourceQ L level)

Closed-interval form used by the fourth-moment producer.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20UnconditionalFirstBound (x L level B k m H D Q : ℕ) : ℝ

Explicit alpha half-line bound; there is no caller-supplied growth, continuity, or integral-payment premise.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20UnconditionalFirstBound x L level B k m H D Q = 2 * Real.log ↑x ^ (231 / 100) / AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19FirstFixedPower x L level B k m H D Q (AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) * ∫ (v : ℝ) in Set.Ioi 0, AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19LinearDecay v

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20UnconditionalSecondRawBound (x L level B k m H D Q : ℕ) (r : ℝ) : ℝ

The raw beta half-line coefficient supplied by fourth-power decay.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20UnconditionalSecondRawBound x L level B k m H D Q r = 2 * Real.log ↑x ^ (22 / 5) / AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SecondFixedPower x L level B k m H D Q (AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x) r * ∫ (v : ℝ) in Set.Ioi 0, AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19QuadraticDecay v

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20UnconditionalSecondBound (x L level B k m H D Q : ℕ) (r : ℝ) : ℝ

Raw beta budget divided by sqrt x. This is only a normalization; smallness of this explicit coefficient still requires a separate proof.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20UnconditionalSecondBound x L level B k m H D Q r = AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20UnconditionalSecondRawBound x L level B k m H D Q r * ↑x ^ (-1 / 2)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_first_integral_unconditional {x L level B k m H D Q : ℕ} (hx : 3 ≤ x) (hH : 0 < H) (hD : 0 < D) (hDQ : D < Q) (horder : 3 ≤ chen1973PerronOrder ↑x + 1) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : chen1973Lemma6Eq20CorrectedFirstIntegral x L level B k m H ≤ chen1973Lemma6Eq20UnconditionalFirstBound x L level B k m H D Q

The alpha integral is bounded by the derived fixed 21/10 envelope.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_second_integral_unconditional {x L level B k m H D Q : ℕ} {r : ℝ} (hx : 3 ≤ x) (hD : 0 < D) (hQ : 2 ≤ Q) (hr : 0 < r) (horder : 4 ≤ chen1973PerronOrder ↑x + 1) (hcellIoc : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) (hcellIcc : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Icc 2 Q) (hdom : ∀ (t : ℝ), Chen1973Lemma3Domain (↑(chen1973Lemma6Beta x) + ↑t * Complex.I) (chen1973Lemma6Beta x) t) (hsphere : ∀ (t : ℝ), ∀ z ∈ Metric.sphere (↑(chen1973Lemma6Beta x) + ↑t * Complex.I) r, Chen1973Lemma3Domain z z.re z.im) : chen1973Lemma6Eq20CorrectedSecondIntegral x L level B k m H ≤ chen1973Lemma6Eq20UnconditionalSecondBound x L level B k m H D Q r * ↑x ^ (1 / 2)

The beta integral is bounded by the derived multiplicative 2,4,4 fourth-power envelope and is displayed with its x¹ᐟ² normalization.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation20_unconditional_final {x L B lastD level k m : ℕ} {ε r : ℝ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) (hr : 0 < r) (hdom : ∀ (t : ℝ), Chen1973Lemma3Domain (↑(chen1973Lemma6Beta x) + ↑t * Complex.I) (chen1973Lemma6Beta x) t) (hsphere : ∀ (t : ℝ), ∀ z ∈ Metric.sphere (↑(chen1973Lemma6Beta x) + ↑t * Complex.I) r, Chen1973Lemma3Domain z z.re z.im) : have H := chen1973Lemma6Equation20H x level k ε; have D := chen1973Lemma6Eq20SourceD L level; have Q := chen1973Lemma6Eq20SourceQ L level; chen1973Lemma6NmBlockActual x L level B k m ≤ 12 * ↑x * Real.log ↑x ^ 2 * chen1973Lemma6Eq20UnconditionalFirstBound x L level B k m H D Q + 2 * ↑x ^ (1 / 2) * (chen1973Lemma6Eq20UnconditionalSecondBound x L level B k m H D Q r * ↑x ^ (1 / 2))

Final corrected equation-(20) complementary-cell estimate. All former continuity, growth, scalar-payment, and contour parameters are absent. Cutoff positivity follows from the second max-cutoff branch, and the upstream contour inequality is supplied by the unconditional corrected equation-(17) assembly. The Cauchy radius and beta-domain premises remain explicit here; they are discharged in chen1973Lemma6_equation20_corrected_actual_budget below.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation20_corrected_actual_budget {x L B lastD level k m : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) (ε : ℝ) : have H := chen1973Lemma6Equation20H x level k ε; have D := chen1973Lemma6Eq20SourceD L level; have Q := chen1973Lemma6Eq20SourceQ L level; chen1973Lemma6NmBlockActual x L level B k m ≤ 12 * ↑x * Real.log ↑x ^ 2 * chen1973Lemma6Eq20UnconditionalFirstBound x L level B k m H D Q + 2 * ↑x ^ (1 / 2) * (chen1973Lemma6Eq20UnconditionalSecondBound x L level B k m H D Q (1 / (2 * Real.log ↑x)) * ↑x ^ (1 / 2))

Corrected actual equation-(20) budget, with the Cauchy radius and both beta-domain obligations proved internally. The right-hand side is the explicit fixed-power budget, not an x / log(x)^20 estimate. Only the literal source packet and epsilon are supplied by the caller.