Canonical dyadic ledger for the full Vaughan Type-II prefix

The canonical blocks are the fibres of the floor binary logarithm on the literal truncated ranges u < d ≤ N and v < e ≤ N. Thus the first block also handles d = 1 (or e = 1), while a cutoff lying inside a dyadic shell only truncates that one shell. Every retained integer belongs to exactly one block, including the zero/empty boundary cases.

def AnalyticNumberTheory.LargeSieve.vaughanTypeIIRange (N u : ℕ) : Finset ℕ

The literal positive truncated interval u < d ≤ N.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIIRange N u = {d ∈ Finset.Icc 1 N | u < d}

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_vaughanTypeIIRange {N u d : ℕ} : d ∈ vaughanTypeIIRange N u ↔ 0 < d ∧ d ≤ N ∧ u < d

def AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBases (N u : ℕ) : Finset ℕ

Canonical dyadic bases, represented by binary-logarithm levels.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBases N u = Finset.image (Nat.log 2) (AnalyticNumberTheory.LargeSieve.vaughanTypeIIRange N u)

def AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock (N u k : ℕ) : Finset ℕ

The canonical (possibly cutoff-truncated) binary shell at level k.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock N u k = {d ∈ AnalyticNumberTheory.LargeSieve.vaughanTypeIIRange N u | Nat.log 2 d = k}

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_vaughanCanonicalDyadicBlock {N u k d : ℕ} : d ∈ vaughanCanonicalDyadicBlock N u k ↔ 0 < d ∧ d ≤ N ∧ u < d ∧ Nat.log 2 d = k

theorem AnalyticNumberTheory.LargeSieve.mem_vaughanCanonicalDyadicBases_iff {N u k : ℕ} : k ∈ vaughanCanonicalDyadicBases N u ↔ ∃ d ∈ vaughanCanonicalDyadicBlock N u k, True

A level is selected exactly when its block is nonempty.

theorem AnalyticNumberTheory.LargeSieve.mem_own_vaughanCanonicalDyadicBlock {N u d : ℕ} (hd : d ∈ vaughanTypeIIRange N u) : Nat.log 2 d ∈ vaughanCanonicalDyadicBases N u ∧ d ∈ vaughanCanonicalDyadicBlock N u (Nat.log 2 d)

Every retained integer lies in the block indexed by its own level.

theorem AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock_level_unique {N u d k₁ k₂ : ℕ} (h₁ : d ∈ vaughanCanonicalDyadicBlock N u k₁) (h₂ : d ∈ vaughanCanonicalDyadicBlock N u k₂) : k₁ = k₂

Membership determines the dyadic level uniquely.

theorem AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock_pow_bounds {N u k d : ℕ} (hd : d ∈ vaughanCanonicalDyadicBlock N u k) : 2 ^ k ≤ d ∧ d < 2 ^ (k + 1)

A canonical level really is the half-open binary shell [2^k,2^(k+1)), after the literal cutoff truncations.

theorem AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock_disjoint {N u k₁ k₂ : ℕ} (h : k₁ ≠ k₂) : Disjoint (vaughanCanonicalDyadicBlock N u k₁) (vaughanCanonicalDyadicBlock N u k₂)

Distinct canonical blocks are disjoint.

theorem AnalyticNumberTheory.LargeSieve.biUnion_vaughanCanonicalDyadicBlock (N u : ℕ) : (vaughanCanonicalDyadicBases N u).biUnion (vaughanCanonicalDyadicBlock N u) = vaughanTypeIIRange N u

The canonical blocks cover the retained interval exactly.

theorem AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBases_eq_empty_of_le {N u : ℕ} (hNu : N ≤ u) : vaughanCanonicalDyadicBases N u = ∅

If the strict cutoff reaches the upper endpoint, every canonical block base disappears. This includes the N = 0 boundary.

theorem AnalyticNumberTheory.LargeSieve.sum_vaughanCanonicalDyadicBlock {M : Type u_1} [AddCommMonoid M] (N u : ℕ) (f : ℕ → M) : ∑ k ∈ vaughanCanonicalDyadicBases N u, ∑ d ∈ vaughanCanonicalDyadicBlock N u k, f d = ∑ d ∈ vaughanTypeIIRange N u, f d

Exact one-dimensional fibrewise sum ledger.

theorem AnalyticNumberTheory.LargeSieve.card_vaughanCanonicalDyadicBases_le (N u : ℕ) : (vaughanCanonicalDyadicBases N u).card ≤ Nat.log 2 N + 1

The number of nonempty canonical shells has the exact natural upper bound log₂ N + 1, uniformly in the cutoff (and also when the range is empty).

def AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicRectangles (N u v : ℕ) : Finset (ℕ × ℕ)

Canonical rectangle indices for the two cutoff ranges.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicRectangles N u v = AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBases N u ×ˢ AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBases N v

def AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicRectangleBlock (N u v : ℕ) (kl : ℕ × ℕ) : Finset (ℕ × ℕ)

The integer pairs belonging to one canonical dyadic rectangle.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicRectangleBlock N u v kl = AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock N u kl.1 ×ˢ AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock N v kl.2

theorem AnalyticNumberTheory.LargeSieve.mem_own_vaughanCanonicalDyadicRectangleBlock {N u v d e : ℕ} (hd : d ∈ vaughanTypeIIRange N u) (he : e ∈ vaughanTypeIIRange N v) : (Nat.log 2 d, Nat.log 2 e) ∈ vaughanCanonicalDyadicRectangles N u v ∧ (d, e) ∈ vaughanCanonicalDyadicRectangleBlock N u v (Nat.log 2 d, Nat.log 2 e)

A retained pair belongs to the rectangle indexed by its two logarithms.

theorem AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicRectangleBlock_level_unique {N u v d e : ℕ} {kl₁ kl₂ : ℕ × ℕ} (h₁ : (d, e) ∈ vaughanCanonicalDyadicRectangleBlock N u v kl₁) (h₂ : (d, e) ∈ vaughanCanonicalDyadicRectangleBlock N u v kl₂) : kl₁ = kl₂

Membership of a pair determines its canonical rectangle uniquely.

theorem AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicRectangleBlock_disjoint {N u v : ℕ} {kl₁ kl₂ : ℕ × ℕ} (h : kl₁ ≠ kl₂) : Disjoint (vaughanCanonicalDyadicRectangleBlock N u v kl₁) (vaughanCanonicalDyadicRectangleBlock N u v kl₂)

Distinct canonical rectangles are pairwise disjoint.

theorem AnalyticNumberTheory.LargeSieve.biUnion_vaughanCanonicalDyadicRectangleBlock (N u v : ℕ) : (vaughanCanonicalDyadicRectangles N u v).biUnion (vaughanCanonicalDyadicRectangleBlock N u v) = vaughanTypeIIRange N u ×ˢ vaughanTypeIIRange N v

The rectangle family is an exact disjoint cover of all pairs satisfying u < d ≤ N and v < e ≤ N.

theorem AnalyticNumberTheory.LargeSieve.card_vaughanCanonicalDyadicRectangles_le (N u v : ℕ) : (vaughanCanonicalDyadicRectangles N u v).card ≤ (Nat.log 2 N + 1) ^ 2

Precise O(log² N) natural-number rectangle count.

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

The actual nested Vaughan Type-II factor at n, with complex weights.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIIFullAt n u v = ∑ d ∈ n.divisors with u < d, ∑ e ∈ (n / d).divisors with v < e, AnalyticNumberTheory.LargeSieve.vaughanMoebiusCoeff d * AnalyticNumberTheory.LargeSieve.vaughanMangoldtCoeff e

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIIFullAt_eq_vaughanThird (n u v : ℕ) : vaughanTypeIIFullAt n u v = ↑(Sieve.vaughanThird n u v)

The complex nested factor is literally the cast of Vaughan's real vaughanThird (the public Type-II factor).

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIIFullAt_eq_bounded_rectangular {n N u v : ℕ} (hn : 0 < n) (hnN : n ≤ N) : vaughanTypeIIFullAt n u v = ∑ d ∈ vaughanTypeIIRange N u, ∑ e ∈ vaughanTypeIIRange N v, if d * e ∣ n then vaughanMoebiusCoeff d * vaughanMangoldtCoeff e else 0

On a positive prefix n ≤ N, the nested divisor factor is exactly the bounded rectangular divisibility sum.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIIFullAt_eq_sum_canonical_blocks {n N u v : ℕ} (hn : 0 < n) (hnN : n ≤ N) : vaughanTypeIIFullAt n u v = ∑ k ∈ vaughanCanonicalDyadicBases N u, ∑ l ∈ vaughanCanonicalDyadicBases N v, ∑ d ∈ vaughanCanonicalDyadicBlock N u k, ∑ e ∈ vaughanCanonicalDyadicBlock N v l, if d * e ∣ n then vaughanMoebiusCoeff d * vaughanMangoldtCoeff e else 0

Pointwise two-dimensional canonical partition of the full Type-II factor.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIICanonicalBlockPrefix (b : ℕ → ℂ) (y N u v k l q : ℕ) (χ : PrimitiveCharacter q) : ℂ

One canonical rectangle before the n=d*e*m substitution.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIICanonicalBlockPrefix b y N u v k l q χ = ∑ n ∈ Finset.Icc 1 y, b n * ↑χ ↑n * ∑ d ∈ AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock N u k, ∑ e ∈ AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock N v l, if d * e ∣ n then AnalyticNumberTheory.LargeSieve.vaughanMoebiusCoeff d * AnalyticNumberTheory.LargeSieve.vaughanMangoldtCoeff e else 0

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIICanonicalBilinearBlock (b : ℕ → ℂ) (y N u v k l q : ℕ) (χ : PrimitiveCharacter q) : ℂ

The separated bilinear form attached to one canonical rectangle.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIICanonicalBilinearBlock b y N u v k l q χ = ∑ d ∈ AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock N u k, AnalyticNumberTheory.LargeSieve.vaughanMoebiusCoeff d * ↑χ ↑d * ∑ e ∈ AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock N v l, AnalyticNumberTheory.LargeSieve.vaughanMangoldtCoeff e * ↑χ ↑e * ∑ m ∈ Finset.Icc 1 (y / (d * e)), b (d * e * m) * ↑χ ↑m

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIICanonicalBlockPrefix_eq_bilinear (b : ℕ → ℂ) (y N u v k l q : ℕ) (χ : PrimitiveCharacter q) : vaughanTypeIICanonicalBlockPrefix b y N u v k l q χ = vaughanTypeIICanonicalBilinearBlock b y N u v k l q χ

Exact finite substitution and character separation on a canonical block. Positivity is obtained from block membership, so no global assumption on N,u,v,k,l is needed.

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

The complete Vaughan Type-II prefix (before any analytic inequality).

Equations

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

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIIFullPrefix_eq_sum_canonical_bilinear (b : ℕ → ℂ) (y N u v q : ℕ) (χ : PrimitiveCharacter q) (hyN : y ≤ N) : vaughanTypeIIFullPrefix b y u v q χ = ∑ k ∈ vaughanCanonicalDyadicBases N u, ∑ l ∈ vaughanCanonicalDyadicBases N v, vaughanTypeIICanonicalBilinearBlock b y N u v k l q χ

Full Type-II ledger: the literal prefix is exactly the finite sum of the canonical dyadic rectangles, each already in separated bilinear form. The hypothesis y ≤ N is precisely what turns divisors of prefix indices into the bounds d,e ≤ N; all strict-cutoff and empty-range boundary cases remain literal in the definitions.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIIFullLedger (b : ℕ → ℂ) (y N u v q : ℕ) (χ : PrimitiveCharacter q) (hyN : y ≤ N) : vaughanTypeIIFullPrefix b y u v q χ = ∑ kl ∈ vaughanCanonicalDyadicRectangles N u v, vaughanTypeIICanonicalBilinearBlock b y N u v kl.1 kl.2 q χ ∧ (vaughanCanonicalDyadicRectangles N u v).card ≤ (Nat.log 2 N + 1) ^ 2

A compact package for handing the full Type-II lane to a bilinear large sieve: exact equality plus the natural rectangle-count budget.