AnalyticNumberTheory.Sieve.PanMeanValueBody #
Finite reductions for weighted Pan mean values #
This module supplies reductions toward PanMeanValueUniform
(WeightedPan.lean), following Liu 2022 §II--§III:
- Sections 1--2 absorb a coprime scaling factor
ainto the residue class:π(y;a,q,l) = π(y/a;q,l·a⁻¹). The Pan expression becomes a weighted sum of ordinary arithmetic-progression prime counts. - Section 3 proves nonnegativity and maximum-to-sum bounds for
panMaxLandpanMaxY. - Sections 4--5 record Type I, Type II, and main-term input propositions and prove the finite character-expansion/Cauchy--Schwarz reductions.
Section 1 defines natInvMod q a and proves
a·p ≡ l [MOD q] ⟺ p ≡ natInvMod q a · l [MOD q] for (a,q)=1.
Section 2 uses this and a·p ≤ y ⟺ p ≤ y/a for positive a to prove
primesInAPBelow y a q l = primesInAP (y/a) q (natInvMod q a · l % q).
The counting bijection is the identity on p.
Consequently the distribution error is
π(y/a;q,l·a⁻¹) − li(y/a)/φ(q), with natural division in the
prime-count cutoff and real division in the main-term argument.
Here li denotes the project's x/log x proxy.
The weighted sum becomes
Σ_{1≤a≤X} [a.Coprime q]·f(a)·(π(y/a;q,l·a⁻¹) − li(y/a)/φ(q))
plus the explicitly separated a = 0 term. This is an exact identity,
not an asymptotic error term.
Related inputs include the Farey-point large sieve
LargeSieve.Multiplicative.largeSieveRationalPoints, the per-modulus
character bound characterSieveModulus_le, Vaughan's identity
(Sieve.VaughanIdentity), and the squarefree weight identity
3^{ω(q)} = Σ_{d|q} 2^{ω(d)} in WeightedPan.
The Type I and Type II reductions are conditional:
PanTypeIWeightedBound.of_characterMeanValue and
PanTypeIIWeightedBound.of_characterMeanValue require their
respective character-mean inputs. The later square-mean reductions
do not prove those analytic inputs or an unrestricted uniform
all-character bound. Further assembly is in PanAssembly.lean;
the main-term distinction is described in PanMainTerm.lean.
1. Inverse residues and congruence cancellation modulo q #
Inverse residue modulo q: when (a,q)=1, take the natural
representative of the inverse of a in ZMod q. ZMod.val is the
least nonnegative representative, or the absolute value at modulus 0.
It satisfies a·b ≡ 1 [MOD q]. Otherwise use 0; the inverse
properties are only used under the coprimality hypothesis.
Equations
- AnalyticNumberTheory.Sieve.natInvMod q a = if _h : a.Coprime q then (↑a)⁻¹.val else 0
Instances For
Cancellation by an invertible factor: if a·b ≡ 1 [MOD q],
then a·p ≡ l [MOD q] ⟺ p ≡ b·l [MOD q].
This is the congruence step in Liu §II's absorption of a:
replace the congruence on the coprime multiple a·p by a residue
condition on p.
2. Absorbing a as in Liu §II: scaled counts and weighted errors #
Scaled count as an ordinary AP count (Liu §II):
for (a,q)=1 and a ≥ 1,
π(y;a,q,l) = π(y/a;q,l·a⁻¹).
Among primes,
#{p : a·p ≤ y, a·p ≡ l [MOD q]} = #{p : p ≤ y/a, p ≡ l·a⁻¹ [MOD q]}.
Division is in ℕ, since the integer solutions of a·p ≤ y
satisfy p ≤ ⌊y/a⌋.
Distribution-error form of a-absorption (Liu §II):
for (a,q)=1 and a ≥ 1,
Δ(y;a,q,l) = π(y/a;q,l·a⁻¹) − li(y/a)/φ(q).
The li proxy uses the real argument (y : ℝ)/a, whereas
the prime count uses natural division y/a. This distinction must
be retained when comparing the main term with the sieve main term.
Weighted distribution sum in Liu §II form: for any f,
Σ_{(a,q)=1, a≤X} f(a)·Δ(y;a,q,l) equals
Σ_{1≤a≤X} [a.Coprime q]·f(a)·(π(y/a;q,l·a⁻¹) − li(y/a)/φ(q))
plus the a = 0 term.
That term can be nonzero only when q = 1, since
0.Coprime q ↔ q = 1. It is left unreduced and explicit:
the classical sum starts at 1, so separating it preserves exactness.
3. Maximum bounds for panMaxL and panMaxY #
The residue maximum is bounded by the sum of absolute values:
max_l |·| ≤ Σ_l |·|.
The y-maximum panMaxY is bounded by the sum of
the individual panMaxL values.
Combined bound:
panMaxY ≤ Σ_{y≤x} Σ_{(l,q)=1} |panDistributionSum y X q l f|.
It replaces both maxima by finite sums for termwise Type I/II estimates.
4. Type I, Type II, and main-term input propositions #
After a-absorption, the classical argument (Liu 2022 §III;
Halberstam--Richert 1974 Ch. 10) separates Vaughan V1 with d ≤ u,
V3 with d > u, e > v, and the signed small/middle/main-term
contribution involving li and the middle Vaughan term.
The def ... : Prop declarations below record bounds as explicit
analytic inputs; defining them does not prove them.
The relevant analytic ingredients are the Farey-point large sieve
LargeSieve.Multiplicative.largeSieveRationalPoints, the per-modulus
character bound characterSieveModulus_le, Vaughan's identity in
Sieve.VaughanIdentity, and prime-distribution main-term estimates.
The pure-li bound below is deliberately coarse and does not replace
the signed classical main-term estimate.
AP von Mangoldt count after a-absorption:
Σ_{n≤y, n≡l [MOD q]} Λ(n), the AP version of ψ.
Applying vaughanIdentity to each Λ n supplies the Type I/II
pieces apV1 and apV3 together with the small and middle terms.
Equations
- AnalyticNumberTheory.Sieve.apVonMangoldt y q l = ∑ n ∈ Finset.range (y + 1), if n ≡ l [MOD q] then ArithmeticFunction.vonMangoldt n else 0
Instances For
Type I piece (Vaughan V1):
Σ_{n≤y, n≡l [MOD q]} Σ_{d|n, d≤u} μ(d)·log(n/d).
Equations
- AnalyticNumberTheory.Sieve.apV1 y q l u = ∑ n ∈ Finset.range (y + 1), if n ≡ l [MOD q] then AnalyticNumberTheory.Sieve.vaughanFirst n u else 0
Instances For
Type II piece (Vaughan V3):
Σ_{n≤y, n≡l [MOD q]} Σ_{d|n, u<d} Σ_{e|n/d, v<e} μ(d)·Λ(e).
Equations
- AnalyticNumberTheory.Sieve.apV3 y q l u v = ∑ n ∈ Finset.range (y + 1), if n ≡ l [MOD q] then AnalyticNumberTheory.Sieve.vaughanThird n u v else 0
Instances For
Weighted piece before maxima:
Σ_{1≤a≤X, (a,q)=1} f(a)·g(y/a,q,l·a⁻¹ mod q).
This is the a-absorbed expression for any piece g.
Only positive a occur; the zero term is separated in
panDistributionSum_eq_weighted.
Equations
- AnalyticNumberTheory.Sieve.panPieceSum y X q l f g = ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * g (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) else 0
Instances For
Residue maximum of a weighted piece, mirroring panMaxL.
Equations
- AnalyticNumberTheory.Sieve.panPieceMaxL y X q f g = if h : (AnalyticNumberTheory.Sieve.unitResidues q).Nonempty then (Finset.image (fun (l : ℕ) => |AnalyticNumberTheory.Sieve.panPieceSum y X q l f g|) (AnalyticNumberTheory.Sieve.unitResidues q)).max' ⋯ else 0
Instances For
Truncation maximum of a weighted piece, mirroring panMaxY.
Equations
- AnalyticNumberTheory.Sieve.panPieceMaxY X q x f g = (Finset.image (fun (y : ℕ) => AnalyticNumberTheory.Sieve.panPieceMaxL y X q f g) (Finset.range (x + 1))).max' ⋯
Instances For
Type I weighted-bound proposition: for each A > 0, there
exist C > 0, B, and x₀ such that for every X ≥ x₀, with
Q = (xX)^{1/2}/log^B(xX),
Σ_{q≤Q} μ²(q)·3^{ω(q)}·max_{y≤xX} max_{(l,q)=1} |Σ_{1≤a≤X, (a,q)=1} f(a)·apV1(y/a;q,l·a⁻¹;u)/log(y/a)| ≤ C·xX/log^A(xX).
The classical small-factor argument uses character expansion and a
Farey-point large-sieve mean estimate (Liu §III Lemma 1; HR 1974 Ch. 10).
This declaration is for fixed x,f,u; it does not establish
uniformity over all |f| ≤ 1, which requires additional support
conditions as discussed in LargeSieve/PanTypeIAssembly.lean.
Equations
- AnalyticNumberTheory.Sieve.PanTypeIWeightedBound x f u = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ) (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → (∑ q ∈ Finset.range (⌊x X ^ (1 / 2) / Real.log (x X) ^ B⌋₊ + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panPieceMaxY X q ⌊x X⌋₊ f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV1 y q l u / Real.log ↑y) ≤ C * x X / Real.log (x X) ^ A
Instances For
Type II weighted-bound proposition for the bilinear Vaughan V3
piece. The classical argument bounds bilinear expressions with
|α|, |β| ≤ 1 using a large-sieve mean estimate on Farey points
(largeSieveRationalPoints) for
Σ_{q≤Q} Σ_{(l,q)=1} |Σ α(d)β(e)·e(de·l/q)|²,
then applies Cauchy--Schwarz (Liu §III; Montgomery's mean-value theorem).
The proposition below is an input, not a proof of that uniform estimate.
Equations
- AnalyticNumberTheory.Sieve.PanTypeIIWeightedBound x f u v = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ) (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → (∑ q ∈ Finset.range (⌊x X ^ (1 / 2) / Real.log (x X) ^ B⌋₊ + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panPieceMaxY X q ⌊x X⌋₊ f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV3 y q l u v / Real.log ↑y) ≤ C * x X / Real.log (x X) ^ A
Instances For
Pure main-term weighted bound, polylogarithmic form:
Σ_{q≤Q} μ²(q)·3^{ω(q)}·max |Σ_{(a,q)=1} f(a)·li(y/a)/φ(q)| ≤ C·xX·(log xX)^{A+7}.
Classically, subtraction of the sieve main term
x/log x·∏(1-ν(p)) leaves O(x/log^A x)
(Liu 2022 §III; HR 1974 Ch. 10).
That requires a sieve-product object and PNT-level main-term input
such as PrimeDistribution.primeCounting_asymptotic_real, not just
the elementary absolute-value chain here.
The present coarse bound uses a larger log power to absorb a
fixed degree-7 polylogarithmic factor (PanMainTerm.lean §6).
PanMainTermBound.of_sieveBound reduces it to PanMainTermSieveBound,
which follows from PanMainSieveAbsorption under its scale-domination
hypothesis. The classical signed logarithmic-saving main-term input
is a separate requirement.
Equations
- AnalyticNumberTheory.Sieve.PanMainTermBound x f = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ) (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → (∑ q ∈ Finset.range (⌊x X ^ (1 / 2) / Real.log (x X) ^ B⌋₊ + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panPieceMaxY X q ⌊x X⌋₊ f fun (y q x : ℕ) => AnalyticNumberTheory.Sieve.logarithmicIntegral ↑y / ↑q.totient) ≤ C * x X * Real.log (x X) ^ (A + 7)
Instances For
5. Type I reduction to a character mean #
The finite chain for the small-factor V1 piece (d ≤ u) is:
apV1 -- charSum_ap --> V_χ(y,u) = Σ_{n≤y} vaughanFirst(n,u)·χ(n)
-- |apV1| ≤ φ(q)⁻¹·Σ_χ ‖V_χ‖, |χ(l)| = 1 --> termwise triangle bound
-- residue-independent bound --> panPieceMaxL ≤ panTypeIDistributionSum
-- maximum over y --> panPieceMaxY ≤ panTypeIMeanValueMaxY
-- nonnegative weights --> PanTypeICharacterMeanValue → PanTypeIWeightedBound.
The only analytic input to this implication is
PanTypeICharacterMeanValue. The classical approach uses a
multiplicative large-sieve mean for Σ_χ‖V_χ‖² and
Cauchy--Schwarz (Liu 2022 §III Lemma 1; HR 1974 Ch. 10).
The implication does not assert that the input holds without
the required analytic and support conditions.
Complex Type I character sum:
V_χ(y,u) = Σ_{n≤y} vaughanFirst(n,u)·χ(n).
Equations
- AnalyticNumberTheory.Sieve.panTypeIV1CharSum q y u χ = ∑ n ∈ Finset.range (y + 1), ↑(AnalyticNumberTheory.Sieve.vaughanFirst n u) * χ ↑n
Instances For
A Dirichlet character has norm 1 on units: the image of a finite-order unit is a root of unity.
Complex character expansion:
(apV1 y q l u : ℂ) = φ(q)⁻¹·Σ_χ star(χ(l))·V_χ(y,u)
for unit l, directly from charSum_ap.
Type I character-mean expression: for each y, the
a-absorbed weighted piece reduces to
Σ_{1≤a≤X} |f(a)|/|log(y/a)| · Σ_χ ‖V_χ(y/a,u)‖.
Equations
- AnalyticNumberTheory.Sieve.panTypeIDistributionSum y X q f u = ∑ a ∈ Finset.Icc 1 X, |f a| / |Real.log ↑(y / a)| * ∑ χ : DirichletCharacter ℂ q, ‖AnalyticNumberTheory.Sieve.panTypeIV1CharSum q (y / a) u χ‖
Instances For
The distribution sum is nonnegative.
Residue-uniform Type I reduction: for unit l,
|panPieceSum y X q l f g| is bounded by
panTypeIDistributionSum, independently of l.
Residue-maximum reduction:
panPieceMaxL ≤ panTypeIDistributionSum, since the bound is
independent of the residue.
Maximum over y of the character-mean expression,
mirroring panPieceMaxY.
Equations
- AnalyticNumberTheory.Sieve.panTypeIMeanValueMaxY X q x f u = (Finset.image (fun (y : ℕ) => AnalyticNumberTheory.Sieve.panTypeIDistributionSum y X q f u) (Finset.range (x + 1))).max' ⋯
Instances For
Truncation-maximum reduction:
panPieceMaxY ≤ panTypeIMeanValueMaxY, by maximizing the
pointwise bound panPieceMaxL ≤ panTypeIDistributionSum.
Type I character-mean input under |f| ≤ 1, with weight
3^{ω(q)}. It is the remaining analytic hypothesis in the
reduction to PanTypeIWeightedBound. The classical approach uses
a multiplicative large-sieve mean for Σ_χ‖V_χ‖² and
Cauchy--Schwarz; this definition does not establish a uniform
estimate for every bounded f.
Equations
- AnalyticNumberTheory.Sieve.PanTypeICharacterMeanValue x f u = ((∀ (a : ℕ), |f a| ≤ 1) ∧ ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ) (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → ∑ q ∈ Finset.range (⌊x X ^ (1 / 2) / Real.log (x X) ^ B⌋₊ + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panTypeIMeanValueMaxY X q ⌊x X⌋₊ f u ≤ C * x X / Real.log (x X) ^ A)
Instances For
Type I reduction:
PanTypeICharacterMeanValue → PanTypeIWeightedBound.
Character expansion, pointwise estimates, both maximum reductions,
and weight monotonicity are proved here; the character mean itself
remains the analytic hypothesis.
5.1 Type I square-mean reduction #
The proposed analytic chain (Liu 2022 §III Lemma 1; HR 1974 Ch. 10) is
Σ_{q≤Q} μ²(q)·3^{ω(q)}·max_{y≤xX}
Σ_{1≤a≤X} |f(a)|/|log(y/a)|·Σ_χ ‖V_χ(y/a)‖
≤ Σ_{q≤Q} μ²(q)·3^{ω(q)}·√φ(q)·max_{y≤xX}
Σ_{1≤a≤X} |f(a)|/|log(y/a)|·√(Σ_χ ‖V_χ(y/a)‖²).
The inequality follows from Cauchy--Schwarz and the character count
φ(q). A further logarithmic-saving bound would require a
multiplicative large-sieve mean, a square-sum estimate for
vaughanFirst, totient-weight estimates, and the outer (y,a) sum.
This section proves the finite components:
panTypeI_charAbsSum_le_cs, using
DirichletCharacter.card_eq_totient_of_hasEnoughRootsOfUnity;
panTypeIDistributionSum_le_csWeighted;
panTypeIMeanValueMaxY_le_charSqrtMeanMaxY;
panTypeI_weight_nonneg;
panTypeICharSqrtMeanMaxY_le_of_abs_le_one; and
PanTypeICharacterMeanValue.of_sieveBound.
The input is panTypeICharMeanSieveBound, with the separate
square-mean proposition panTypeICharSquareMeanBound.
Primitive-character decomposition and Gauss sums are essential in
the classical Bombieri--Davenport theorem. Directly summing
all-character Parseval bounds does not work: for a_n ≡ 1,
Q = 2, and large N,
Σ_q (q/φ(q))Σ_χ |S(χ)|² ≈ 3N²/2,
whereas C(N,1/4)·N = (N+64)·N.
See Multiplicative.lean; the all-character input is not a
consequence of the primitive-character theorem alone.
Character-sum L² expression t_q(m) = Σ_χ ‖V_χ(m)‖²,
the natural square-mean object for the multiplicative large sieve.
Equations
- AnalyticNumberTheory.Sieve.panTypeICharSqSum q m u = ∑ χ : DirichletCharacter ℂ q, ‖AnalyticNumberTheory.Sieve.panTypeIV1CharSum q m u χ‖ ^ 2
Instances For
Cauchy--Schwarz:
Σ_χ ‖V_χ(m)‖ ≤ √φ(q)·√(Σ_χ ‖V_χ(m)‖²),
using the character count φ(q) and (Σa_i)² ≤ n·Σa_i².
Termwise weighted Cauchy--Schwarz in the distribution sum:
panTypeIDistributionSum y X q f u ≤ √φ(q)·Σ_{1≤a≤X} |f(a)|/|log(y/a)|·√t_q(y/a).
The fixed-y slice of the weighted square-mean expression:
W(y) = Σ_{1≤a≤X} |f(a)|/|log(y/a)|·√t_q(y/a).
Equations
- AnalyticNumberTheory.Sieve.panTypeICharSqrtMean y X q f u = ∑ a ∈ Finset.Icc 1 X, |f a| / |Real.log ↑(y / a)| * √(AnalyticNumberTheory.Sieve.panTypeICharSqSum q (y / a) u)
Instances For
Maximum over y of the weighted square-mean expression,
mirroring panTypeIMeanValueMaxY.
Equations
- AnalyticNumberTheory.Sieve.panTypeICharSqrtMeanMaxY X q x f u = (Finset.image (fun (y : ℕ) => AnalyticNumberTheory.Sieve.panTypeICharSqrtMean y X q f u) (Finset.range (x + 1))).max' ⋯
Instances For
Truncation-maximum reduction:
panTypeIMeanValueMaxY ≤ √φ(q)·panTypeICharSqrtMeanMaxY,
by maximizing the weighted Cauchy--Schwarz bound.
Nonnegative weight: μ²(q)·3^{ω(q)} ≥ 0.
Type I square-mean assembly input: under |f| ≤ 1, for
each A > 0 there are C > 0, B, and x₀ such that
for every X ≥ x₀, with Q = (xX)^{1/2}/log^B(xX),
Σ_{q≤Q} μ²(q)·3^{ω(q)}·√φ(q)·max_{y≤xX} Σ_{1≤a≤X} |f(a)|/|log(y/a)|·√(Σ_χ ‖V_χ(y/a)‖²) ≤ C·xX/log^A(xX).
This is the remaining hypothesis in the reduction to
PanTypeICharacterMeanValue. The classical route combines the
multiplicative large sieve, Cauchy--Schwarz in q, a square-sum
bound for vaughanFirst, totient weights, and the outer (y,a) sum
(Liu 2022 §III Lemma 1; HR 1974 Ch. 10).
The all-character sum is not obtained by direct Parseval stacking;
primitive-character and Gauss-sum analysis is separate
(Multiplicative.lean). Nor does this definition prove uniformity
for all bounded f; see the support obstruction in PanTypeIAssembly.lean.
Equations
- AnalyticNumberTheory.Sieve.panTypeICharMeanSieveBound x f u = ((∀ (a : ℕ), |f a| ≤ 1) ∧ ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ) (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → ∑ q ∈ Finset.range (⌊x X ^ (1 / 2) / Real.log (x X) ^ B⌋₊ + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * √↑q.totient * AnalyticNumberTheory.Sieve.panTypeICharSqrtMeanMaxY X q ⌊x X⌋₊ f u ≤ C * x X / Real.log (x X) ^ A)
Instances For
Type I all-character square-mean proposition:
Σ_{q≤Q} μ²(q)·3^{ω(q)}·Σ_χ ‖V_χ(m)‖² ≤ C·(m+Q²)·Σ_{n≤m} vaughanFirst(n,u)².
The classical Bombieri--Davenport theorem (Montgomery 1971 Ch. 1;
Iwaniec--Kowalski 2004 Ch. 7) uses primitive characters and
Gauss sums |τ(χ)|² = q; direct all-character Parseval stacking
fails, as explained in Multiplicative.lean.
The proposed further assembly also calls for a square-sum estimate
for vaughanFirst (classically of m·log³(m+2) shape),
Σ_{q≤Q} μ²(q)3^{ω(q)}φ(q) ≪ Q²·log³(Q+2),
and a uniform outer-sum bound of the form
Σ_{a≤X} |f(a)|/|log(y/a)|·(y/a)^{1/2}·(y/a+Q²)^{1/2}·log³
for y ≤ xX, followed by Cauchy--Schwarz in q.
The maximum must remain outside the modulus-dependent estimates.
These requirements describe a proposed route to
panTypeICharMeanSieveBound, not a theorem supplied by this definition.
Equations
- AnalyticNumberTheory.Sieve.panTypeICharSquareMeanBound u = ∃ (C : ℝ), 0 < C ∧ ∀ (Q m : ℕ), ∑ q ∈ Finset.range (Q + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panTypeICharSqSum q m u ≤ C * (↑m + ↑Q ^ 2) * ∑ n ∈ Finset.range (m + 1), AnalyticNumberTheory.Sieve.vaughanFirst n u ^ 2
Instances For
Type I square-mean reduction:
panTypeICharMeanSieveBound → PanTypeICharacterMeanValue.
Cauchy--Schwarz, the maximum reduction, nonnegative weights, and
the zero weight at q = 0 are proved here; the supplied mean
estimate is the sole analytic input.
5.2 Type II character and square-mean reductions #
For V3 with u < d, v < e, the finite chain parallels §§5--5.1,
replacing apV1, vaughanFirst, and panTypeI* by
apV3, vaughanThird, and panTypeII*:
apV3 -- charSum_ap --> V_χ(y,u,v) = Σ_{n≤y} vaughanThird(n,u,v)·χ(n)
-- |apV3| ≤ φ(q)⁻¹·Σ_χ ‖V_χ‖ --> termwise triangle bound
-- residue-uniform bound --> panPieceMaxL ≤ panTypeIIDistributionSum
-- maximum over y --> panPieceMaxY ≤ panTypeIIMeanValueMaxY
-- nonnegative weights --> PanTypeIICharacterMeanValue → PanTypeIIWeightedBound
-- Cauchy--Schwarz, character count φ(q) --> panTypeIICharSqSum / panTypeIICharSqrtMeanMaxY
-- panTypeIICharMeanSieveBound --> PanTypeIICharacterMeanValue.of_sieveBound.
The remaining analytic input is panTypeIICharMeanSieveBound.
The classical bilinear route combines a multiplicative large-sieve
mean for Σ_χ‖V_χ‖², a square-sum bound for vaughanThird,
and Cauchy--Schwarz in q (Liu 2022 §III; Montgomery 1971 Ch. 1).
All finite implications here are conditional on that input.
Complex Type II character sum:
V_χ(y,u,v) = Σ_{n≤y} vaughanThird(n,u,v)·χ(n).
Equations
- AnalyticNumberTheory.Sieve.panTypeIIV3CharSum q y u v χ = ∑ n ∈ Finset.range (y + 1), ↑(AnalyticNumberTheory.Sieve.vaughanThird n u v) * χ ↑n
Instances For
Complex character expansion:
(apV3 y q l u v : ℂ) = φ(q)⁻¹·Σ_χ star(χ(l))·V_χ(y,u,v)
for unit l, directly from charSum_ap.
Type II character-mean expression: for each y, the
a-absorbed weighted piece reduces to
Σ_{1≤a≤X} |f(a)|/|log(y/a)| · Σ_χ ‖V_χ(y/a,u,v)‖.
Equations
- AnalyticNumberTheory.Sieve.panTypeIIDistributionSum y X q f u v = ∑ a ∈ Finset.Icc 1 X, |f a| / |Real.log ↑(y / a)| * ∑ χ : DirichletCharacter ℂ q, ‖AnalyticNumberTheory.Sieve.panTypeIIV3CharSum q (y / a) u v χ‖
Instances For
The distribution sum is nonnegative.
Residue-uniform Type II reduction: for unit l,
|panPieceSum y X q l f g| is bounded by
panTypeIIDistributionSum, independently of l.
Residue-maximum reduction:
panPieceMaxL ≤ panTypeIIDistributionSum, since the bound
is independent of the residue.
Maximum over y of the Type II character-mean expression,
mirroring panTypeIMeanValueMaxY.
Equations
- AnalyticNumberTheory.Sieve.panTypeIIMeanValueMaxY X q x f u v = (Finset.image (fun (y : ℕ) => AnalyticNumberTheory.Sieve.panTypeIIDistributionSum y X q f u v) (Finset.range (x + 1))).max' ⋯
Instances For
Truncation-maximum reduction:
panPieceMaxY ≤ panTypeIIMeanValueMaxY, by maximizing the
pointwise bound panPieceMaxL ≤ panTypeIIDistributionSum.
Type II character-mean input under |f| ≤ 1, with weight
3^{ω(q)}. It is the remaining analytic hypothesis in the
reduction to PanTypeIIWeightedBound. The classical approach uses
a multiplicative large-sieve mean for Σ_χ‖V_χ‖² and
Cauchy--Schwarz; this definition does not itself prove the estimate.
Equations
- AnalyticNumberTheory.Sieve.PanTypeIICharacterMeanValue x f u v = ((∀ (a : ℕ), |f a| ≤ 1) ∧ ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ) (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → ∑ q ∈ Finset.range (⌊x X ^ (1 / 2) / Real.log (x X) ^ B⌋₊ + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panTypeIIMeanValueMaxY X q ⌊x X⌋₊ f u v ≤ C * x X / Real.log (x X) ^ A)
Instances For
Type II reduction:
PanTypeIICharacterMeanValue → PanTypeIIWeightedBound.
Character expansion, pointwise estimates, both maximum reductions,
and weight monotonicity are proved here; the character mean itself
remains the analytic hypothesis.
Character-sum L² expression t_q(m) = Σ_χ ‖V_χ(m)‖²,
the natural square-mean object for the multiplicative large sieve.
Equations
- AnalyticNumberTheory.Sieve.panTypeIICharSqSum q m u v = ∑ χ : DirichletCharacter ℂ q, ‖AnalyticNumberTheory.Sieve.panTypeIIV3CharSum q m u v χ‖ ^ 2
Instances For
Cauchy--Schwarz:
Σ_χ ‖V_χ(m)‖ ≤ √φ(q)·√(Σ_χ ‖V_χ(m)‖²),
using the character count φ(q) and (Σa_i)² ≤ n·Σa_i².
Termwise weighted Cauchy--Schwarz:
panTypeIIDistributionSum y X q f u v ≤ √φ(q)·Σ_{1≤a≤X} |f(a)|/|log(y/a)|·√t_q(y/a).
The fixed-y slice of the weighted square-mean expression:
W(y) = Σ_{1≤a≤X} |f(a)|/|log(y/a)|·√t_q(y/a).
Equations
- AnalyticNumberTheory.Sieve.panTypeIICharSqrtMean y X q f u v = ∑ a ∈ Finset.Icc 1 X, |f a| / |Real.log ↑(y / a)| * √(AnalyticNumberTheory.Sieve.panTypeIICharSqSum q (y / a) u v)
Instances For
Maximum over y of the weighted square-mean expression,
mirroring panTypeICharSqrtMeanMaxY.
Equations
- AnalyticNumberTheory.Sieve.panTypeIICharSqrtMeanMaxY X q x f u v = (Finset.image (fun (y : ℕ) => AnalyticNumberTheory.Sieve.panTypeIICharSqrtMean y X q f u v) (Finset.range (x + 1))).max' ⋯
Instances For
Truncation-maximum reduction:
panTypeIIMeanValueMaxY ≤ √φ(q)·panTypeIICharSqrtMeanMaxY,
by maximizing the weighted Cauchy--Schwarz bound.
Nonnegative weight: μ²(q)·3^{ω(q)} ≥ 0.
Type II square-mean assembly input: under |f| ≤ 1, for
each A > 0 there are C > 0, B, and x₀ such that for
every X ≥ x₀, with Q = (xX)^{1/2}/log^B(xX),
Σ_{q≤Q} μ²(q)·3^{ω(q)}·√φ(q)·max_{y≤xX} Σ_{1≤a≤X} |f(a)|/|log(y/a)|·√(Σ_χ ‖V_χ(y/a)‖²) ≤ C·xX/log^A(xX).
This is the remaining hypothesis in the reduction to
PanTypeIICharacterMeanValue. The classical bilinear route combines
the multiplicative large sieve, Cauchy--Schwarz in q, a square-sum
bound for vaughanThird, totient weights, and the outer (y,a) sum
(Liu 2022 §III; Montgomery 1971 Ch. 1; HR 1974 Ch. 10).
The definition is not an unconditional uniform estimate.
Equations
- AnalyticNumberTheory.Sieve.panTypeIICharMeanSieveBound x f u v = ((∀ (a : ℕ), |f a| ≤ 1) ∧ ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ) (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → ∑ q ∈ Finset.range (⌊x X ^ (1 / 2) / Real.log (x X) ^ B⌋₊ + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * √↑q.totient * AnalyticNumberTheory.Sieve.panTypeIICharSqrtMeanMaxY X q ⌊x X⌋₊ f u v ≤ C * x X / Real.log (x X) ^ A)
Instances For
Type II all-character square-mean proposition:
Σ_{q≤Q} μ²(q)·3^{ω(q)}·Σ_χ ‖V_χ(m)‖² ≤ C·(m+Q²)·Σ_{n≤m} vaughanThird(n,u,v)².
The classical Bombieri--Davenport theorem (Montgomery 1971 Ch. 1;
Iwaniec--Kowalski 2004 Ch. 7) uses primitive-character decomposition
and Gauss sums. The bilinear Type II structure enters after expanding
Vaughan's identity in d,e (Liu 2022 §III).
This declaration records an input, not a proved all-character bound.
Equations
- AnalyticNumberTheory.Sieve.panTypeIICharSquareMeanBound u v = ∃ (C : ℝ), 0 < C ∧ ∀ (Q m : ℕ), ∑ q ∈ Finset.range (Q + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panTypeIICharSqSum q m u v ≤ C * (↑m + ↑Q ^ 2) * ∑ n ∈ Finset.range (m + 1), AnalyticNumberTheory.Sieve.vaughanThird n u v ^ 2
Instances For
Type II square-mean reduction:
panTypeIICharMeanSieveBound → PanTypeIICharacterMeanValue.
Cauchy--Schwarz, the maximum reduction, nonnegative weights, and
the zero weight at q = 0 are proved here; the supplied character
mean is the sole analytic input.