Chen 1973, Lemma 6, equation (19): source parameters

This module freezes the literal positive-level parameter domain on p. 122. The conductor cell is L*2^(level-1) < d ≤ L*2^level, the pair cell is B*2^k < p₁p₂ ≤ B*2^(k+1). The legacy height helpers in this module use the actual maximum W, not the printed exponential I. The genuine source height ⌈2^level (log x)^200 I_{level,x}⌉₊ is defined in SourceWeightHeight.

No final-payment hypothesis is stored in the source packet. The final logarithmic payments below are proved from explicit large-x inequalities. Any constant coming from a source ≪ is therefore quantified once, before all cell parameters.

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

Lower endpoint of the positive-level conductor cell.

Equations

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

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

Upper endpoint of the positive-level conductor cell.

Equations

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

def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PairD (B k : ℕ) : ℕ

Lower endpoint of the equation-(19) prime-pair shell.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PairD B k = B * 2 ^ k

def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PairQ (B k : ℕ) : ℕ

Upper endpoint of the equation-(19) prime-pair shell.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PairQ B k = B * 2 ^ (k + 1)

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

The real legacy W-based cutoff; not the printed exponential-I height.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19HeightReal x L level = 2 ^ level * Real.log ↑x ^ 200 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I x L level

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

Literal p. 122 positive-level equation-(19) domain.

lastD is Chen's final conductor cutoff occurring in the branch split. It is not confused with the lower endpoint chen1973Lemma6Eq19SourceD L level. The real-to-natural identifications L ≈ (log x)^100 and B ≈ x^(13/30) are kept as exact two-sided rounding inequalities.

• hx : 3 ≤ x
• 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
• hbranch : chen1973Lemma6Eq19Cell x L B lastD level k

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SourceParameters.log_pos {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) : 0 < Real.log ↑x

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SourceParameters.log_one_le {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) : 1 ≤ Real.log ↑x

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SourceParameters.branch {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) : lastD < chen1973Lemma6Eq19PairD B k ∨ chen1973Lemma6Eq19PairD B k ≤ lastD ∧ chen1973Lemma6Eq19SourceQ L level < chen1973Lemma6Eq19PairD B k

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SourceD_pos {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) : 0 < chen1973Lemma6Eq19SourceD L level

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SourceQ_pos {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) : 0 < chen1973Lemma6Eq19SourceQ L level

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SourceQ_ge_two {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) : 2 ≤ chen1973Lemma6Eq19SourceQ L level

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SourceD_lt_Q {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) : chen1973Lemma6Eq19SourceD L level < chen1973Lemma6Eq19SourceQ L level

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_conductorBlock_subset_source_Ioc {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) ⦃d : ℕ⦄ : d ∈ chen1973Lemma6ConductorBlock x L level → d ∈ Finset.Ioc (chen1973Lemma6Eq19SourceD L level) (chen1973Lemma6Eq19SourceQ L level)

The actual conductor carrier lies in the literal positive-level interval.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_conductorBlock_subset_source_Icc {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) ⦃d : ℕ⦄ : d ∈ chen1973Lemma6ConductorBlock x L level → d ∈ Finset.Icc 2 (chen1973Lemma6Eq19SourceQ L level)

Closed-interval form required by the fourth-moment input.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_primePairShell_product_mem_source_Ioc {x L B lastD level k m : ℕ} (_P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) {pp : ℕ × ℕ} (hpp : pp ∈ chen1973Lemma6PrimePairShell x B k m) : pp.1 * pp.2 ∈ Finset.Ioc (chen1973Lemma6Eq19PairD B k) (chen1973Lemma6Eq19PairQ B k)

Every pair in the actual filtered shell has the printed dyadic product bounds.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19Height_eq_ceil (x L level : ℕ) : chen1973Lemma6Eq19Height x L level = ⌈chen1973Lemma6Eq19HeightReal x L level⌉₊

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19HeightReal_pos {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) : 0 < chen1973Lemma6Eq19HeightReal x L level

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19Height_pos {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) : 0 < chen1973Lemma6Eq19Height x L level

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19HeightReal_le_height (x L level : ℕ) : chen1973Lemma6Eq19HeightReal x L level ≤ ↑(chen1973Lemma6Eq19Height x L level)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19Height_lt_real_add_one {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) : ↑(chen1973Lemma6Eq19Height x L level) < chen1973Lemma6Eq19HeightReal x L level + 1

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_first_log_payment {x C : ℝ} (_hx : 0 < x) (hlog : 0 < Real.log x) : x * Real.log x ^ 2 * (C / Real.log x ^ 22) = C * x / Real.log x ^ 20

Exact payment of the first log² contour prefactor.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_second_power_payment {x C : ℝ} (hx : 0 < x) (_hlog : 0 < Real.log x) : x ^ (1 / 2) * (C * x ^ (1 / 2) / Real.log x ^ 20) = C * x / Real.log x ^ 20

Exact payment of the printed square-root contour prefactor against a square-root-sized second-integral bound.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_absorb_global_constant (Cabs : ℝ) {x : ℝ} (_hC : 0 ≤ Cabs) (hlog : 1 ≤ Real.log x) {a b : ℕ} (hab : a ≤ b) (hlarge : Cabs ≤ Real.log x ^ (b - a)) : Cabs * Real.log x ^ a ≤ Real.log x ^ b

Uniform polylogarithmic absorption. The absolute constant is selected before x and before every cell parameter; hlarge is the explicit large-x threshold.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_absorb_global_constant_div (Cabs : ℝ) {x : ℝ} (hC : 0 ≤ Cabs) (hlog : 1 ≤ Real.log x) {a b target : ℕ} (hba : a + target ≤ b) (hlarge : Cabs ≤ Real.log x ^ (b - (a + target))) : Cabs * Real.log x ^ a / Real.log x ^ b ≤ 1 / Real.log x ^ target

Division form used when a source ≪ contributes one global absolute constant. There is no cell-wise or height-wise existential constant.