theorem AnalyticNumberTheory.LargeSieve.eq20small_root_product_fourth (A B C : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hC : 0 ≤ C) : (√A * √√B * √√C) ^ 4 = A ^ 2 * B * C

theorem AnalyticNumberTheory.LargeSieve.eq20small_scalar_root_bound (A B C c W Q Z t u l : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hC : 0 ≤ C) (hc : 0 ≤ c) (hW : 0 ≤ W) (hQ : 0 < Q) (hZ : 0 ≤ Z) (ht : 0 ≤ t) (hu : 0 ≤ u) (hl : 0 < l) (hAb : A ≤ 2 * c * W / Q * Z * t) (hBb : B ≤ 186624 * c * W * Q / l ^ 4) (hCb : C ≤ 60480000000000 * W * Q * l ^ 4 * u ^ 4) : √A * √√B * √√C ≤ 1000000 * (1 + c) * W * √Z * √t * u

A scalar algebra lemma, preserving conductor and height scales.

theorem AnalyticNumberTheory.LargeSieve.eq20small_log_nat_nonneg (H : ℕ) : 0 ≤ Real.log ↑H

theorem AnalyticNumberTheory.LargeSieve.eq20small_actual_coefficient_bound (x L level B k H D Q : ℕ) (hl : 1 ≤ Real.log ↑x) (hB : 0 < B) (hQ : 2 ≤ Q) (hDQ : ↑Q = 2 * ↑D) (hYQ : B * 2 ^ k ≤ Q) : chen1973Lemma6Eq20BetaLinearCoefficient x L level B k H D Q ≤ 1000000 * (1 + chen1973Lemma6Eq19SharpConstant) * chen1973Lemma6Eq19I x L level * √(↑Q ^ 2 + ↑H) * √(1 + Real.log ↑H) * (1 + Real.log ↑Q)

The three actual moment factors retain sqrt(Q²+H), not a polynomial replacement of log Q. The inverse radius cancels the pair logarithm.

theorem AnalyticNumberTheory.LargeSieve.eq20small_source_Q_eq_twice_D {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) : ↑(chen1973Lemma6Eq20SourceQ L level) = 2 * ↑(chen1973Lemma6Eq20SourceD L level)

theorem AnalyticNumberTheory.LargeSieve.eq20small_source_coefficient_bound {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) (H : ℕ) : chen1973Lemma6Eq20BetaLinearCoefficient x L level B k H (chen1973Lemma6Eq20SourceD L level) (chen1973Lemma6Eq20SourceQ L level) ≤ 1000000 * (1 + chen1973Lemma6Eq19SharpConstant) * chen1973Lemma6Eq19I x L level * √(↑(chen1973Lemma6Eq20SourceQ L level) ^ 2 + ↑H) * √(1 + Real.log ↑H) * (1 + Real.log ↑(chen1973Lemma6Eq20SourceQ L level))

Source-cell version: no moment, integral, or scalar budget assumption.

theorem AnalyticNumberTheory.LargeSieve.eq20small_source_integral_bound {x L B lastD level k m : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) (ε : ℝ) : have H := chen1973Lemma6Equation20H x level k ε; have Q := chen1973Lemma6Eq20SourceQ L level; 2 * ↑x ^ (1 / 2) * chen1973Lemma6Eq20CorrectedSecondIntegral x L level B k m H ≤ 6000000 * Real.pi * (1 + chen1973Lemma6Eq19SharpConstant) * ↑x ^ (1 / 2) * Real.log ↑x ^ (11 / 10) * chen1973Lemma6Eq19I x L level * √(↑Q ^ 2 + ↑H) * √(1 + Real.log ↑H) * (1 + Real.log ↑Q)

The actual corrected beta integral with the exact source ceiling and conductor scales. The caller supplies only the literal complementary cell.

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

Literal exponential-source conductor scale.

Equations

• AnalyticNumberTheory.LargeSieve.eq20small_Q0 x level = 2 ^ level * Real.log ↑x ^ 100

theorem AnalyticNumberTheory.LargeSieve.eq20small_source_Q0_bounds {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) : Real.log ↑x ≤ eq20small_Q0 x level ∧ eq20small_Q0 x level ≤ 2 * ↑(chen1973Lemma6Eq20SourceQ L level)

theorem AnalyticNumberTheory.LargeSieve.eq20small_source_Q_cut {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) (ε : ℝ) (hcut : ↑lastD ≤ ↑x ^ (1 / 2 - ε)) : ↑(chen1973Lemma6Eq20SourceQ L level) ≤ 2 * ↑x ^ (1 / 2 - ε)

theorem AnalyticNumberTheory.LargeSieve.eq20small_source_Q0_le_x {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) (ε : ℝ) (hε : 0 ≤ ε) (hx : 16 ≤ ↑x) (hcut : ↑lastD ≤ ↑x ^ (1 / 2 - ε)) : eq20small_Q0 x level ≤ ↑x

theorem AnalyticNumberTheory.LargeSieve.eq20small_Ilx_subpower (η : ℝ) (hη : 0 < η) : ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (level : ℕ), 1 ≤ Real.log ↑x → Real.log ↑x ≤ eq20small_Q0 x level → eq20small_Q0 x level ≤ ↑x → chen1973Lemma6Equation20Ilx x level ≤ ↑x ^ η

Uniform subpower control of the literal exponential weight. Its cutoff is chosen before level and every source-cell parameter.

theorem AnalyticNumberTheory.LargeSieve.eq20small_log_power_absorb (a C : ℝ) (n : ℕ) (ha : 0 < a) (hC : 0 < C) : ∀ᶠ (x : ℝ) in Filter.atTop, C * Real.log x ^ n ≤ x ^ a

theorem AnalyticNumberTheory.LargeSieve.eq20small_H_first_bound {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k) (ε : ℝ) (hε : 0 ≤ ε) (hcut : ↑lastD ≤ ↑x ^ (1 / 2 - ε)) : 2 ^ (2 * ↑level - ↑k) * ↑x ^ (-13 / 30) * Real.log ↑x ^ 400 * chen1973Lemma6Equation20Ilx x level ≤ 16 * ↑x ^ (17 / 30) * Real.log ↑x ^ 200 * chen1973Lemma6Equation20Ilx x level

theorem AnalyticNumberTheory.LargeSieve.eq20small_actual_H_subpower : ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k : ℕ), Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k → ∀ (ε : ℝ), 0 ≤ ε → ↑lastD ≤ ↑x ^ (1 / 2 - ε) → ↑(chen1973Lemma6Equation20H x level k ε) ≤ ↑x ^ (2 / 3)

Uniform control of the actual rounded source height. In particular, level is not held fixed when selecting the threshold.

theorem AnalyticNumberTheory.LargeSieve.eq20small_actual_W_subpower (η : ℝ) (hη : 0 < η) : ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k : ℕ), Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k → ∀ (ε : ℝ), 0 ≤ ε → ↑lastD ≤ ↑x ^ (1 / 2 - ε) → chen1973Lemma6Eq19I x L level ≤ ↑x ^ η

Actual finite maximum W, uniformly bounded using the proved W²≤Ilx bridge.

theorem AnalyticNumberTheory.LargeSieve.eq20small_scalar_power_envelope (x W C ε : ℝ) (H Q : ℕ) (hx : 16 ≤ x) (hl : 1 ≤ Real.log x) (hC : 0 ≤ C) (hε0 : 0 ≤ ε) (hε1 : ε < 1 / 10) (hW0 : 0 ≤ W) (hW : W ≤ x ^ (ε / 8)) (hH : ↑H ≤ x ^ (2 / 3)) (hQ1 : 1 ≤ Q) (hQ : ↑Q ≤ 2 * x ^ (1 / 2 - ε)) : C * x ^ (1 / 2) * Real.log x ^ (11 / 10) * W * √(↑Q ^ 2 + ↑H) * √(1 + Real.log ↑H) * (1 + Real.log ↑Q) ≤ 12 * C * x ^ (1 - 7 * ε / 8) * Real.log x ^ 4

Pointwise scalar payment envelope. The input bounds here are elementary real inequalities; the source theorem below derives all of them internally.

theorem AnalyticNumberTheory.LargeSieve.eq20small_scalar_budget_paid (ε C : ℝ) (hε : 0 < ε) (hε1 : ε < 1 / 10) (hC : 0 < C) : ∃ (X₀ : ℝ), ∀ (x : ℝ), X₀ ≤ x → 1 ≤ Real.log x → ∀ (W : ℝ) (H Q : ℕ), 0 ≤ W → W ≤ x ^ (ε / 8) → ↑H ≤ x ^ (2 / 3) → 1 ≤ Q → ↑Q ≤ 2 * x ^ (1 / 2 - ε) → C * x ^ (1 / 2) * Real.log x ^ (11 / 10) * W * √(↑Q ^ 2 + ↑H) * √(1 + Real.log ↑H) * (1 + Real.log ↑Q) ≤ x / Real.log x ^ 20

Complete scalar payment, with its threshold before every moving parameter.

theorem AnalyticNumberTheory.LargeSieve.eq20small_actual_beta_budget_paid (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1 / 10) : ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k : ℕ), Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k → ↑lastD ≤ ↑x ^ (1 / 2 - ε) → 6 * Real.pi * ↑x ^ (1 / 2) * Real.log ↑x ^ (11 / 10) * chen1973Lemma6Eq20BetaLinearCoefficient x L level B k (chen1973Lemma6Equation20H x level k ε) (chen1973Lemma6Eq20SourceD L level) (chen1973Lemma6Eq20SourceQ L level) ≤ ↑x / Real.log ↑x ^ 20

Full scalar payment of the actual three-moment beta budget, before the integral theorem is called. All source sizes remain uniformly quantified.

theorem AnalyticNumberTheory.LargeSieve.eq20small_actual_beta_paid (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1 / 10) : ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k m : ℕ), Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k → ↑lastD ≤ ↑x ^ (1 / 2 - ε) → 2 * ↑x ^ (1 / 2) * chen1973Lemma6Eq20CorrectedSecondIntegral x L level B k m (chen1973Lemma6Equation20H x level k ε) ≤ ↑x / Real.log ↑x ^ 20

The actual corrected beta contribution is paid by x/log^20 x. Only the literal source cell and its ordinary geometric cutoff are assumed. No budget, moment, integrability, growth, or conclusion-shaped predicate is a premise. The threshold is before all cell parameters, including level.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_beta_source_uniform_log20 (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1 / 10) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k m : ℕ), Chen1973Lemma6Eq20ComplementarySourceParameters x L B lastD level k → ↑lastD ≤ ↑x ^ (1 / 2 - ε) → chen1973Lemma6Eq20SourceQ L level ≤ 2 * lastD → 2 * ↑x ^ (1 / 2) * chen1973Lemma6Eq20CorrectedSecondIntegral x L level B k m (chen1973Lemma6Equation20H x level k ε) ≤ C * ↑x / Real.log ↑x ^ 20

Requested existential-constant formulation. The displayed hQ is merely source geometry and is already implied by P.hcell; it is not an analytic payment premise. In fact the stronger theorem above permits the choice C=1.