Chen 1973, Lemma 6, equation (19): uniform moment constants

This leaf freezes the sharp Lemma-2 constant before every coefficient, spectral height, and cell parameter. It also records injectivity of the actual ordered prime-pair shell, the structural input needed to pay its collected coefficient energy without a collision multiplicity. No final-cell estimate is assumed.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SharpConstant : ℝ

One fixed global constant for all complex-coefficient uses of sharp Lemma 2.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SharpConstant = 2 * Classical.choose AnalyticNumberTheory.LargeSieve.eq19SharpRealPackage✝

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19SharpConstant_pos : 0 < chen1973Lemma6Eq19SharpConstant

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma2_equationThree_complex_fixed (c : ℤ → ℂ) (M : ℤ) (N D Q : ℕ) (hD : 0 < D) : ∑ q ∈ Finset.Ioc D Q, 1 / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), c n * ↑χ ↑n‖ ^ 2 ≤ chen1973Lemma6Eq19SharpConstant * (↑Q + ↑N / ↑D) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖c n‖ ^ 2

Complex sharp Lemma 2 with a single constant chosen before the coefficient sequence and all interval/conductor parameters.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_pair_product_injective (x B k m : ℕ) : Set.InjOn (fun (pp : ℕ × ℕ) => pp.1 * pp.2) ↑(chen1973Lemma6PrimePairShell x B k m)

Products are injective on Chen's actual ordered prime-pair shell. The small/large prime separation rules out the swapped factorization.

theorem AnalyticNumberTheory.LargeSieve.norm_collected_sq_eq_fiber_energy {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] (S : Finset ι) (g : ι → κ) (a : ι → ℂ) (hg : Set.InjOn g ↑S) (y : κ) : ‖∑ i ∈ S, if g i = y then a i else 0‖ ^ 2 = ∑ i ∈ S with g i = y, ‖a i‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PairAtom (x : ℕ) (s : ℂ) (pp : ℕ × ℕ) : ℂ

One atom in the literal ordered prime-pair coefficient energy.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PairAtom x s pp = 1 / ((↑pp.1 * ↑pp.2) ^ s * ↑(Real.log (↑x / (↑pp.1 * ↑pp.2))))

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_pairCoefficient_square_energy (x B k m : ℕ) (s : ℂ) : ∑ n ∈ Finset.Icc 1 ↑(x * x), ‖chen1973Lemma6Eq19PairCoefficient x B k m s n‖ ^ 2 = ∑ pp ∈ chen1973Lemma6PrimePairShell x B k m, ‖chen1973Lemma6Eq19PairAtom x s pp‖ ^ 2

The collected coefficient has exactly the energy of the actual ordered dyadic pair shell. In particular, no pair-collision multiplicity is lost.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation15_fixed_log_power (H D Q : ℕ) (s : ℂ) (hD : 0 < D) (hs : Chen1973Lemma3Domain s s.re s.im) : ∑ d ∈ Finset.Ioc D Q, 1 / ↑d.totient * ∑ χ : PrimitiveCharacter d, ‖chen1973Lemma6NaturalMobiusPolynomial H s χ‖ ^ 4 ≤ chen1973Lemma6Eq19SharpConstant * (↑Q + ↑(H * H) / ↑D) * (1 + Real.log ↑(H * H)) ^ 4

Equation (15) with the global sharp constant; the constant is selected before H,D,Q,s and hence before every vertical height.

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

The literal pair-polynomial second moment, with the global sharp constant and the exact ordered-pair coefficient energy. Neither the constant nor the coefficient support depends on a conductor cell.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation14_fixed_log_power (H D Q : ℕ) (s : ℂ) (hH : 0 < H) (hD : 0 < D) (hDQ : D < Q) (hs : 1 ≤ s.re) : ∑ d ∈ Finset.Ioc D Q, 1 / ↑d.totient * ∑ χ : PrimitiveCharacter d, ‖chen1973Lemma6OneSubLS H s χ‖ ^ 2 ≤ 2 * chen1973Lemma6Eq19SharpConstant * (↑Q + ↑(H * H) / ↑D) * (1 + Real.log ↑(H * H)) ^ 4 + 2 * ↑Q * (40 * ‖s‖ * √↑Q * Real.log ↑Q * ↑(H + 1) ^ (-s.re) * (1 + Real.log ↑H)) ^ 2

Equation (14), with the same global sharp constant as equations (15) and Lemma 2. The constant is fixed before s and hence before a vertical height.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_oneSub_second_moment_fixed (x L level H D Q : ℕ) (s : ℂ) (hH : 0 < H) (hD : 0 < D) (hDQ : D < Q) (hs : 1 ≤ s.re) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : chen1973Lemma6Eq19OneSubSecondMoment x L level H s ≤ chen1973Lemma6Eq19I x L level * (2 * chen1973Lemma6Eq19SharpConstant * (↑Q + ↑(H * H) / ↑D) * (1 + Real.log ↑(H * H)) ^ 4 + 2 * ↑Q * (40 * ‖s‖ * √↑Q * Real.log ↑Q * ↑(H + 1) ^ (-s.re) * (1 + Real.log ↑H)) ^ 2)

Equation (14) transported to an equation-(19) cell, with its constant fixed globally before the spectral parameter.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_mobius_fourth_moment_uniform (x L level H D Q : ℕ) (σ T : ℝ) (hD : 0 < D) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) (hdom : ∀ v ∈ Set.Icc (-T) T, Chen1973Lemma3Domain (↑σ + ↑v * Complex.I) σ v) (v : ℝ) : v ∈ Set.Icc (-T) T → chen1973Lemma6Eq19MobiusFourthMoment x L level H (↑σ + ↑v * Complex.I) ≤ chen1973Lemma6Eq19I x L level * (chen1973Lemma6Eq19SharpConstant * (↑Q + ↑(H * H) / ↑D) * (1 + Real.log ↑(H * H)) ^ 4)

v-uniform equation-(15) moment on an explicit closed height interval.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19OneSubUniformEnvelope (H Q : ℕ) (σ T : ℝ) : ℝ

A scalar equation-(14) envelope independent of the vertical parameter.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19OneSubUniformEnvelope H Q σ T = (40 * (|σ| + T) * √↑Q * Real.log ↑Q * ↑(H + 1) ^ (-σ) * (1 + Real.log ↑H)) ^ 2

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_oneSub_second_moment_uniform (x L level H D Q : ℕ) (σ T : ℝ) (hH : 0 < H) (hD : 0 < D) (hDQ : D < Q) (hσ : 1 ≤ σ) (_hT : 0 ≤ T) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) (v : ℝ) : v ∈ Set.Icc (-T) T → chen1973Lemma6Eq19OneSubSecondMoment x L level H (↑σ + ↑v * Complex.I) ≤ chen1973Lemma6Eq19I x L level * (2 * chen1973Lemma6Eq19SharpConstant * (↑Q + ↑(H * H) / ↑D) * (1 + Real.log ↑(H * H)) ^ 4 + 2 * ↑Q * chen1973Lemma6Eq19OneSubUniformEnvelope H Q σ T)

The equation-(14) moment uniformly on a closed vertical interval. The sharp large-sieve constant and the complete scalar envelope are selected before v, so this theorem can be placed under a height integral without choice.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19CircleFourthEnvelopeUniform (Q : ℕ) (σ T r : ℝ) : ℝ

A Cauchy-circle fourth-moment envelope uniform in the centre height.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19CircleFourthEnvelopeUniform Q σ T r = 21000000 * ↑Q ^ 2 * (|σ| + T + r) ^ 2 * Real.log (↑Q * (1 + (|σ| + T + r))) ^ 4

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_LDeriv_fourth_moment_uniform (x L level Q : ℕ) (σ T r : ℝ) (hQ : 2 ≤ Q) (hT : 0 ≤ T) (hr : 0 < r) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Icc 2 Q) (hspheres : ∀ v ∈ Set.Icc (-T) T, ∀ z ∈ Metric.sphere (↑σ + ↑v * Complex.I) r, Chen1973Lemma3Domain z z.re z.im) (v : ℝ) : v ∈ Set.Icc (-T) T → chen1973Lemma6Eq19LDerivFourthMoment x L level (↑σ + ↑v * Complex.I) ≤ chen1973Lemma6Eq19I x L level * ↑Q * ((chen1973Lemma6Eq19CircleFourthEnvelopeUniform Q σ T r + 1) / r) ^ 4

The actual L' fourth moment uniformly on a closed vertical interval. Both the Cauchy radius and the scalar envelope are fixed outside v.