Chen 1973, Lemma 6, equation (19)

This file isolates the finite Cauchy--Schwarz/Hölder step in (19). All four moments below are moments of the literal pair polynomial, 1-LS, S, and L'; no free Phi occurs. The legacy height uses a natural ceiling with the finite conductor maximum W; the printed exponential cutoff H = 2^l (log x)^200 I_{l,x} is treated in SourceWeightHeight.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I (x L level : ℕ) : ℝ

The actual conductor maximum W, not the printed exponential I_{l,x}. Equation18Weight proves W² ≤ I_{l,x}; the legacy name Eq19I is retained. The inserted value 1 makes the maximum total, including an empty cell.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I x L level = ({1} ∪ Finset.image (fun (d : ℕ) => 3 ^ d.primeFactors.card) (AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L level)).max' ⋯

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19Height (x L level : ℕ) : ℕ

Legacy max-weight cutoff. The printed cutoff uses the larger exponential I; see Eq19PrintedHeight in SourceWeightHeight. This definition is retained for existing coarse-budget consumers, not asserted equal to the source cutoff.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19Height x L level = ⌈2 ^ level * Real.log ↑x ^ 200 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I x L level⌉₊

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19I_pos (x L level : ℕ) : 0 < chen1973Lemma6Eq19I x L level

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_threePow_le_Eq19I {x L level d : ℕ} (hd : d ∈ chen1973Lemma6ConductorBlock x L level) : 3 ^ d.primeFactors.card ≤ chen1973Lemma6Eq19I x L level

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19Height_cast_ge (x L level : ℕ) : 2 ^ level * Real.log ↑x ^ 200 * chen1973Lemma6Eq19I x L level ≤ ↑(chen1973Lemma6Eq19Height x L level)

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

The literal pair-polynomial second moment occurring in (19), with the same squarefree cell weight as equation (17).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PairSecondMoment x L level B k m s = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L level, AnalyticNumberTheory.LargeSieve.eq19Weight✝ d * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, ‖AnalyticNumberTheory.LargeSieve.eq19PairPolynomial✝ x B k m s χ‖ ^ 2

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

The literal equation-(14) factor, retained on the actual equation-(17) cell weight.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19OneSubSecondMoment x L level H s = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L level, AnalyticNumberTheory.LargeSieve.eq19Weight✝ d * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, ‖AnalyticNumberTheory.LargeSieve.chen1973Lemma6OneSubLS H s χ‖ ^ 2

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

The literal equation-(15) fourth moment on the equation-(17) cell.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19MobiusFourthMoment x L level H s = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L level, AnalyticNumberTheory.LargeSieve.eq19Weight✝ d * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, ‖AnalyticNumberTheory.LargeSieve.chen1973Lemma6NaturalMobiusPolynomial H s χ‖ ^ 4

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

The fourth moment of the actual totalized derivative in the second term of (17).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19LDerivFourthMoment x L level s = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L level, AnalyticNumberTheory.LargeSieve.eq19Weight✝ d * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, ‖AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLDeriv d s χ‖ ^ 4

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6A_le_moment_product (x L level B k m H : ℕ) (s : ℂ) : chen1973Lemma6A x L level B k m H s ≤ √(chen1973Lemma6Eq19PairSecondMoment x L level B k m s) * √(chen1973Lemma6Eq19OneSubSecondMoment x L level H s)

The first displayed Cauchy--Schwarz step of (19), before inserting the paid equation-(14) scalar bound.