Actual hyperbolic decomposition of the direct Vaughan Type-II mean

The prefix cutoff in Vaughan Type II is the genuine hyperbola d * e * m ≤ y. This file does not replace it by a rowwise square estimate. Instead it first partitions the two divisor variables into the canonical dyadic rectangles, then takes the finite maximum of each resulting collected (d,t=e*m) prefix over the original prefix endpoint y. Rectangles whose lower dyadic corner lies above N are proved identically zero and removed before the direct mean is summed.

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

Canonical rectangles which can meet the hyperbola d*e*m ≤ N (m ≥ 1).

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIIActiveCanonicalRectangles N u v = {kl ∈ AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicRectangles N u v | 2 ^ kl.1 * 2 ^ kl.2 ≤ N}

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_vaughanTypeIIActiveCanonicalRectangles {N u v : ℕ} {kl : ℕ × ℕ} : kl ∈ vaughanTypeIIActiveCanonicalRectangles N u v ↔ kl ∈ vaughanCanonicalDyadicRectangles N u v ∧ 2 ^ kl.1 * 2 ^ kl.2 ≤ N

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanCanonicalCollectedPrefixMaxSquare (N u v k l q : ℕ) (χ : PrimitiveCharacter q) : ℝ

The actual maximal collected-prefix square on one canonical rectangle. The tensor collection is the exact substitution t=e*m; the maximum is still over the original hyperbolic endpoint, so no rectangular majorization has been inserted.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanCanonicalCollectedPrefixMaxSquare N u v k l q χ = (Finset.image (fun (y : ℕ) => ‖AnalyticNumberTheory.LargeSieve.vaughanTypeIICanonicalBilinearBlock (fun (x : ℕ) => 1) y N u v k l q χ‖ ^ 2) (Finset.range (N + 1))).max' ⋯

theorem AnalyticNumberTheory.LargeSieve.vaughanCanonicalCollectedPrefixMaxSquare_nonneg (N u v k l q : ℕ) (χ : PrimitiveCharacter q) : 0 ≤ vaughanCanonicalCollectedPrefixMaxSquare N u v k l q χ

noncomputable def AnalyticNumberTheory.LargeSieve.apNormalizedVaughanActualCollectedShellMean (N Q u v k l : ℕ) : ℝ

AP-normalized direct mean of one actual canonical collected-prefix shell.

Equations

• AnalyticNumberTheory.LargeSieve.apNormalizedVaughanActualCollectedShellMean N Q u v k l = ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, √(AnalyticNumberTheory.LargeSieve.vaughanCanonicalCollectedPrefixMaxSquare N u v k l q χ)

theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanActualCollectedShellMean_nonneg (N Q u v k l : ℕ) : 0 ≤ apNormalizedVaughanActualCollectedShellMean N Q u v k l

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIICanonicalBilinearBlock_norm_sq_le_rowPrefixMax (b : ℕ → ℂ) (y N u v k l q : ℕ) (χ : PrimitiveCharacter q) (hyN : y ≤ N) : ‖vaughanTypeIICanonicalBilinearBlock b y N u v k l q χ‖ ^ 2 ≤ vaughanBilinearCoeffEnergy vaughanMoebiusCoeff (vaughanCanonicalDyadicBlock N u k) * vaughanCanonicalTensorPrefixMaxEnergy b N N u v k l q χ

A genuine hyperbolic shell is controlled by rowwise tensor prefix maxima. Each row keeps its own endpoint y/d; Cauchy is applied only after the exact row-prefix identity above.

theorem AnalyticNumberTheory.LargeSieve.vaughanCanonicalCollectedPrefixMaxSquare_le_rowPrefixMax (N u v k l q : ℕ) (χ : PrimitiveCharacter q) : vaughanCanonicalCollectedPrefixMaxSquare N u v k l q χ ≤ vaughanBilinearCoeffEnergy vaughanMoebiusCoeff (vaughanCanonicalDyadicBlock N u k) * vaughanCanonicalTensorPrefixMaxEnergy (fun (x : ℕ) => 1) N N u v k l q χ

Maximizing the preceding pointwise estimate over the actual endpoint keeps one fixed ambient tensor on the right.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIICanonicalBilinearBlock_eq_zero_of_inactive {y N u v k l q : ℕ} (χ : PrimitiveCharacter q) (hyN : y ≤ N) (hinactive : N < 2 ^ k * 2 ^ l) : vaughanTypeIICanonicalBilinearBlock (fun (x : ℕ) => 1) y N u v k l q χ = 0

A canonical rectangle above the lower-corner hyperbola contributes zero to every prefix y ≤ N.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIIFullPrefix_eq_sum_active_canonical (y N u v q : ℕ) (χ : PrimitiveCharacter q) (hyN : y ≤ N) : vaughanTypeIIFullPrefix (fun (x : ℕ) => 1) y u v q χ = ∑ kl ∈ vaughanTypeIIActiveCanonicalRectangles N u v, vaughanTypeIICanonicalBilinearBlock (fun (x : ℕ) => 1) y N u v kl.1 kl.2 q χ

Exact finite reindexing: at every prefix endpoint the full Type-II form is the sum of precisely the active canonical hyperbolic shells.

theorem AnalyticNumberTheory.LargeSieve.primitivePrefixAmplitude_vaughanTypeII_le_active_collected_shells (N u v q : ℕ) (χ : PrimitiveCharacter q) : primitivePrefixAmplitude (vaughanTypeIICoeff vaughanUnitIntegerCoeff u v) N q χ ≤ ∑ kl ∈ vaughanTypeIIActiveCanonicalRectangles N u v, √(vaughanCanonicalCollectedPrefixMaxSquare N u v kl.1 kl.2 q χ)

The maximal full Type-II prefix of one primitive character is dominated by the sum of the actual canonical collected-prefix shell maxima.

theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIIMean_le_active_collected_shells (N Q u v : ℕ) : apNormalizedVaughanTypeIIMean N Q u v ≤ ∑ kl ∈ vaughanTypeIIActiveCanonicalRectangles N u v, apNormalizedVaughanActualCollectedShellMean N Q u v kl.1 kl.2

Shell coverage after summing primitive characters and moduli. This is the exact direct-mean decomposition; no rowwise N² estimate is used.

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

The active family is finite with the same canonical log² N budget.

theorem AnalyticNumberTheory.LargeSieve.vaughanDirectAPNormalizedTypeIIInput_of_actual_collected_shells (N Q u v : ℕ) (logPay : ℝ) (hshell : ∀ kl ∈ vaughanTypeIIActiveCanonicalRectangles N u v, apNormalizedVaughanActualCollectedShellMean N Q u v kl.1 kl.2 ≤ logPay * (↑N + ↑Q * ↑N / √↑(u + 1))) : VaughanDirectAPNormalizedTypeIIInput N Q u v (↑(vaughanTypeIIActiveCanonicalRectangles N u v).card) logPay

Canonical inhabitance of the existing AP-normalized Type-II input once the physical bilinear estimate has been supplied for each actual hyperbolic shell. In particular the required scale retains the term Q*N/sqrt(u+1) and never passes through a rowwise N² majorant.