Exact Vaughan Type-I decomposition into actual dyadic long rows

theorem AnalyticNumberTheory.LargeSieve.norm_vaughanTypeIFirstLong_le {N y u q : ℕ} (hy : y ≤ N) (χ : PrimitiveCharacter q) : ‖vaughanTypeIFirstLong (fun (x : ℕ) => 1) y u q χ‖ ≤ ∑ d ∈ Finset.Icc 1 u, ‖↑(ArithmeticFunction.moebius d)‖ * √(primitiveCharacterPrefixMaxSquare (vaughanTypeIFirstRowCoeff (fun (x : ℕ) => 1) d) 0 (N / d) q χ)

theorem AnalyticNumberTheory.LargeSieve.norm_vaughanTypeIMiddleLong_le {N y u v q : ℕ} (hy : y ≤ N) (χ : PrimitiveCharacter q) : ‖vaughanTypeIMiddleLong (fun (x : ℕ) => 1) y u v q χ‖ ≤ ∑ de ∈ Finset.Icc 1 u ×ˢ Finset.Icc 1 v, ‖↑(ArithmeticFunction.moebius de.1)‖ * ‖↑(ArithmeticFunction.vonMangoldt de.2)‖ * √(primitiveCharacterPrefixMaxSquare (vaughanTypeIMiddlePairRowCoeff (fun (x : ℕ) => 1) de) 0 (N / (de.1 * de.2)) q χ)

The complete middle row is bounded by its fully summed (d,e) prefix amplitude. This is public because the whole-first-row Type-I decomposition must split before applying triangle only to the middle lane.

theorem AnalyticNumberTheory.LargeSieve.primitivePrefixAmplitude_vaughanTypeI_le_rows (N u v q : ℕ) (χ : PrimitiveCharacter q) : primitivePrefixAmplitude (vaughanTypeICoeff vaughanUnitIntegerCoeff u v) N q χ ≤ ∑ d ∈ Finset.Icc 1 u, ‖↑(ArithmeticFunction.moebius d)‖ * √(primitiveCharacterPrefixMaxSquare (vaughanTypeIFirstRowCoeff (fun (x : ℕ) => 1) d) 0 (N / d) q χ) + ∑ de ∈ Finset.Icc 1 u ×ˢ Finset.Icc 1 v, ‖↑(ArithmeticFunction.moebius de.1) * ↑(ArithmeticFunction.vonMangoldt de.2)‖ * √(primitiveCharacterPrefixMaxSquare (vaughanTypeIMiddlePairRowCoeff (fun (x : ℕ) => 1) de) 0 (N / (de.1 * de.2)) q χ)

For each primitive character, the maximum over all Vaughan Type-I prefixes is bounded by the sum of the complete first and middle long-row maxima.

theorem AnalyticNumberTheory.LargeSieve.sum_vaughanTypeIFirstDyadicShell {M : Type u_1} [AddCommMonoid M] (u : ℕ) (f : ℕ → M) : ∑ k ∈ Finset.range (u.log2 + 1), ∑ d ∈ vaughanTypeIFirstDyadicShell u k, f d = ∑ d ∈ Finset.Icc 1 u, f d

The first dyadic shells partition the complete positive short range exactly.

theorem AnalyticNumberTheory.LargeSieve.sum_vaughanTypeIMiddleProductDyadicShell {M : Type u_1} [AddCommMonoid M] (u v : ℕ) (f : ℕ × ℕ → M) : ∑ k ∈ Finset.range ((u * v).log2 + 1), ∑ de ∈ vaughanTypeIMiddleProductDyadicShell u v k, f de = ∑ de ∈ Finset.Icc 1 u ×ˢ Finset.Icc 1 v, f de

Product-dyadic shells partition the complete positive (d,e) rectangle exactly, with the shell selected by the actual product d*e.