Weighted Pan mean-value assembly

This module assembles the separate coarse Vaughan proposition PanVaughanSplitCrude from three input propositions (PanTypeICharacterMeanValue, PanTypeIICharacterMeanValue, PanMainTermSieveBound) and two analytic conditions (PanLogEventuallyLarge, PanVaughanPointwiseSplit). It yields the polylogarithmic PanMeanValueUniformCrude through PanMeanValueUniformCrude.of_vaughanSplit. The classical PanMeanValueUniform is assembled separately by PanMeanValueUniform.of_signedAnalyticInputs.

The mathematical decomposition (Liu 2022 §III Thm 2; Pan 1963) starts from panMaxY X q x f = max_{y≤x} max_l |Σ_a f(a)·Δ(y;a,q,l)|, where Δ(y;a,q,l) = π(y;a,q,l) − li(y/a)/φ(q). Vaughan's identity separates the Type I (apV1), Type II (apV3), and main-term contributions. In this coarse interface the third piece is the absolute pure-li term, with li denoting the project's x/log x proxy. The signed assembly retains the necessary subtraction.

The three bounds are obtained conditionally through PanTypeIWeightedBound.of_characterMeanValue (PanMeanValueBody §5), PanTypeIIWeightedBound.of_characterMeanValue (§5.2), and PanMainTermBound.of_sieveBound (PanMainTerm §2).

The finite algebra proved here consists of:

1. The per-modulus split w_q·panMaxY ≤ w_q·PI + w_q·PII + w_q·PM (panAssembly_pointwise). At q = 0, μ²(q) = 0; for q > 0, use the pointwise input and nonnegative weights.
2. Splitting the modulus sum by sum_add_distrib.
3. Reconciling cutoffs (panAssembly_floor_le): choose B = max B₁ (max B₂ B₃). If log(xX) ≥ 1, then Q_B ≤ Q_{B_i}; nonnegative terms allow enlargement of each range.
4. Bounding the Type I/II terms by C_i·xX/log^A(xX) and the pure main term by C₃·xX·(log xX)^{A+7}. For log(xX) ≥ 1, each Type I/II bound is at most C_i·xX·(log xX)^{A+7}, giving (C₁+C₂+C₃)·xX·(log xX)^{A+7}.

The pure main-term estimate is polylogarithmic: PanMainSieveAbsorption (PanMainTerm.lean §6) absorbs fixed polylogarithmic factors into a larger logarithmic power. It does not yield the classical C·xX/log^A(xX) saving (Liu Thm 2), which requires signed main-term cancellation.

The two coarse analytic inputs are propositions, not unconditional theorems: (a) eventual log(xX) ≥ 1, as follows from xX → ∞; (b) the pointwise conversion from prime AP counts to the apV1/apV3/li pieces. The latter concerns the analytic transition from von Mangoldt counts to prime counts and is not supplied by finite Vaughan algebra alone.

def AnalyticNumberTheory.Sieve.PanVaughanSplitCrude (x f : ℕ → ℝ) (_u _v : ℕ) : Prop

Coarse pure-li Vaughan split, with a polylogarithmic right side: 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)}·panMaxY X q ⌊xX⌋ f ≤ C·xX·(log xX)^{A+7}.

This is definitionally the coarse PanMeanValueUniformCrude proposition, not the classical PanMeanValueUniform. PanVaughanSplitCrude.of_analyticInputs derives it from the three bound inputs and the two analytic conditions. The pure-li piece admits polylogarithmic absorption (PanMainSieveAbsorption, PanMainTerm.lean §6), not a C·xX/log^A(xX) saving. The classical Vaughan argument controls Type I/II by their weighted bounds and retains the signed middle/main-term difference; its logarithmic saving needs that additional analytic cancellation (Liu Thm 2).

Equations

• AnalyticNumberTheory.Sieve.PanVaughanSplitCrude 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.panMaxY X q ⌊x X⌋₊ f ≤ C * x X * Real.log (x X) ^ (A + 7)

def AnalyticNumberTheory.Sieve.PanLogEventuallyLarge (x : ℕ → ℝ) : Prop

Eventual logarithmic lower bound: log(x X) ≥ 1 for all sufficiently large X. This follows classically from x X → ∞ (Liu 2022 §III). It permits cutoff comparison Q_B ≤ Q_{B_i}, using monotonicity of real powers in the exponent for bases at least 1.

Equations

• AnalyticNumberTheory.Sieve.PanLogEventuallyLarge x = ∃ (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → 1 ≤ Real.log (x X)

def AnalyticNumberTheory.Sieve.PanVaughanPointwiseSplit (_x f : ℕ → ℝ) (u v : ℕ) : Prop

Coarse pointwise Vaughan-split input: for each q > 0 and all truncations, the maximum weighted prime-distribution error is bounded by three piecewise maxima:

panMaxY X q x f ≤ panPieceMaxY X q x f (fun y q l => apV1 y q l u / log y) + panPieceMaxY X q x f (fun y q l => apV3 y q l u v / log y) + panPieceMaxY X q x f (fun y q l => li y / φ(q)).

The classical route (Liu 2022 §III Thm 2; HR 1974 Ch. 10) applies Vaughan's identity (vaughanIdentity_threeTerm, VaughanIdentity.lean) to apVonMangoldt (PanMeanValueBody §4), retaining the small and middle terms as well as V1 and V3. Passing from π(y;q,l)·log y to Σ_{n≤y,n≡l} Λ(n) and handling the signed main-term difference require analytic input before taking maxima over y,l. The pure-li inequality here is an explicit coarse assumption, not a consequence of that finite identity alone.

Equations

• AnalyticNumberTheory.Sieve.PanVaughanPointwiseSplit _x f u v = ∀ (X q y : ℕ), 0 < q → AnalyticNumberTheory.Sieve.panMaxY X q y f ≤ ((AnalyticNumberTheory.Sieve.panPieceMaxY X q y f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV1 y q l u / Real.log ↑y) + AnalyticNumberTheory.Sieve.panPieceMaxY X q y f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV3 y q l u v / Real.log ↑y) + AnalyticNumberTheory.Sieve.panPieceMaxY X q y f fun (y q x : ℕ) => AnalyticNumberTheory.Sieve.logarithmicIntegral ↑y / ↑q.totient

theorem AnalyticNumberTheory.Sieve.panPieceMaxL_nonneg (y X q : ℕ) (f : ℕ → ℝ) (g : ℕ → ℕ → ℕ → ℝ) : 0 ≤ panPieceMaxL y X q f g

The piece's l-maximum is nonnegative; when q = 0 the residue set is empty and its value is 0. This mirrors panMaxL_nonneg.

theorem AnalyticNumberTheory.Sieve.panAssembly_floor_le (z L B B' : ℝ) (hz : 0 ≤ z) (hL1 : 1 ≤ L) (hB : B' ≤ B) : ⌊z / L ^ B⌋₊ ≤ ⌊z / L ^ B'⌋₊

Cutoff comparison: if B' ≤ B, 1 ≤ L, and z ≥ 0, then ⌊z/L^B⌋ ≤ ⌊z/L^{B'}⌋. This gives Q_B ≤ Q_{B_i}.

theorem AnalyticNumberTheory.Sieve.panAssembly_sum_le_sum (Q Q' : ℕ) (w : ℕ → ℝ) (hQQ' : Q ≤ Q') (hw : ∀ (q : ℕ), 0 ≤ w q) : ∑ q ∈ Finset.range (Q + 1), w q ≤ ∑ q ∈ Finset.range (Q' + 1), w q

Enlarging a sum: if Q ≤ Q' and w is nonnegative, then Σ_{q ≤ Q} w q ≤ Σ_{q ≤ Q'} w q.

theorem AnalyticNumberTheory.Sieve.PanVaughanSplitCrude.of_analyticInputs {x f : ℕ → ℝ} {u v : ℕ} (hI : PanTypeICharacterMeanValue x f u) (hII : PanTypeIICharacterMeanValue x f u v) (hM : PanMainTermSieveBound x f) (hfin : PanLogEventuallyLarge x) (hsplit : PanVaughanPointwiseSplit x f u v) : PanVaughanSplitCrude x f u v

Conditional coarse Vaughan assembly: three character-mean/sieve inputs and two analytic conditions (eventual log growth and the pointwise split) imply PanVaughanSplitCrude.

1. Apply the reduction theorems, including PanTypeIWeightedBound.of_characterMeanValue, to obtain bounds with constants Cᵢ, exponents Bᵢ, and thresholds x₀ᵢ.
2. For each A > 0, choose C = C₁+C₂+C₃, B = max B₁ (max B₂ B₃), and x₀ = max (max x₀₁ (max x₀₂ x₀₃)) X₀.
3. Use the weighted pointwise split, with zero weight at q = 0, and split the sum into three pieces.
4. From hfin, log(xX) ≥ 1; since Bᵢ ≤ B, enlarge each nonnegative sum from Q_B to Q_{Bᵢ}.
5. Convert the Type I/II logarithmic-saving bounds to the common polylogarithmic scale of the main-term bound and sum.

All cutoff, weight, and logarithmic-power algebra is proved here; the input propositions remain hypotheses.

theorem AnalyticNumberTheory.Sieve.PanMeanValueUniformCrude.of_vaughanSplit {x f : ℕ → ℝ} {u v : ℕ} (hV : PanVaughanSplitCrude x f u v) : PanMeanValueUniformCrude x f

The coarse pure-li split yields only the polylogarithmic PanMeanValueUniformCrude, not the classical Pan theorem.

The old theorem at this seam returned PanMeanValueUniform by definitional equality. That was the semantic bug: the old split has a polylogarithmic RHS, whereas Liu's signed theorem has inverse-log decay. The faithful assembly is defined below and requires an explicit signed-main block.

def AnalyticNumberTheory.Sieve.PanSignedMainTermBound (x f : ℕ → ℝ) (main correction : ℕ → ℕ → ℕ → ℝ) : Prop

A weighted bound for the two residual kernels which together form the signed main block. The first kernel is the signed li-minus-middle/small piece; the second carries the prime-power correction.

Equations

• AnalyticNumberTheory.Sieve.PanSignedMainTermBound x f main correction = ∀ (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 main + AnalyticNumberTheory.Sieve.panPieceMaxY X q ⌊x X⌋₊ (fun (a : ℕ) => |f a|) correction) ≤ C * x X / Real.log (x X) ^ A

def AnalyticNumberTheory.Sieve.PanVaughanPointwiseSplitSigned (_x f : ℕ → ℝ) (u v : ℕ) (main correction : ℕ → ℕ → ℕ → ℝ) : Prop

Corrected pointwise Vaughan split. Unlike PanVaughanPointwiseSplit, the residual kernels stay inside the signed main block.

Equations

• AnalyticNumberTheory.Sieve.PanVaughanPointwiseSplitSigned _x f u v main correction = ∀ (X q y : ℕ), 0 < q → AnalyticNumberTheory.Sieve.panMaxY X q y f ≤ ((AnalyticNumberTheory.Sieve.panPieceMaxY X q y f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV1 y q l u / Real.log ↑y) + AnalyticNumberTheory.Sieve.panPieceMaxY X q y f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV3 y q l u v / Real.log ↑y) + (AnalyticNumberTheory.Sieve.panPieceMaxY X q y f main + AnalyticNumberTheory.Sieve.panPieceMaxY X q y (fun (a : ℕ) => |f a|) correction)

theorem AnalyticNumberTheory.Sieve.PanMeanValueUniform.of_signedAnalyticInputs {x f : ℕ → ℝ} {u v : ℕ} {main correction : ℕ → ℕ → ℕ → ℝ} (hI : PanTypeICharacterMeanValue x f u) (hII : PanTypeIICharacterMeanValue x f u v) (hM : PanSignedMainTermBound x f main correction) (hfin : PanLogEventuallyLarge x) (hsplit : PanVaughanPointwiseSplitSigned x f u v main correction) : PanMeanValueUniform x f

Weighted finite assembly for the honest signed split. All three analytic bounds retain inverse-log decay; this theorem only aligns their cutoffs and sums the pointwise inequality.

Eventual log growth: PanLogEventuallyLarge

For x : ℕ → ℝ with Tendsto x atTop atTop, PanLogEventuallyLarge x follows from standard eventuality. Real.tendsto_log_atTop.comp htend gives Tendsto (log ∘ x) atTop atTop. Use Filter.Tendsto.eventually and eventually_ge_atTop to pull back ∀ᶠ y, 1 ≤ y to ∀ᶠ X, 1 ≤ log (x X), then eventually_atTop to express it as ∃ x₀, ∀ X ≥ x₀, ....

theorem AnalyticNumberTheory.Sieve.panLogEventuallyLarge_of_tendsto_atTop {x : ℕ → ℝ} (htend : Filter.Tendsto x Filter.atTop Filter.atTop) : PanLogEventuallyLarge x

If x : ℕ → ℝ tends to infinity, then PanLogEventuallyLarge x: eventually log(x X) ≥ 1, since log(x X) → ∞.

theorem AnalyticNumberTheory.Sieve.panLogEventuallyLarge_natCast : PanLogEventuallyLarge fun (N : ℕ) => ↑N

The real embedding x X = (X : ℝ) tends to infinity by tendsto_natCast_atTop_atTop, so it satisfies PanLogEventuallyLarge.