Vaughan Type I in the long variable

The first and middle prefixes are rearranged before any square is taken. Their literal divisor sums become finite sums over the short variables d and (d,e), while the remaining character sum is in the long variable m.

The final ledger deliberately freezes only the resulting coefficient moment. It does not assume a Type-I character estimate, and it does not reuse the pointwise divisor-cardinality energy from VaughanTypeIEnergy.

def AnalyticNumberTheory.LargeSieve.vaughanTypeIShortRange (y u : ℕ) : Finset ℕ

The positive short-variable range occurring in a prefix of length y.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIShortRange y u = Finset.Icc 1 (min y u)

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_vaughanTypeIShortRange {y u d : ℕ} : d ∈ vaughanTypeIShortRange y u ↔ 0 < d ∧ d ≤ y ∧ d ≤ u

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstAt (n u : ℕ) : ℂ

Complex form of the first Vaughan divisor factor.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstAt n u = ∑ d ∈ n.divisors with d ≤ u, ↑(ArithmeticFunction.moebius d) * ↑(Real.log ↑(n / d))

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleAt (n u v : ℕ) : ℂ

Complex form of the middle Vaughan divisor factor.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleAt n u v = ∑ d ∈ n.divisors with d ≤ u, ∑ e ∈ (n / d).divisors with e ≤ v, ↑(ArithmeticFunction.moebius d) * ↑(ArithmeticFunction.vonMangoldt e)

@[simp]

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstAt_eq_cast (n u : ℕ) : vaughanTypeIFirstAt n u = ↑(Sieve.vaughanFirst n u)

@[simp]

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleAt_eq_cast (n u v : ℕ) : vaughanTypeIMiddleAt n u v = ↑(Sieve.vaughanMiddle n u v)

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstAt_eq_bounded {n y u : ℕ} (hn : 0 < n) (hny : n ≤ y) : vaughanTypeIFirstAt n u = ∑ d ∈ vaughanTypeIShortRange y u, if d ∣ n then ↑(ArithmeticFunction.moebius d) * ↑(Real.log ↑(n / d)) else 0

On 0 < n ≤ y, the first divisor factor has a fixed short support.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleAt_eq_bounded {n y u v : ℕ} (hn : 0 < n) (hny : n ≤ y) : vaughanTypeIMiddleAt n u v = ∑ d ∈ vaughanTypeIShortRange y u, ∑ e ∈ vaughanTypeIShortRange y v, if d * e ∣ n then ↑(ArithmeticFunction.moebius d) * ↑(ArithmeticFunction.vonMangoldt e) else 0

On 0 < n ≤ y, the middle factor is a fixed short (d,e) rectangle. The condition e ∣ n/d has become the single product condition d*e ∣ n.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstPrefix (b : ℕ → ℂ) (y u q : ℕ) (χ : PrimitiveCharacter q) : ℂ

The first Type-I prefix before rearrangement.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstPrefix b y u q χ = ∑ n ∈ Finset.Icc 1 y, b n * ↑χ ↑n * AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstAt n u

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstLong (b : ℕ → ℂ) (y u q : ℕ) (χ : PrimitiveCharacter q) : ℂ

The first prefix after n=d*m; the character sum is long in m.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstLong b y u q χ = ∑ d ∈ AnalyticNumberTheory.LargeSieve.vaughanTypeIShortRange y u, ↑(ArithmeticFunction.moebius d) * ↑χ ↑d * ∑ m ∈ Finset.Icc 1 (y / d), b (d * m) * ↑(Real.log ↑m) * ↑χ ↑m

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstPrefix_eq_long (b : ℕ → ℂ) (y u q : ℕ) (χ : PrimitiveCharacter q) : vaughanTypeIFirstPrefix b y u q χ = vaughanTypeIFirstLong b y u q χ

Exact first-prefix rearrangement into a short d coefficient and a long m character sum.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddlePrefix (b : ℕ → ℂ) (y u v q : ℕ) (χ : PrimitiveCharacter q) : ℂ

The middle Type-I prefix before rearrangement.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddlePrefix b y u v q χ = ∑ n ∈ Finset.Icc 1 y, b n * ↑χ ↑n * AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleAt n u v

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleLong (b : ℕ → ℂ) (y u v q : ℕ) (χ : PrimitiveCharacter q) : ℂ

The middle prefix after n=d*e*m; (d,e) are short and m is long.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleLong b y u v q χ = ∑ d ∈ AnalyticNumberTheory.LargeSieve.vaughanTypeIShortRange y u, ∑ e ∈ AnalyticNumberTheory.LargeSieve.vaughanTypeIShortRange y v, ↑(ArithmeticFunction.moebius d) * ↑(ArithmeticFunction.vonMangoldt e) * ↑χ ↑d * ↑χ ↑e * ∑ m ∈ Finset.Icc 1 (y / (d * e)), b (d * e * m) * ↑χ ↑m

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddlePrefix_eq_long (b : ℕ → ℂ) (y u v q : ℕ) (χ : PrimitiveCharacter q) : vaughanTypeIMiddlePrefix b y u v q χ = vaughanTypeIMiddleLong b y u v q χ

Exact middle-prefix rearrangement into short (d,e) coefficients and a long m character sum.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeILongPrefix (b : ℕ → ℂ) (y u v q : ℕ) (χ : PrimitiveCharacter q) : ℂ

The signed Type-I prefix, exactly equal to first minus middle.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeILongPrefix b y u v q χ = AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstLong b y u q χ - AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleLong b y u v q χ

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIPrefix_eq_long (b : ℕ → ℂ) (y u v q : ℕ) (χ : PrimitiveCharacter q) : ∑ n ∈ Finset.Icc 1 y, b n * ↑χ ↑n * ↑(vaughanTypeI n u v) = vaughanTypeILongPrefix b y u v q χ

Exact replacement of the packaged Type-I prefix by its long-variable form.

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

Character-free Type-I coefficient produced by the exact long-variable rearrangement. This is the smallest coefficient moment needed by the primitive prefix large sieve.

Equations

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

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeILongCoeffMoment (b : ℤ → ℂ) (N u v : ℕ) : ℝ

The literal finite coefficient moment; no pointwise divisor-cardinality majorant has been inserted.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeILongCoeffMoment b N u v = ∑ n ∈ Finset.Icc 1 ↑N, ‖AnalyticNumberTheory.LargeSieve.vaughanTypeILongCoeff b u v n‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeILongPrefixMaxSquare (b : ℤ → ℂ) (N u v q : ℕ) (χ : PrimitiveCharacter q) : ℝ

Prefix maximum written on the rearranged long-variable forms themselves.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeILongPrefixMaxSquare b N u v q χ = (Finset.image (fun (y : ℕ) => ‖AnalyticNumberTheory.LargeSieve.vaughanTypeILongPrefix (fun (n : ℕ) => b ↑n) y u v q χ‖ ^ 2) (Finset.range (N + 1))).max' ⋯

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixSquare_typeI_eq_long (b : ℤ → ℂ) (y u v q : ℕ) (χ : PrimitiveCharacter q) : primitiveCharacterPrefixSquare (vaughanTypeILongCoeff b u v) 0 y q χ = ‖vaughanTypeILongPrefix (fun (n : ℕ) => b ↑n) y u v q χ‖ ^ 2

Every prefix of the collected coefficient sequence is literally the previously rearranged short-times-long expression.

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixMaxSquare_typeI_eq_long (b : ℤ → ℂ) (N u v q : ℕ) (χ : PrimitiveCharacter q) : primitiveCharacterPrefixMaxSquare (vaughanTypeILongCoeff b u v) 0 N q χ = vaughanTypeILongPrefixMaxSquare b N u v q χ

The generic prefix maximum and the maximum of the exact long-variable forms are equal, not merely comparable.

def AnalyticNumberTheory.LargeSieve.VaughanTypeILongCoeffMomentBound (b : ℤ → ℂ) (N u v : ℕ) (C : ℝ) (κ : ℕ) : Prop

Minimal BV-scale scalar hypothesis. It is a coefficient moment only, not a Type-I character-sum conclusion. All of u,v,N remain explicit.

Equations

• AnalyticNumberTheory.LargeSieve.VaughanTypeILongCoeffMomentBound b N u v C κ = (AnalyticNumberTheory.LargeSieve.vaughanTypeILongCoeffMoment b N u v ≤ C * ↑N * Real.log ↑(N + 1) ^ κ)

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanTypeILong (b : ℤ → ℂ) (N Q u v : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare (vaughanTypeILongCoeff b u v) 0 N q χ ≤ ↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N Q * vaughanTypeILongCoeffMoment b N u v

Primitive large sieve applied only after the exact long-variable rearrangement.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanTypeILong_rearranged (b : ℤ → ℂ) (N Q u v : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, vaughanTypeILongPrefixMaxSquare b N u v q χ ≤ ↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N Q * vaughanTypeILongCoeffMoment b N u v

Primitive large sieve in the publication-facing, genuinely rearranged form: its left side is a maximum of short-variable coefficients multiplying long-variable character sums.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanTypeILong_of_moment (b : ℤ → ℂ) (N Q u v : ℕ) (C : ℝ) (κ : ℕ) (hQ : 0 < Q) (hMoment : VaughanTypeILongCoeffMomentBound b N u v C κ) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare (vaughanTypeILongCoeff b u v) 0 N q χ ≤ ↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N Q * (C * ↑N * Real.log ↑(N + 1) ^ κ)

Explicit BV-compatible N * log^κ coefficient scale. The only premise is the minimal coefficient moment above.

theorem AnalyticNumberTheory.LargeSieve.weighted_vaughan_prefix_large_sieve_long_typeI_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 * (vaughanTypeILongCoeffMoment b N u v + ∑ n ∈ Finset.Icc 1 ↑N, ‖vaughanTypeIICoeff b u v n‖ ^ 2 + ∑ n ∈ Finset.Icc 1 ↑N, ‖vaughanSmallCoeff b v n‖ ^ 2)

Weighted Vaughan ledger with the old pointwise Type-I energy removed. Type I is charged by the exact long-variable coefficient moment; Type II and the small range retain their existing coefficient moments.

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

The integrated weighted Vaughan ledger after inserting precisely the BV-scale coefficient-moment premise. No Type-I character-sum estimate is assumed: the primitive large sieve was proved above from the coefficient moment.