AnalyticNumberTheory.LargeSieve.PanTypeIAssembly #

Primitive-to-all-character reductions for Type I mean values #

This module relates the primitive-character Bombieri--Davenport estimate bombieriDavenport_vaughanFirst in BombieriDavenport.lean to weighted all-character Type I expressions. It proves structural reductions and records further inputs as explicit propositions; it does not prove the unrestricted uniform target below.

Available estimates:

bombieriDavenport_vaughanFirst (Q m u) (hQ : 0 < Q): Σ_{1≤q≤Q} (q/φ(q))·Σ_{χ primitive mod q} ‖V_χ(m)‖² ≤ LSB(m+1, 1/Q²)·S(m), where S(m) = Σ_{n≤m} vaughanFirst(n,u)².
panTypeICharSqSum_le_additiveSieve q m u hq: for each modulus, t_q(m) := Σ_{χ mod q} ‖V_χ(m)‖² ≤ (φ(q)/q)·LSB(m+1, 1/q²)·S(m).
panTypeI_charAbsSum_le_cs: Σ_χ‖V_χ‖ ≤ √φ(q)·√(t_q(m)).
panTypeICharSqrtMeanMaxY_le_sieveSqrtSum: panTypeICharSqrtMeanMaxY X q x f u ≤ Σ_{y≤x}Σ_{a≤X} |f(a)|/|log(y/a)| ·√((φ/q)·LSB(y/a+1,1/q²))·√S(y/a).

The target panTypeICharMeanSieveBound x f u in PanMeanValueBody.lean is Σ_{q≤Q} μ²(q)3^{ω(q)}·√φ(q)·panTypeICharSqrtMeanMaxY X q (xX) f u ≤ C·xX/log^A(xX), with Q = (xX)^{1/2}/log^B(xX).

Limitation: the target is false uniformly over all |f| ≤ 1 #

Take u = 1, so vaughanFirst(n,1) = log n, and f = 1_{a = 1} (f(1) = 1, zero elsewhere). Set y = xX, a = 1. The principal character χ₀ mod q contributes to t_q: ‖V_{χ₀}(xX)‖ = Σ_{n≤xX, (n,q)=1} log n ~ (φ(q)/q)·xX·log(xX), by elementary density estimates, without the PNT. Since the maximum over y includes y = xX and all terms are nonnegative,

LHS ≥ (1/log(xX))·Σ_{q≤Q} μ²(q)3^{ω(q)}·√φ(q)·‖V_{χ₀}(xX)‖
    ~ xX·Σ_{q≤Q} μ²(q)3^{ω(q)}·φ(q)^{3/2}/q
    ≥ xX·Σ_{p≤Q, p prime} 3·(p−1)^{3/2}/p.

The prime sum has order Q^{3/2}/log Q, giving order (xX)^{7/4}/(log xX)^{1+3B/2}. This exceeds C·xX/log^A(xX) for any fixed A, B, C and sufficiently large xX. Thus uniformity over all (∀ a, |f a| ≤ 1) is impossible. The classical Type I mean-value theorem (Liu 2022 §III Lemma 1; HR 1974 Ch. 10) uses support conditions on f. For Chen weights f(a) = 1_{a = p₁p₂, z ≤ p₁ ≤ p₂}, one has f(1) = 0 and control of Σ_{a≤X}|f(a)|/a. The proposed support-sensitive input panTypeI_charMeanSieveBound_chenWeight is recorded in §S4; its precise hypotheses still require comparison with the classical sources.

S2: Conductor decomposition #

For χ mod q, let q' = χ.conductor, with q' | q, and let χ' be its unique primitive character. Mathlib provides χ.FactorsThrough q', χ.primitiveCharacter, and primitive-character induction. For (n,q)=1, χ(n) = χ'(n mod q'); otherwise χ(n) = 0, by the convention for nonunits. Consequently,

V_χ(m) = Σ_{n≤m, (n,q)=1} vaughanFirst(n,u)·χ'(n mod q'),
‖V_χ(m)‖ ≤ ‖V_χ'(m)‖ + D_q(m),
D_q(m) = Σ_{n≤m, (n,q)>1} |vaughanFirst(n,u)|,
‖V_χ(m)‖² ≤ 2‖V_χ'(m)‖² + 2·D_q(m)².

Writing P_{q'}(m) = Σ_{χ' primitive mod q'} ‖V_χ'(m)‖², a sharper grouping argument with fiber bound φ(q)/φ(q') would give t_q(m) ≤ 2·Σ_{q'|q} (φ(q)/φ(q'))·P_{q'}(m) + 2·φ(q)·D_q(m)². The theorem here instead proves the coarser coefficient φ(q), by termwise domination and fiber cardinality, without a dependent grouping bijection. An injectivity-based coefficient 1 is not established here. The related star_conductor and star_isPrimitive lemmas are used elsewhere in the project.

S2a panTypeI_char_induced_by_primitive: pointwise induction.
S2b panTypeI_sqSum_primitiveDecomposition: square-sum decomposition with the coarse coefficient and the density term.
S2c panTypeI_nonCoprimeDensity_le_primePartition: structural bound D_q(m) ≤ Σ_{p|q} Σ_{n≤m, p|n} |vaughanFirst(n,u)|. A quantitative density estimate would substitute n = p·k, use vaughanFirst_abs_le, namely |vaughanFirst(n,u)| ≤ τ(n)·log(n+1), and estimate Σ_{k≤m/p} τ(pk)·log(pk+1) ≤ C·(1/p)·m·log²(m+2)·polylog(p). The full density estimate is not proved in this module.

S3: μ²3^ω weight estimates #

The elementary estimates relevant to assembly have the following shapes:

(W1) Σ_{q≤Q} μ²(q)3^{ω(q)}·φ(q)/q ≤ C·Q·log⁶(Q+2)
     [φ(q)/q ≤ 1 and Σ μ²3^ω ≤ C·Q·log³(Q+2)]
(W2) Σ_{k≤Q/q'} μ²(q'k)3^{ω(q'k)}·(q'k)
     ≤ C·(Q²/q')·3^{ω(q')}·log⁶(Q+2)
     [q = q'·k, μ²(q'k) ≤ μ²(k),
      3^{ω(q'k)} ≤ 3^{ω(q')}·3^{ω(k)},
      Σ_{k≤K} μ²3^ω·k ≤ C·K²·log³(K+2)]
(W3) Σ_{q≤Q} μ²(q)3^{ω(q)}/φ(q) ≤ C·log⁶(Q+2).

W1 and W2 use the same elementary ingredients as PanMainTerm.lean §4: subset expansion, sum_squarefree_prod_primeFactors_le_prod_one_add, and Mertens' second theorem mertensSecond_nat. W3 is supplied by panMainTotientWeightedSum_le_polylog, restated here as panTypeI_totientWeightSum_polylog. The definition panTypeI_threeOmegaWeightSums records the estimate family; it is not a proof of uniform W1 or W2.

S4: Square-root reduction and assembly inputs #

(1) Cauchy--Schwarz algebra: csSqrtSum_le_card_mul_sum proves (Σ_i √(a_i·b_i))² ≤ (card s)·Σ_i a_i·b_i for a_i·b_i ≥ 0. With a_q = w_q·φ(q)/q, b_q = w_q·q·t_q(m), and w_q = μ²3^ω, this yields (Σ_q w_q·√(φ(q)·t_q(m)))² ≤ (card)·Σ_q w_q²·φ(q)·t_q(m). The related weighted Cauchy--Schwarz approach separates factors involving Σ_q (φ(q)/q) and Σ_q q·t_q(m); for q ≤ Q, q·t_q(m) ≤ Q·(q/φ(q))·t_q(m) since φ(q) ≤ q.

(2) All-character BD-shaped input: panTypeI_allCharSieveMean records Σ_{q≤Q} μ²3^ω·(q/φ(q))·t_q(m) ≤ C·(m+Q²)·S(m)·log⁶(Q+2). The proposed route is conductor decomposition, reordering with q = q'·k, applying bombieriDavenport_vaughanFirst to P_{q'}(m) for q' ≤ Q, and controlling the non-coprime term by a density estimate. The weaker large-sieve constant has shape LSB(m+1, 1/Q²) ~ m + Q²·log Q; see the discussion in BombieriDavenport.lean. For a fixed divisor q', weight transfer gives (φ(q)/φ(q'))·(q/φ(q)) = q/φ(q'). The W2 factor Q²/q' introduces an extra Q² in naive assembly. An argument using the (q'/φ(q'))-weighted primitive bound together with W1/W3 therefore requires precise weight bookkeeping; no uniform all-character conclusion is supplied by this definition.

(3) Outer (y,a) weights: after replacing the maximum using panTypeICharSqrtMeanMaxY_le_sieveSqrtSum, the remaining expression has the form Σ_{y,a} |f(a)|/|log(y/a)|·(φ(q)/√q)·√LSB·√S. Control of Σ_{a≤X}|f(a)|/a for Chen weights is central to this step; the counterexample above excludes uniformity under |f| ≤ 1 alone. References: Liu 2022 §III Lemma 1; HR 1974 Ch. 10.

The proved components are pointwise induction, the norm and square reductions, the coarse fiber decomposition, the prime-partition density bound, Cauchy--Schwarz algebra, and W3. Sharper fiber bookkeeping, quantitative density control, uniform weight assembly, and the precise support-sensitive mean-value input remain separate requirements.

AnalyticNumberTheory.LargeSieve.PanTypeIAssembly #

Primitive-to-all-character reductions for Type I mean values #

Limitation: the target is false uniformly over all |f| ≤ 1 #

S2: Conductor decomposition #

S3: μ²3^ω weight estimates #

S4: Square-root reduction and assembly inputs #

S3: The totient-weight sum #

S2: Conductor decomposition and the structural density bound #

S2a: Pointwise induction via mathlib's primitiveCharacter #

Pointwise components of the S2 square-sum decomposition #

S2b: Primitive-character decomposition by termwise bounds and fiber cardinality #

S2c: Structural non-coprime density bound #

S3: Propositions recording μ²3^ω weight estimates #

S4: Square-root Cauchy--Schwarz and assembly inputs #