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

Original Eq19 allocation: pair second, natural Mobius fourth, derivative fourth.

Equations

• AnalyticNumberTheory.LargeSieve.eq19BetaLinearCoefficient x L level B k H D Q = √(9 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SharpConstant * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I x L level / Real.log ↑x ^ 2 * (↑Q + ↑(B * 2 ^ k) / ↑D) * ↑(B * 2 ^ k) ^ (1 - 2 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x)) * √√(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I x L level * (AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SharpConstant * (↑Q + ↑(H * H) / ↑D) * (1 + Real.log ↑(H * H)) ^ 4)) * √√(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20BetaDerivativeCoefficient x L level D Q)

theorem AnalyticNumberTheory.LargeSieve.eq19Beta_actual_linear (x L level B k m H D Q : ℕ) (hx : 3 ≤ x) (hB : 0 < B) (hD : 0 < D) (hQ : 2 ≤ Q) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) (v : ℝ) : chen1973Lemma6B x L level B k m H (↑(chen1973Lemma6Beta x) + ↑v * Complex.I) ≤ eq19BetaLinearCoefficient x L level B k H D Q * (1 + |v|)

theorem AnalyticNumberTheory.LargeSieve.eq19Beta_integrable_and_budget (x L level B k m H D Q : ℕ) (hx : 3 ≤ x) (hB : 0 < B) (hD : 0 < D) (hQ : 2 ≤ Q) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : MeasureTheory.IntegrableOn (fun (v : ℝ) => chen1973Lemma6B x L level B k m H (↑(chen1973Lemma6Beta x) + ↑v * Complex.I) / chen1973Lemma6Eq17CorrectedKernel x (↑(chen1973Lemma6Beta x) + ↑v * Complex.I)) (Set.Ioi 0) MeasureTheory.volume ∧ chen1973Lemma6Eq20CorrectedSecondIntegral x L level B k m H ≤ 3 * Real.pi * chen1973PerronScale ↑x * eq19BetaLinearCoefficient x L level B k H D Q

The corrected beta integral at any H; the height is not an Eq20 complement.

theorem AnalyticNumberTheory.LargeSieve.eq19Beta_nonempty_pairD_bound {x B k m : ℕ} (hx : 3 ≤ x) (hne : (chen1973Lemma6PrimePairShell x B k m).Nonempty) : ↑(B * 2 ^ k) ≤ ↑x ^ (2 / 3)

The large-Y cutoff is a consequence of the actual carrier, never an extra assumption.

theorem AnalyticNumberTheory.LargeSieve.eq19Beta_empty_integral {x L level B k m H : ℕ} (he : chen1973Lemma6PrimePairShell x B k m = ∅) : chen1973Lemma6Eq20CorrectedSecondIntegral x L level B k m H = 0

Empty shells give the literal zero numerator and corrected integral.

theorem AnalyticNumberTheory.LargeSieve.eq19Beta_source_cap {x L B lastD level k : ℕ} {ε : ℝ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) (hε : 0 ≤ ε) (hcut : ↑lastD ≤ ↑x ^ (1 / 2 - ε)) (hQ : chen1973Lemma6Eq19SourceQ L level ≤ 2 * lastD) : ↑(chen1973Lemma6Eq19SourceQ L level) ≤ 2 * ↑x ^ (1 / 2)

The source cut gives the cap required by the already verified alpha endpoint.

theorem AnalyticNumberTheory.LargeSieve.eq19Beta_Ilx_subpower (η : ℝ) (hη : 0 < η) : ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k : ℕ), Chen1973Lemma6Eq19SourceParameters x L B lastD level k → chen1973Lemma6Eq19SourceQ L level ≤ 2 * lastD → ↑(chen1973Lemma6Eq19SourceQ L level) ≤ 2 * ↑x ^ (1 / 2) → chen1973Lemma6Equation20Ilx x level ≤ ↑x ^ η

Uniform subpower control of the printed exponential, with threshold before level.

theorem AnalyticNumberTheory.LargeSieve.eq19Beta_printedHeight_upper {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) (hQ : chen1973Lemma6Eq19SourceQ L level ≤ 2 * lastD) (htt : 60 ≤ Real.log (Real.log (eq19AlphaQ0 x level))) : ↑(chen1973Lemma6Eq19PrintedHeight x level) ≤ 4 * ↑(chen1973Lemma6Eq19SourceQ L level) * Real.log ↑x ^ 100 * chen1973Lemma6Equation20Ilx x level

Upper height budget at the actual ceil, not the obsolete W-height.

def AnalyticNumberTheory.LargeSieve.eq19BetaDerivativeConstant : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.eq19BetaDerivativeConstant = 32 * 21000000 * 9 * 8 ^ 4 * 16

noncomputable def AnalyticNumberTheory.LargeSieve.eq19BetaMobiusConstant : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.eq19BetaMobiusConstant = 33 * 241 ^ 4 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SharpConstant

noncomputable def AnalyticNumberTheory.LargeSieve.eq19BetaNumeratorConstant : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.eq19BetaNumeratorConstant = √(18 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SharpConstant * √(AnalyticNumberTheory.LargeSieve.eq19BetaMobiusConstant * AnalyticNumberTheory.LargeSieve.eq19BetaDerivativeConstant))

theorem AnalyticNumberTheory.LargeSieve.eq19Beta_derivative_coefficient {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) (hQ : chen1973Lemma6Eq19SourceQ L level ≤ 2 * lastD) (hlogQ : Real.log ↑(chen1973Lemma6Eq19SourceQ L level) ≤ 4 * Real.log ↑x) : chen1973Lemma6Eq20BetaDerivativeCoefficient x L level (chen1973Lemma6Eq19SourceD L level) (chen1973Lemma6Eq19SourceQ L level) ≤ eq19BetaDerivativeConstant * chen1973Lemma6Eq19I x L level * ↑(chen1973Lemma6Eq19SourceQ L level) * Real.log ↑x ^ 8

theorem AnalyticNumberTheory.LargeSieve.eq19Beta_mobius_coefficient {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) (hQ : chen1973Lemma6Eq19SourceQ L level ≤ 2 * lastD) (hcap : ↑(chen1973Lemma6Eq19SourceQ L level) ≤ 2 * ↑x ^ (1 / 2)) (htt : 60 ≤ Real.log (Real.log (eq19AlphaQ0 x level))) : have H := chen1973Lemma6Eq19PrintedHeight x level; chen1973Lemma6Eq19I x L level * (chen1973Lemma6Eq19SharpConstant * (↑(chen1973Lemma6Eq19SourceQ L level) + ↑(H * H) / ↑(chen1973Lemma6Eq19SourceD L level)) * (1 + Real.log ↑(H * H)) ^ 4) ≤ eq19BetaMobiusConstant * chen1973Lemma6Eq19I x L level * ↑(chen1973Lemma6Eq19SourceQ L level) * Real.log ↑x ^ 204 * chen1973Lemma6Equation20Ilx x level ^ 2

theorem AnalyticNumberTheory.LargeSieve.eq19Beta_three_roots {A C₁ C₂ W Q D Y u J : ℝ} (hA : 0 ≤ A) (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) (hW : 0 ≤ W) (hQ : 0 ≤ Q) (hD : 0 < D) (hY : 0 ≤ Y) (hu : 0 ≤ u) (hJ : 0 ≤ J) (hQD : Q = 2 * D) : √(A * W * (Q + Y / D)) * √√(C₁ * W * Q * u ^ 204 * J ^ 2) * √√(C₂ * W * Q * u ^ 8) ≤ √(2 * A * √(C₁ * C₂)) * W * √J * (Q + √Y) * u ^ 53

Algebraic joining of pair², S⁴ and L'⁴ preserves the square-root conductor scale.

theorem AnalyticNumberTheory.LargeSieve.eq19Beta_printed_coefficient {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) (hQ : chen1973Lemma6Eq19SourceQ L level ≤ 2 * lastD) (hcap : ↑(chen1973Lemma6Eq19SourceQ L level) ≤ 2 * ↑x ^ (1 / 2)) (htt : 60 ≤ Real.log (Real.log (eq19AlphaQ0 x level))) : eq19BetaLinearCoefficient x L level B k (chen1973Lemma6Eq19PrintedHeight x level) (chen1973Lemma6Eq19SourceD L level) (chen1973Lemma6Eq19SourceQ L level) ≤ eq19BetaNumeratorConstant * chen1973Lemma6Eq19I x L level * √(chen1973Lemma6Equation20Ilx x level) * (↑(chen1973Lemma6Eq19SourceQ L level) + √↑(B * 2 ^ k)) * Real.log ↑x ^ 53

Source-faithful scalar numerator coefficient at the printed height.

theorem AnalyticNumberTheory.LargeSieve.eq19Beta_log75_eventually (η : ℝ) (hη : 0 < η) : ∃ (X₀ : ℝ), ∀ (x : ℝ), X₀ ≤ x → Real.log x ^ 75 ≤ x ^ η

Fixed log-power absorption, quantified before every cell parameter.

theorem AnalyticNumberTheory.LargeSieve.eq19Beta_gap_scalar {x Q Y J u ε : ℝ} (hx : 1 ≤ x) (hu : 1 ≤ u) (hε : 0 < ε) (hεu : ε < 1 / 10) (_hJ : 0 ≤ J) (hQ : 0 ≤ Q) (_hY : 0 ≤ Y) (hJup : J ≤ x ^ (ε / 4)) (hQup : Q ≤ 2 * x ^ (1 / 2 - ε)) (hYup : Y ≤ x ^ (2 / 3)) (hlog : u ^ 75 ≤ x ^ (ε / 4)) : x ^ (1 / 2) * J * (Q + √Y) * u ^ 55 ≤ 3 * x / u ^ 20

Both conductor and nonempty-pair scales retain a strict power margin.

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

Printed-height beta smallness for every source cell; no hypothesis bounds Y.

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

The positive Eq19 cell, now with both actual corrected integrals paid.