Chen 1973, Lemma 6, equation (19): final Hölder reduction

This module closes the second, three-factor Hölder step on the literal equation-(17) cell and imports the uniform equation-(14), equation-(15), L', and exact prime-pair-energy interfaces. It deliberately stops before claiming the final x / log(x)^20 estimate: that final cell still requires the equation-(17) height-integration assembly.

theorem AnalyticNumberTheory.LargeSieve.eq19_weighted_sum_sqrt_mul_sqrt_le {ι : Type u_1} (S : Finset ι) (w f g : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (hf : ∀ (i : ι), 0 ≤ f i) (hg : ∀ (i : ι), 0 ≤ g i) : ∑ i ∈ S, w i * (√(f i) * √(g i)) ≤ √(∑ i ∈ S, w i * f i) * √(∑ i ∈ S, w i * g i)

Weighted Cauchy-Schwarz for nonnegative conductor weights and factors.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6B_le_moment_product (x L level B k m H : ℕ) (s : ℂ) : chen1973Lemma6B x L level B k m H s ≤ √(chen1973Lemma6Eq19PairSecondMoment x L level B k m s) * √(√(chen1973Lemma6Eq19LDerivFourthMoment x L level s) * √(chen1973Lemma6Eq19MobiusFourthMoment x L level H s))

The second displayed Hölder step in (19). All factors are the literal pair polynomial, natural Möbius polynomial, and totalized primitive L' from (17); there is no free analytic function and no conclusion-shaped premise.