Finite Vaughan decomposition and primitive-character prefix reduction

This module is a purely finite algebraic layer between Vaughan's identity and weighted_primitive_prefix_maximal. It makes no Bombieri--Vinogradov claim and introduces no analytic hypothesis.

For arbitrary cutoffs u,v, the exact all-n decomposition is

Λ n = TypeI(n;u,v) + TypeII(n;u,v) + Small(n;v).

Here Type I is vaughanFirst - vaughanMiddle, Type II is vaughanThird, and the last term retains the complete exceptional range n ≤ v. The final theorem consumes this equality inside every primitive-character prefix and reduces its weighted square maximum to three explicit coefficient energies. No cutoff is selected or hidden.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeI (n u v : ℕ) : ℝ

The two Type-I pieces of Vaughan's identity, kept together with their correct relative sign.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeI n u v = AnalyticNumberTheory.Sieve.vaughanFirst n u - AnalyticNumberTheory.Sieve.vaughanMiddle n u v

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeII (n u v : ℕ) : ℝ

The genuinely bilinear (large-large) piece of Vaughan's identity.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeII n u v = AnalyticNumberTheory.Sieve.vaughanThird n u v

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanSmall (n v : ℕ) : ℝ

The complete small-factor exception. Keeping this term makes the identity valid without a premise such as v < n.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanSmall n v = if n ≤ v then ArithmeticFunction.vonMangoldt n else 0

theorem AnalyticNumberTheory.LargeSieve.vaughanIdentity_typeI_typeII_small (n u v : ℕ) : ArithmeticFunction.vonMangoldt n = vaughanTypeI n u v + vaughanTypeII n u v + vaughanSmall n v

The finite Vaughan identity, valid for every natural n and every pair of cutoffs. This internalizes Mathlib's μ * log = Λ API through the exact finite identity in AnalyticNumberTheory.Sieve.VaughanIdentity.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanLambdaCoeff (b : ℤ → ℂ) (n : ℤ) : ℂ

A scalar coefficient sequence multiplied by the von Mangoldt function.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanLambdaCoeff b n = b n * ↑(ArithmeticFunction.vonMangoldt n.toNat)

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeICoeff (b : ℤ → ℂ) (u v : ℕ) (n : ℤ) : ℂ

The Type-I coefficient sequence at the literal cutoffs u,v.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeICoeff b u v n = b n * ↑(AnalyticNumberTheory.LargeSieve.vaughanTypeI n.toNat u v)

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIICoeff (b : ℤ → ℂ) (u v : ℕ) (n : ℤ) : ℂ

The Type-II coefficient sequence at the literal cutoffs u,v.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIICoeff b u v n = b n * ↑(AnalyticNumberTheory.LargeSieve.vaughanTypeII n.toNat u v)

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanSmallCoeff (b : ℤ → ℂ) (v : ℕ) (n : ℤ) : ℂ

The small-factor coefficient sequence at the literal cutoff v.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanSmallCoeff b v n = b n * ↑(AnalyticNumberTheory.LargeSieve.vaughanSmall n.toNat v)

theorem AnalyticNumberTheory.LargeSieve.vaughanLambdaCoeff_eq (b : ℤ → ℂ) (u v : ℕ) (n : ℤ) : vaughanLambdaCoeff b n = vaughanTypeICoeff b u v n + vaughanTypeIICoeff b u v n + vaughanSmallCoeff b v n

Pointwise complex-linear form of the exact finite Vaughan identity.

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefix_vaughan_eq (b : ℤ → ℂ) (y q u v : ℕ) (χ : PrimitiveCharacter q) : ∑ n ∈ Finset.Icc 1 ↑y, vaughanLambdaCoeff b n * ↑χ ↑n = ∑ n ∈ Finset.Icc 1 ↑y, vaughanTypeICoeff b u v n * ↑χ ↑n + ∑ n ∈ Finset.Icc 1 ↑y, vaughanTypeIICoeff b u v n * ↑χ ↑n + ∑ n ∈ Finset.Icc 1 ↑y, vaughanSmallCoeff b v n * ↑χ ↑n

Exact consumption by one primitive character and one finite prefix. This is the algebraic interface used before taking character/modulus sums or prefix maxima; no estimate has yet been applied.

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixMaxSquare_le_three (b bI bII bSmall : ℤ → ℂ) (N q : ℕ) (χ : PrimitiveCharacter q) (hdecomp : ∀ n ∈ Finset.Icc 1 ↑N, b n = bI n + bII n + bSmall n) : primitiveCharacterPrefixMaxSquare b 0 N q χ ≤ 3 * (primitiveCharacterPrefixMaxSquare bI 0 N q χ + primitiveCharacterPrefixMaxSquare bII 0 N q χ + primitiveCharacterPrefixMaxSquare bSmall 0 N q χ)

A finite pointwise three-piece decomposition on [1,N] is consumed by the primitive-character prefix maximum, uniformly in the character and modulus.

theorem AnalyticNumberTheory.LargeSieve.weighted_vaughan_prefix_reduction (b : ℤ → ℂ) (N Q u v : ℕ) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare (vaughanLambdaCoeff b) 0 N q χ ≤ 3 * (∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare (vaughanTypeICoeff b u v) 0 N q χ + ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare (vaughanTypeIICoeff b u v) 0 N q χ + ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare (vaughanSmallCoeff b v) 0 N q χ)

Exact algebraic reduction of every primitive-character prefix maximum of b Λ to Type I, Type II, and the retained small range. All four finite parameters N,Q,u,v remain explicit.

theorem AnalyticNumberTheory.LargeSieve.weighted_vaughan_prefix_large_sieve_ledger (b : ℤ → ℂ) (N Q u v : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare (vaughanLambdaCoeff b) 0 N q χ ≤ 3 * ↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N Q * (∑ n ∈ Finset.Icc 1 ↑N, ‖vaughanTypeICoeff b u v n‖ ^ 2 + ∑ n ∈ Finset.Icc 1 ↑N, ‖vaughanTypeIICoeff b u v n‖ ^ 2 + ∑ n ∈ Finset.Icc 1 ↑N, ‖vaughanSmallCoeff b v n‖ ^ 2)

The concrete algebraic consumer of the proved prefix-maximal primitive large sieve. Closing Standard BV from here still requires genuine Type-I and Type-II energy estimates; this theorem does not disguise those estimates as a Prop premise or a BV conclusion.