Chen 1973, Lemma 6, equation (19): fixed-power infinite-height envelopes

The alpha lane uses the 21/10 corrected-kernel weakening after the square root of equation (14), hence only linear height growth. The beta lane keeps the literal multiplicative 2,4,4 Hölder estimate and takes the genuine fourth root of the Lemma-3 fourth moment before using the fourth-power kernel weakening. No final H/logarithm absorption is performed here.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19FixedPairBound (x L level B k m D Q : ℕ) (σ : ℝ) : ℝ

The fixed (height-independent) pair-energy bound.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19FixedPairBound x L level B k m D Q σ = AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I x L level * (AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SharpConstant * (↑Q + ↑(x * x) / ↑D) * ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell x B k m, ‖AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PairAtom x (↑σ) pp‖ ^ 2)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_pair_second_moment_fixed_height (x L level B k m D Q : ℕ) (σ v : ℝ) (hD : 0 < D) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : chen1973Lemma6Eq19PairSecondMoment x L level B k m (↑σ + ↑v * Complex.I) ≤ chen1973Lemma6Eq19FixedPairBound x L level B k m D Q σ

The pair second moment is uniformly bounded on the whole vertical line.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_LDeriv_fourth_moment_sharp_cauchy (x L level Q : ℕ) (s : ℂ) (r : ℝ) (hQ : 2 ≤ Q) (hr : 0 < r) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Icc 2 Q) (hsphere : ∀ z ∈ Metric.sphere s r, Chen1973Lemma3Domain z z.re z.im) : chen1973Lemma6Eq19LDerivFourthMoment x L level s ≤ chen1973Lemma6Eq19I x L level * ↑Q * (√√(chen1973Lemma6Eq19CircleFourthEnvelope Q s r + 1) / r) ^ 4

Sharp fourth-root Cauchy envelope for the L' fourth moment. Unlike the older compatibility bound, the fourth moment from Lemma 3 is not first weakened to a first-power pointwise bound.

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

Fixed coefficient left after extracting the alpha lane's single power of 1+v from the square root of equation (14).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19FirstFixedPower x L level B k m H D Q σ = √(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19FixedPairBound x L level B k m D Q σ) * √(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I x L level * (2 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SharpConstant * (↑Q + ↑(H * H) / ↑D) * (1 + Real.log ↑(H * H)) ^ 4 + 2 * ↑Q * (40 * (|σ| + 1) * √↑Q * Real.log ↑Q * ↑(H + 1) ^ (-σ) * (1 + Real.log ↑H)) ^ 2))

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_first_le_fixedPower (x L level B k m H D Q : ℕ) (σ v : ℝ) (hH : 0 < H) (hD : 0 < D) (hDQ : D < Q) (hσ : 1 ≤ σ) (hv : 0 ≤ v) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : chen1973Lemma6A x L level B k m H (↑σ + ↑v * Complex.I) ≤ chen1973Lemma6Eq19FirstFixedPower x L level B k m H D Q σ * (1 + v)

The first numerator has genuinely linear, rather than postulated, height growth.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19LinearDecay (v : ℝ) : ℝ

The two fixed decay profiles used below.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19LinearDecay v = (1 + v) / (1 + |v| ^ (21 / 10))

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19QuadraticDecay (v : ℝ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19QuadraticDecay v = (1 + v) ^ 2 / (1 + |v| ^ 4)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_linearDecay_integrable : MeasureTheory.IntegrableOn chen1973Lemma6Eq19LinearDecay (Set.Ioi 0) MeasureTheory.volume

The alpha fixed-power profile is integrable on the positive half-line.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_correctedKernel_inv_le_linearDecay {x : ℕ} (hx : 3 ≤ x) {σ v : ℝ} (hσ : 0 < σ) (horder : 3 ≤ chen1973PerronOrder ↑x + 1) : (chen1973Lemma6Eq17CorrectedKernel x (↑σ + ↑v * Complex.I))⁻¹ ≤ 2 * Real.log ↑x ^ (231 / 100) / σ / (1 + |v| ^ (21 / 10))

The corrected Perron kernel has the fixed linear-growth decay bound.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_first_fixedPower_integrable_and_bound (x L level B k m H D Q : ℕ) (σ : ℝ) (hx : 3 ≤ x) (_hH : 0 < H) (_hD : 0 < D) (_hDQ : D < Q) (hσ : 1 ≤ σ) (horder : 3 ≤ chen1973PerronOrder ↑x + 1) (_hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : have F := fun (v : ℝ) => chen1973Lemma6Eq19FirstFixedPower x L level B k m H D Q σ * (1 + v) / chen1973Lemma6Eq17CorrectedKernel x (↑σ + ↑v * Complex.I); MeasureTheory.IntegrableOn F (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (v : ℝ) in Set.Ioi 0, F v ≤ 2 * Real.log ↑x ^ (231 / 100) / σ * chen1973Lemma6Eq19FirstFixedPower x L level B k m H D Q σ * ∫ (v : ℝ) in Set.Ioi 0, chen1973Lemma6Eq19LinearDecay v

Explicit alpha-envelope integral, with no continuity or growth premise.

def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SecondCircleFixedPower (Q : ℕ) (σ r : ℝ) : ℝ

A height-independent polynomial majorant for the Lemma-3 circle envelope. The two nested square roots of this quantity are deliberately retained in the beta-lane coefficient.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SecondCircleFixedPower Q σ r = 21000000 * ↑Q ^ 6 * (1 + |σ| + r) ^ 6 + 1

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SecondFixedPower (x L level B k m H D Q : ℕ) (σ r : ℝ) : ℝ

Fixed beta-lane coefficient after genuine multiplicative 2,4,4 Hölder. The L' contribution visibly retains the nested fourth-root envelope.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SecondFixedPower x L level B k m H D Q σ r = √(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19FixedPairBound x L level B k m D Q σ) * √(√(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I x L level * ↑Q * (√√(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SecondCircleFixedPower Q σ r) / r) ^ 4) * √(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I x L level * (AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SharpConstant * (↑Q + ↑(H * H) / ↑D) * (1 + Real.log ↑(H * H)) ^ 4)))

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_second_le_fixedPower (x L level B k m H D Q : ℕ) (σ r v : ℝ) (hD : 0 < D) (hQ : 2 ≤ Q) (hr : 0 < r) (hv : 0 ≤ v) (hcellIoc : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) (hcellIcc : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Icc 2 Q) (hdom : ∀ t ∈ Set.Icc (-v) v, Chen1973Lemma3Domain (↑σ + ↑t * Complex.I) σ t) (hsphere : ∀ z ∈ Metric.sphere (↑σ + ↑v * Complex.I) r, Chen1973Lemma3Domain z z.re z.im) : chen1973Lemma6B x L level B k m H (↑σ + ↑v * Complex.I) ≤ chen1973Lemma6Eq19SecondFixedPower x L level B k m H D Q σ r * (1 + v) ^ 2

The beta numerator has a derived quadratic envelope. Its proof uses the literal multiplicative 2,4,4 Hölder theorem and the sharp fourth-root Cauchy bound, rather than a postulated growth hypothesis.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_quadraticDecay_integrable : MeasureTheory.IntegrableOn chen1973Lemma6Eq19QuadraticDecay (Set.Ioi 0) MeasureTheory.volume

The beta fixed-power profile is integrable on the positive half-line.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_second_fixedPower_integrable_and_bound (x L level B k m H D Q : ℕ) (σ r : ℝ) (hx : 3 ≤ x) (hσ : 0 < σ) (horder : 4 ≤ chen1973PerronOrder ↑x + 1) : have F := fun (v : ℝ) => chen1973Lemma6Eq19SecondFixedPower x L level B k m H D Q σ r * (1 + v) ^ 2 / chen1973Lemma6Eq17CorrectedKernel x (↑σ + ↑v * Complex.I); MeasureTheory.IntegrableOn F (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (v : ℝ) in Set.Ioi 0, F v ≤ 2 * Real.log ↑x ^ (22 / 5) / σ * chen1973Lemma6Eq19SecondFixedPower x L level B k m H D Q σ r * ∫ (v : ℝ) in Set.Ioi 0, chen1973Lemma6Eq19QuadraticDecay v

Explicit beta-envelope integral and bound, with neither a caller-supplied growth hypothesis nor a continuity hypothesis.