theorem AnalyticNumberTheory.LargeSieve.eq20_log_height {T : ℝ} (hT : 1 ≤ T) : 1 + Real.log T ≤ 2 * √T

Height extraction preserves the conductor logarithm.

theorem AnalyticNumberTheory.LargeSieve.eq20_derivative_height_algebra (Q a r W D v : ℝ) (hQ : 1 ≤ Q) (ha : 0 ≤ a) (hr : 0 ≤ r) (hW : 0 ≤ W) (hD : 0 ≤ D) : W * (21000000 * Q ^ 2 * (a + |v| + r) ^ 2 * (1 + Real.log (Q * (1 + (a + |v| + r)))) ^ 4 / D / r ^ 4) ≤ 16 * 21000000 * W * Q ^ 2 * (1 + a + r) ^ 2 * (1 + Real.log (Q * (1 + (1 + a + r)))) ^ 4 / (D * r ^ 4) * (1 + |v|) ^ 4

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20BetaDerivativeCoefficient (x L level D Q : ℕ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20BetaDerivativeCoefficient x L level D Q = 16 * 21000000 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I x L level * ↑Q ^ 2 * (1 + |AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x| + 1 / (2 * Real.log ↑x)) ^ 2 * (1 + Real.log (↑Q * (1 + (1 + |AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x| + 1 / (2 * Real.log ↑x))))) ^ 4 / (↑D * (1 / (2 * Real.log ↑x)) ^ 4)

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

Equations

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

theorem AnalyticNumberTheory.LargeSieve.eq20_fourth_root_height {G T : ℝ} (hG : 0 ≤ G) (hT : 0 ≤ T) : √√(G * T ^ 4) = √√G * T

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6B_eq20_beta_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) ≤ chen1973Lemma6Eq20BetaLinearCoefficient x L level B k H D Q * (1 + |v|)

Actual beta numerator, uniformly linear in height, with the S²/pair⁴/L'⁴ allocation.

theorem AnalyticNumberTheory.LargeSieve.eq20_radial_factor_quadratic {u z : ℝ} {N : ℕ} (hz : 0 ≤ z) (hzu : z ≤ u) (hN : 2 ≤ N) : (1 + u ^ N)⁻¹ ≤ 2 / (1 + z ^ 2)

A scale-preserving quadratic comparison: no log(x)^(231/100) payment.

theorem AnalyticNumberTheory.LargeSieve.eq20_linear_over_corrected_kernel {x : ℕ} (hx : 3 ≤ x) {σ v : ℝ} (hσ : 1 / 2 ≤ σ) (hv : 0 ≤ v) : (1 + v) / chen1973Lemma6Eq17CorrectedKernel x (↑σ + ↑v * Complex.I) ≤ 6 * (1 + (v / chen1973PerronScale ↑x) ^ 2)⁻¹

The literal radial |s| pays the linear height before scaling the integral.

theorem AnalyticNumberTheory.LargeSieve.eq20_scaled_cauchy_integrable {A : ℝ} (hA : 0 < A) : MeasureTheory.IntegrableOn (fun (v : ℝ) => (1 + (v / A) ^ 2)⁻¹) (Set.Ioi 0) MeasureTheory.volume

theorem AnalyticNumberTheory.LargeSieve.eq20_scaled_cauchy_integral {A : ℝ} (hA : 0 < A) : ∫ (v : ℝ) in Set.Ioi 0, (1 + (v / A) ^ 2)⁻¹ = A * (Real.pi / 2)

theorem AnalyticNumberTheory.LargeSieve.eq20_corrected_linear_integrable_and_bound {x : ℕ} (hx : 3 ≤ x) {σ K : ℝ} (hσ : 1 / 2 ≤ σ) (hK : 0 ≤ K) (F : ℝ → ℝ) (hcont : Continuous F) (hF0 : ∀ v ∈ Set.Ioi 0, 0 ≤ F v) (hFK : ∀ v ∈ Set.Ioi 0, F v ≤ K * (1 + v)) : MeasureTheory.IntegrableOn (fun (v : ℝ) => F v / chen1973Lemma6Eq17CorrectedKernel x (↑σ + ↑v * Complex.I)) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (v : ℝ) in Set.Ioi 0, F v / chen1973Lemma6Eq17CorrectedKernel x (↑σ + ↑v * Complex.I) ≤ 3 * Real.pi * chen1973PerronScale ↑x * K

A genuine integral theorem for the unchanged corrected kernel, preserving A=(log x)^(11/10). This generic analytic helper is consumed below by the actual three-moment producer and an internally proved continuity theorem.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6B_eq20_beta_continuous {x L level B k m H D Q : ℕ} (hD : 0 < D) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : Continuous fun (v : ℝ) => chen1973Lemma6B x L level B k m H (↑(chen1973Lemma6Beta x) + ↑v * Complex.I)

Continuity of the actual beta numerator; primitive conductors exceed one.

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

Explicit beta half-line budget with only one Perron scale, not a spurious x normalization or a conductor-polynomial replacement of the logarithm.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20BetaIntegralBudget x L level B k H D Q = 3 * Real.pi * Real.log ↑x ^ (11 / 10) * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20BetaLinearCoefficient x L level B k H D Q

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_beta_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 ≤ chen1973Lemma6Eq20BetaIntegralBudget x L level B k H D Q

The new three moments are wired to the literal corrected beta integral. No integrability, continuity, growth, scalar payment, or order hypothesis is supplied by the caller. H is arbitrary, including zero.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_beta_contribution_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) : 2 * ↑x ^ (1 / 2) * chen1973Lemma6Eq20CorrectedSecondIntegral x L level B k m H ≤ 6 * Real.pi * ↑x ^ (1 / 2) * Real.log ↑x ^ (11 / 10) * chen1973Lemma6Eq20BetaLinearCoefficient x L level B k H D Q

The exact beta contribution in corrected (17)/(20), including its outer 2 sqrt x; no extra factor sqrt x is introduced.