noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20MobiusCoefficient (s : ℂ) (n : ℤ) : ℂ

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20MobiusCoefficient s n = ↑(ArithmeticFunction.moebius n.toNat) / ↑n ^ s

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20MobiusSecondMoment (x L level H : ℕ) (s : ℂ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20MobiusSecondMoment x L level H s = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L level, AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19Weight d * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, ‖AnalyticNumberTheory.LargeSieve.chen1973Lemma6NaturalMobiusPolynomial H s χ‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_mobius_eq_linear (H : ℕ) (s : ℂ) {d : ℕ} (χ : PrimitiveCharacter d) : chen1973Lemma6NaturalMobiusPolynomial H s χ = ∑ z ∈ Finset.Icc 1 ↑H, chen1973Lemma6Eq20MobiusCoefficient s z * ↑χ ↑z

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_mobius_atom_energy (s : ℂ) (hs : 1 / 2 ≤ s.re) {n : ℤ} (hn : 1 ≤ n) : ‖chen1973Lemma6Eq20MobiusCoefficient s n‖ ^ 2 ≤ (↑n)⁻¹

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_mobius_coefficient_energy (H : ℕ) (s : ℂ) (hs : 1 / 2 ≤ s.re) : ∑ z ∈ Finset.Icc 1 ↑H, ‖chen1973Lemma6Eq20MobiusCoefficient s z‖ ^ 2 ≤ 1 + Real.log ↑H

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_mobius_second_moment (x L level H D Q : ℕ) (s : ℂ) (hs : 1 / 2 ≤ s.re) (hD : 0 < D) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : chen1973Lemma6Eq20MobiusSecondMoment x L level H s ≤ chen1973Lemma6Eq19SharpConstant * chen1973Lemma6Eq19I x L level * (↑Q + ↑H / ↑D) * (1 + Real.log ↑H)

Fresh sharp LS on M=0,N=H. Valid for every imaginary height.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20PairPolynomial (x B k m : ℕ) {d : ℕ} (s : ℂ) (χ : PrimitiveCharacter d) : ℂ

The unchanged actual pair polynomial from (17).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20PairPolynomial x B k m s χ = ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell x B k m, ↑χ ↑(pp.1 * pp.2) / ((↑pp.1 * ↑pp.2) ^ s * ↑(Real.log (↑x / (↑pp.1 * ↑pp.2))))

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20PairFourthMoment (x L level B k m : ℕ) (s : ℂ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20PairFourthMoment x L level B k m s = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L level, AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19Weight d * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, ‖AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20PairPolynomial x B k m s χ‖ ^ 4

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6B_le_eq20_moment_product (x L level B k m H : ℕ) (s : ℂ) : chen1973Lemma6B x L level B k m H s ≤ √(chen1973Lemma6Eq20MobiusSecondMoment x L level H s) * √(√(chen1973Lemma6Eq19LDerivFourthMoment x L level s) * √(chen1973Lemma6Eq20PairFourthMoment x L level B k m s))

Source equation-(20) Holder allocation: S², pair⁴, derivative⁴.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_pair_square_fiber_card (x B k m n : ℕ) : {a ∈ (chen1973Lemma6PrimePairShell x B k m).product (chen1973Lemma6PrimePairShell x B k m) | AnalyticNumberTheory.LargeSieve.eq20Product✝ a = n}.card ≤ 256

A structural (deliberately generous) bound: every one of the four prime coordinates lies among the four fixed prime factors of one representative. No enumeration or numerical search is used.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20PairSquareCoefficient (x B k m : ℕ) (s : ℂ) (n : ℤ) : ℂ

The coefficient of the square of the actual shell polynomial.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20PairSquareCoefficient x B k m s n = ∑ a ∈ (AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell x B k m).product (AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell x B k m), if ↑(AnalyticNumberTheory.LargeSieve.eq20Product✝ a) = n then AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PairAtom x s a.1 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PairAtom x s a.2 else 0

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_pair_square_eq_collected (x B k m : ℕ) (s : ℂ) {d : ℕ} (χ : PrimitiveCharacter d) : chen1973Lemma6Eq20PairPolynomial x B k m s χ ^ 2 = ∑ n ∈ Finset.Icc (↑((B * 2 ^ k) ^ 2) + 1) (↑((B * 2 ^ k) ^ 2) + ↑(3 * (B * 2 ^ k) ^ 2)), chen1973Lemma6Eq20PairSquareCoefficient x B k m s n * ↑χ ↑n

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_pair_square_coefficient_energy (x B k m : ℕ) (s : ℂ) : ∑ n ∈ Finset.Icc (↑((B * 2 ^ k) ^ 2) + 1) (↑((B * 2 ^ k) ^ 2) + ↑(3 * (B * 2 ^ k) ^ 2)), ‖chen1973Lemma6Eq20PairSquareCoefficient x B k m s n‖ ^ 2 ≤ 256 * (∑ p ∈ chen1973Lemma6PrimePairShell x B k m, ‖chen1973Lemma6Eq19PairAtom x s p‖ ^ 2) ^ 2

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_pair_fourth_moment_fixed (x L level B k m D Q : ℕ) (s : ℂ) (hD : 0 < D) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : chen1973Lemma6Eq20PairFourthMoment x L level B k m s ≤ chen1973Lemma6Eq19I x L level * (chen1973Lemma6Eq19SharpConstant * (↑Q + ↑(3 * (B * 2 ^ k) ^ 2) / ↑D) * (256 * (∑ p ∈ chen1973Lemma6PrimePairShell x B k m, ‖chen1973Lemma6Eq19PairAtom x s p‖ ^ 2) ^ 2))

Sharp LS is re-applied on M=Y²,N=3Y², the true product support.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_pair_fourth_moment_scalar (x L level B k m D Q : ℕ) (hx : 3 ≤ x) (hB : 0 < B) (σ v : ℝ) (hσ : 1 / 2 ≤ σ) (hD : 0 < D) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : chen1973Lemma6Eq20PairFourthMoment x L level B k m (↑σ + ↑v * Complex.I) ≤ 62208 * chen1973Lemma6Eq19SharpConstant * chen1973Lemma6Eq19I x L level / Real.log ↑x ^ 4 * (↑Q + ↑(B * 2 ^ k) ^ 2 / ↑D) * ↑(B * 2 ^ k) ^ (2 - 4 * σ)

Absolute-constant Eq20 pair fourth moment with the genuine Y² scale.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6B_le_eq20_three_roots (x L level B k m H : ℕ) (s : ℂ) : chen1973Lemma6B x L level B k m H s ≤ √(chen1973Lemma6Eq20MobiusSecondMoment x L level H s) * √√(chen1973Lemma6Eq20PairFourthMoment x L level B k m s) * √√(chen1973Lemma6Eq19LDerivFourthMoment x L level s)

Explicit separated fourth roots, with the source-correct allocation.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6B_eq20_beta_paid (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 : ℝ) : have β := chen1973Lemma6Beta x; have r := 1 / (2 * Real.log ↑x); chen1973Lemma6B x L level B k m H (↑β + ↑v * Complex.I) ≤ √(chen1973Lemma6Eq19SharpConstant * chen1973Lemma6Eq19I x L level * (↑Q + ↑H / ↑D) * (1 + Real.log ↑H)) * √√(62208 * chen1973Lemma6Eq19SharpConstant * chen1973Lemma6Eq19I x L level / Real.log ↑x ^ 4 * (↑Q + ↑(B * 2 ^ k) ^ 2 / ↑D) * ↑(B * 2 ^ k) ^ (2 - 4 * β)) * √√(chen1973Lemma6Eq19I x L level * (21000000 * ↑Q ^ 2 * (|β| + |v| + r) ^ 2 * (1 + Real.log (↑Q * (1 + (|β| + |v| + r)))) ^ 4 / ↑D / r ^ 4))

All three budgets are actual producers, applied on Chen's beta line. The same finite cell weight W=Eq19I and conductor-height logarithm are retained.