theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_CHWeightedCoefficient_eq_zero_of_le {H n : ℕ} (hn : 0 < n) (hnH : n ≤ H) (s : ℂ) : chen1973Lemma6CHWeightedCoefficient H s ↑n = 0

Actual low-frequency cancellation, not a support assumption.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_CHWeightedCoefficient_norm_le_div {H : ℕ} (hH : 0 < H) {s : ℂ} {m : ℤ} (hs : 1 ≤ s.re) (hm : m ∈ Finset.Icc 1 ↑(H * H)) : ‖chen1973Lemma6CHWeightedCoefficient H s m‖ ≤ ↑m.toNat.divisors.card / ↑m.toNat

Retain the full reciprocal factor on Re(s) ≥ 1.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_CHWeightedCoefficient_weighted_energy (H : ℕ) (hH : 0 < H) (s : ℂ) (hs : 1 ≤ s.re) : ∑ m ∈ Finset.Icc 1 ↑(H * H), ↑m.toNat * ‖chen1973Lemma6CHWeightedCoefficient H s m‖ ^ 2 ≤ (1 + Real.log ↑(H * H)) ^ 4

Weighted energy is exactly the harmonic divisor-square scale.

noncomputable def AnalyticNumberTheory.LargeSieve.eq14DyadicShell (H j : ℕ) : Finset ℤ

Dyadic integer intervals use their actual length H*2^j.

Equations

• AnalyticNumberTheory.LargeSieve.eq14DyadicShell H j = Finset.Ioc ↑(H * 2 ^ j) ↑(H * 2 ^ (j + 1))

theorem AnalyticNumberTheory.LargeSieve.eq14_sum_dyadicShell {A : Type u_1} [AddCommMonoid A] (f : ℤ → A) (H K : ℕ) : ∑ j ∈ Finset.range K, ∑ n ∈ eq14DyadicShell H j, f n = ∑ n ∈ Finset.Ioc ↑H ↑(H * 2 ^ K), f n

Exact disjoint shell recombination, valid for any finite additive sum.

theorem AnalyticNumberTheory.LargeSieve.eq14_dyadicShell_moment (c : ℤ → ℂ) (H j D Q : ℕ) (hH : 0 < H) (hD : 0 < D) : ∑ d ∈ Finset.Ioc D Q, 1 / ↑d.totient * ∑ χ : PrimitiveCharacter d, ‖∑ n ∈ eq14DyadicShell H j, c n * ↑χ ↑n‖ ^ 2 ≤ chen1973Lemma6Eq19SharpConstant * (↑Q / ↑H + 1 / ↑D) * ∑ n ∈ eq14DyadicShell H j, ↑n.toNat * ‖c n‖ ^ 2

Sharp LS is freshly applied to each shell; its length is H*2^j, not H². The upper bound pays the shell's own weighted energy.

theorem AnalyticNumberTheory.LargeSieve.eq14_tail_polynomial_moment (c : ℤ → ℂ) (H X K D Q : ℕ) (hH : 0 < H) (hD : 0 < D) (hHX : H ≤ X) (hXK : X ≤ H * 2 ^ K) (hlow : ∀ n ∈ Finset.Icc 1 ↑H, c n = 0) : ∑ d ∈ Finset.Ioc D Q, 1 / ↑d.totient * ∑ χ : PrimitiveCharacter d, ‖∑ n ∈ Finset.Icc 1 ↑X, c n * ↑χ ↑n‖ ^ 2 ≤ ↑K * chen1973Lemma6Eq19SharpConstant * (↑Q / ↑H + 1 / ↑D) * ∑ n ∈ Finset.Icc 1 ↑X, ↑n.toNat * ‖c n‖ ^ 2

A tail-supported finite polynomial: Cauchy costs one shell count, while disjoint weighted energies are summed without a second loss.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_CH_polynomial_moment_dyadic (H D Q : ℕ) (s : ℂ) (hH : 0 < H) (hD : 0 < D) (hs : 1 ≤ s.re) : ∑ d ∈ Finset.Ioc D Q, 1 / ↑d.totient * ∑ χ : PrimitiveCharacter d, ‖∑ n ∈ Finset.Icc 1 ↑(H * H), chen1973Lemma6CHWeightedCoefficient H s n * ↑χ ↑n‖ ^ 2 ≤ ↑(Nat.log 2 H + 1) * chen1973Lemma6Eq19SharpConstant * (↑Q / ↑H + 1 / ↑D) * (1 + Real.log ↑(H * H)) ^ 4

The CH polynomial bound with its literal logarithmic dyadic count.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq14DyadicConstant : ℝ

Absolute constant fixed before H,D,Q and the complete complex parameter.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq14DyadicConstant = 16 * (1 + 1 / Real.log 2) * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SharpConstant

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq14DyadicConstant_pos : 0 < chen1973Lemma6Eq14DyadicConstant

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_CH_polynomial_moment_fixed_log_five (H D Q : ℕ) (s : ℂ) (hH : 2 ≤ H) (hD : 0 < D) (hs : 1 ≤ s.re) : ∑ d ∈ Finset.Ioc D Q, 1 / ↑d.totient * ∑ χ : PrimitiveCharacter d, ‖∑ n ∈ Finset.Icc 1 ↑(H * H), chen1973Lemma6CHWeightedCoefficient H s n * ↑χ ↑n‖ ^ 2 ≤ chen1973Lemma6Eq14DyadicConstant * (↑Q / ↑H + 1 / ↑D) * (1 + Real.log ↑(H + 1)) ^ 5

The genuine finite polynomial term of (14), on every vertical line Re(s) ≥ 1. The fifth logarithm is the dyadic Cauchy cost; four logarithms come from the globally recombined harmonic divisor-square energy. This theorem does not assert the full printed equation (14): its L-function truncation remainder is deliberately absent.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_CH_polynomial_moment_exists_absolute : ∃ (C : ℝ), 0 < C ∧ ∀ (H D Q : ℕ) (s : ℂ), 2 ≤ H → 0 < D → 1 ≤ s.re → ∑ d ∈ Finset.Ioc D Q, 1 / ↑d.totient * ∑ χ : PrimitiveCharacter d, ‖∑ n ∈ Finset.Icc 1 ↑(H * H), chen1973Lemma6CHWeightedCoefficient H s n * ↑χ ↑n‖ ^ 2 ≤ C * (↑Q / ↑H + 1 / ↑D) * (1 + Real.log ↑(H + 1)) ^ 5

Explicit binder order: one absolute C works for every finite CH polynomial and all imaginary parts of s, with no conductor-order assumption.