Chen 1973, Lemma 6, equation (12)

This module performs the finite, source-faithful part of (12). In particular chen1973Lemma6ActualPhi is the switched von-Mangoldt/Perron kernel itself; no free function called Phi occurs in any statement below. The unconditional Bromwich theorem imported through Lemma 5 identifies every occurrence of chen1973PerronKernelFinite with Chen's vertical integral.

The paper subsequently replaces 1 / φ(l) by O(log x / l) and pays the outer squarefree 3^ν/φ sum by O((log x)^5). These two scalar estimates are kept as two separately typed inequalities in the final theorem, rather than being hidden in a hypothesis having equation (12) itself as its conclusion.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6ActualPhi (x d : ℕ) (χ : PrimitiveCharacter d) (pp : ℕ × ℕ) : ℂ

The actual Φ(x/(p₁p₂),χ) after unconditional Bromwich inversion: it is the finite switched Λ(n) sum with Chen's literal Perron kernel. The source's factor 1 / log(x/(p₁p₂)) is outside Φ in (12), so it is deliberately not part of this definition.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6ActualPhi x d χ pp = ∑ n ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5NCarrier x pp, ↑(ArithmeticFunction.vonMangoldt n) * ↑(AnalyticNumberTheory.LargeSieve.chen1973PerronKernelFinite (↑x) (↑x / (↑pp.1 * ↑pp.2 * ↑n))) * ↑χ ↑n

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_primitiveTwist_eq_actualPhi (x d : ℕ) (χ : PrimitiveCharacter d) : chen1973Lemma5PrimitiveTwist x d χ = star (↑χ ↑x) * ∑ pp ∈ chen1973Lemma5PrimePairs x, ↑(Real.log (↑x / (↑pp.1 * ↑pp.2)))⁻¹ * chen1973Lemma6ActualPhi x d χ pp * ↑χ ↑(pp.1 * pp.2)

Regroup the actual primitive twist by prime pairs. This is the finite counterpart of inserting the unconditional Bromwich formula; no interchange of conditionally convergent infinite sums is involved.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_primitiveTwistCoprime_eq_actualPhi (x l d : ℕ) (χ : PrimitiveCharacter l) : chen1973Lemma5PrimitiveTwistCoprime x l d χ = star (↑χ ↑x) * ∑ pp ∈ chen1973Lemma5PrimePairs x with (pp.1 * pp.2).Coprime d, ↑(Real.log (↑x / (↑pp.1 * ↑pp.2)))⁻¹ * chen1973Lemma6ActualPhi x l χ pp * ↑χ ↑(pp.1 * pp.2)

The same finite Bromwich regrouping after retaining exactly the source prime-pair condition (p₁p₂,d)=1.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmTotient (x D m : ℕ) : ℝ

The conductor expression before the paper replaces φ(l) by l/log x. The parameter m is exactly the source coprimality grouping (p₁p₂,m)=1.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmTotient x D m = ∑ l ∈ Finset.range (D + 1) with l.Coprime x ∧ Squarefree l, ↑(ArithmeticFunction.moebius l) ^ 2 * 3 ^ l.primeFactors.card / ↑l.totient * ‖∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter l, if ↑χ = 1 then 0 else star (↑χ ↑x) * ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimePairs x with (pp.1 * pp.2).Coprime m, ↑(Real.log (↑x / (↑pp.1 * ↑pp.2)))⁻¹ * AnalyticNumberTheory.LargeSieve.chen1973Lemma6ActualPhi x l χ pp * ↑χ ↑(pp.1 * pp.2)‖

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Nm (x D m : ℕ) : ℝ

The literal N_m weight printed after (12), with l rather than φ(l) in the denominator.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Nm x D m = ∑ l ∈ Finset.range (D + 1) with l.Coprime x ∧ Squarefree l, |↑(ArithmeticFunction.moebius l)| * 3 ^ l.primeFactors.card / ↑l * ‖∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter l, if ↑χ = 1 then 0 else star (↑χ ↑x) * ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimePairs x with (pp.1 * pp.2).Coprime m, ↑(Real.log (↑x / (↑pp.1 * ↑pp.2)))⁻¹ * AnalyticNumberTheory.LargeSieve.chen1973Lemma6ActualPhi x l χ pp * ↑χ ↑(pp.1 * pp.2)‖

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmMax (x D M : ℕ) : ℝ

A total finite maximum over the printed range 1 < m ≤ M. The modulus cutoff D in N_m and the upper endpoint M of the maximum are kept separate: on p. 119 they are respectively x^(1/2-ε) and x^(1/2). Inserting 0 makes the definition total when that range is empty.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmMax x D M = ({0} ∪ Finset.image (AnalyticNumberTheory.LargeSieve.chen1973Lemma6Nm x D) (Finset.Icc 2 M)).max' ⋯

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Nm_le_max {x D M m : ℕ} (hm : 2 ≤ m) (hmM : m ≤ M) : chen1973Lemma6Nm x D m ≤ chen1973Lemma6NmMax x D M

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmMax_nonneg (x D M : ℕ) : 0 ≤ chen1973Lemma6NmMax x D M

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2_eq_NmTotient_of_allPrimePairsCoprime {x D m : ℕ} (hpair : ∀ pp ∈ chen1973Lemma5PrimePairs x, (pp.1 * pp.2).Coprime m) : chen1973Lemma5M2 x D = chen1973Lemma6NmTotient x D m

This identity is valid only under the deliberately strong hypothesis that one fixed m is coprime to every prime pair. It is not the outer-d regrouping used in equation (12).

def AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterDivisors (x D : ℕ) : Finset ℕ

The genuine outer d carrier immediately before (12), reusing the Lemma-5 source definition rather than introducing a second carrier.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterDivisors x D = AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2OuterDivisors x D

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterWeight (d : ℕ) : ℝ

The p. 119 outer weight 3^ν(d)|μ(d)|/φ(d).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterWeight d = AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2OuterWeight d

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterWeight_nonneg (d : ℕ) : 0 ≤ chen1973Lemma6OuterWeight d

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2SourceInner_eq_NmTotient (x D d : ℕ) : chen1973Lemma5M2SourceInner x D d = chen1973Lemma6NmTotient x D d

At a fixed outer divisor, the Lemma-5 inner source is exactly the totient-denominator N_d ledger used before equation (12).

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterTotientSum (x D : ℕ) : ℝ

The expression after the true outer-d regrouping and before replacing the inner reciprocal totient by the literal reciprocal modulus in N_d.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterTotientSum x D = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterDivisors x D, AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterWeight d * AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmTotient x D d

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2Source_eq_outerTotientSum (x D : ℕ) : chen1973Lemma5M2Source x D = chen1973Lemma6OuterTotientSum x D

The true p. 119 outer grouping is unconditional: both sides are the same outer-d / inner-l source, with (p₁p₂,d)=1 retained before norms.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterLiteralSum (x D : ℕ) : ℝ

The same outer grouping after the pointwise totient-to-modulus estimate.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterLiteralSum x D = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterDivisors x D, AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterWeight d * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Nm x D d

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterWeightSum (x D : ℕ) : ℝ

Total p. 119 outer weight, estimated there by O((log x)^5).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterWeightSum x D = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterDivisors x D, AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterWeight d

def AnalyticNumberTheory.LargeSieve.Chen1973Equation12OuterGrouping (x D : ℕ) : Prop

The genuine source regrouping proposition preceding (12). It is a proved fact, not a caller-supplied equation-(12) hypothesis.

Equations

• AnalyticNumberTheory.LargeSieve.Chen1973Equation12OuterGrouping x D = (AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2Source x D = AnalyticNumberTheory.LargeSieve.chen1973Lemma6OuterTotientSum x D)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_outerGrouping (x D : ℕ) : Chen1973Equation12OuterGrouping x D

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation12_of_outerGrouping {x D M : ℕ} (hx : 1 ≤ x) (hDM : D ≤ M) (htotient : ∀ d ∈ chen1973Lemma6OuterDivisors x D, chen1973Lemma6NmTotient x D d ≤ Real.log ↑x * chen1973Lemma6Nm x D d) (hweight : chen1973Lemma6OuterWeightSum x D ≤ Real.log ↑x ^ 5) : chen1973Lemma5M2Source x D ≤ Real.log ↑x ^ 6 * chen1973Lemma6NmMax x D M

Source equation (12), consuming the two-layer source object and conditional only on the two scalar estimates printed immediately after the now-proved outer grouping: the pointwise φ(l)-to-l replacement and the total outer-weight bound. No single m is chosen uniformly for all prime pairs.