AnalyticNumberTheory.LargeSieve.PanTypeIIAssembly

Primitive-character decomposition of panTypeIICharSqSum

For the Type II character sum panTypeIIV3CharSum (the vaughanThird sequence), this module proves the decomposition t_q(m) ≤ 2·Σ_{q' | q} φ(q)·P2_{q'}(m) + 2·φ(q)·D2_q(m)². The argument is parallel to the Type I decomposition in PanTypeIAssembly.lean: pointwise square bounds followed by a bound on fiber cardinality, with the sequence replaced by vaughanThird(n,u,v).

Primitive-character decomposition: termwise bounds and fiber cardinality

noncomputable def AnalyticNumberTheory.LargeSieve.panTypeIIPrimitiveSqSum (q' m u v : ℕ) : ℝ

Primitive-character part: P2_{q'}(m) = Σ_{χ' primitive mod q'} ‖V_χ'(m)‖².

Equations

• AnalyticNumberTheory.LargeSieve.panTypeIIPrimitiveSqSum q' m u v = ∑ χ' : DirichletCharacter ℂ q' with χ'.IsPrimitive, ‖AnalyticNumberTheory.Sieve.panTypeIIV3CharSum q' m u v χ'‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.panTypeIIPrimitiveSqSum_nonneg (q' m u v : ℕ) : 0 ≤ panTypeIIPrimitiveSqSum q' m u v

P2_{q'}(m) ≥ 0, since it is a sum of squares.

noncomputable def AnalyticNumberTheory.LargeSieve.panTypeII_nonCoprimeDensity (q m u v : ℕ) : ℝ

Non-coprime density term: D2_q(m) = Σ_{n ≤ m, (n,q) > 1} |vaughanThird(n,u,v)|.

Equations

• AnalyticNumberTheory.LargeSieve.panTypeII_nonCoprimeDensity q m u v = ∑ n ∈ Finset.range (m + 1), if n.gcd q ≠ 1 then |AnalyticNumberTheory.Sieve.vaughanThird n u v| else 0

theorem AnalyticNumberTheory.LargeSieve.panTypeII_nonCoprimeDensity_nonneg (q m u v : ℕ) : 0 ≤ panTypeII_nonCoprimeDensity q m u v

The non-coprime density term is nonnegative.

theorem AnalyticNumberTheory.LargeSieve.panTypeIIV3CharSum_norm_le_primitive {q m u v : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) : ‖Sieve.panTypeIIV3CharSum q m u v χ‖ ≤ ‖Sieve.panTypeIIV3CharSum χ.conductor m u v χ.primitiveCharacter‖ + panTypeII_nonCoprimeDensity q m u v

Pointwise Type II bound: ‖V_χ(m)‖ ≤ ‖V_{χ.primitiveCharacter}(m)‖ + D2_q(m).

theorem AnalyticNumberTheory.LargeSieve.panTypeIIV3CharSum_sq_le_primitive {q m u v : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) : ‖Sieve.panTypeIIV3CharSum q m u v χ‖ ^ 2 ≤ 2 * ‖Sieve.panTypeIIV3CharSum χ.conductor m u v χ.primitiveCharacter‖ ^ 2 + 2 * panTypeII_nonCoprimeDensity q m u v ^ 2

Type II square bound: ‖V_χ‖² ≤ 2‖V_{χ.prim}‖² + 2·D2_q(m)².

theorem AnalyticNumberTheory.LargeSieve.panTypeII_primitiveFiberSqSum_le {q q' m u v : ℕ} (hq : 0 < q) : ∑ χ : DirichletCharacter ℂ q with χ.conductor = q', ‖Sieve.panTypeIIV3CharSum q' m u v (panTypeI_liftPrimitive q' q χ)‖ ^ 2 ≤ ↑q.totient * panTypeIIPrimitiveSqSum q' m u v

Fiber bound at level q': the contribution of characters modulo q with conductor q' to the primitive-character square sum is at most φ(q)·P2_{q'}(m). The fiber has cardinality at most φ(q), and each term satisfies ‖V_{χ.prim}‖² ≤ P2_{q'}(m).

theorem AnalyticNumberTheory.LargeSieve.panTypeII_sqSum_primitiveDecomposition (q m u v : ℕ) (hq : 0 < q) : Sieve.panTypeIICharSqSum q m u v ≤ 2 * ∑ q' ∈ q.divisors, ↑q.totient * panTypeIIPrimitiveSqSum q' m u v + 2 * ↑q.totient * panTypeII_nonCoprimeDensity q m u v ^ 2

Type II primitive-character decomposition of the all-character square sum, with the coarse coefficient φ(q): t_q(m) ≤ 2·Σ_{q' | q} φ(q)·P2_{q'}(m) + 2·φ(q)·D2_q(m)². This parallels the Type I decomposition, replacing the sequence by vaughanThird. An injectivity-based version with coefficient 1 would require conductor casts; that sharper version is not established here.