Short physical length on a canonical Vaughan Type-II shell

For d in the canonical shell of level k, the collected variable t=e*m is supported on t ≤ y / 2^k. Consequently the primitive (prefix-maximal) large sieve is charged at this short length, not at the ambient length y. The last lemmas record the cancellation of the outer Möbius energy 2^k against this length and retain the resulting 2^k Q^2 charge.

def AnalyticNumberTheory.LargeSieve.vaughanCanonicalTensorLength (y k : ℕ) : ℕ

The common long-variable length on the canonical d-shell of level k.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanCanonicalTensorLength y k = y / 2 ^ k

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanCanonicalShortTensorEnergy (β c : ℕ → ℂ) (y N u v k l : ℕ) : ℝ

Tensor energy restricted to the actual common support of a canonical shell.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanCanonicalShortTensorEnergy β c y N u v k l = ∑ d ∈ AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock N u k, ∑ t ∈ Finset.Icc 1 ↑(AnalyticNumberTheory.LargeSieve.vaughanCanonicalTensorLength y k), ‖AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorCoeff β c y d (AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock N v l) t‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.vaughanTensorFiber_canonical_support (y N u v k l d : ℕ) (t : ℤ) (hd : d ∈ vaughanCanonicalDyadicBlock N u k) (ht : t ∈ Finset.Icc 1 ↑y) (hne : (vaughanTensorFiber y d (vaughanCanonicalDyadicBlock N v l) t).Nonempty) : t.toNat ≤ vaughanCanonicalTensorLength y k

Every actual t=e*m fibre on level k lies below y / 2^k. This uses the closed lower shell endpoint 2^k ≤ d; in particular k=0 gives the literal bound t ≤ y.

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorCoeff_canonical_eq_zero (b : ℕ → ℂ) (y N u v k l d : ℕ) (t : ℤ) (hd : d ∈ vaughanCanonicalDyadicBlock N u k) (ht : t ∈ Finset.Icc 1 ↑y) (hlt : vaughanCanonicalTensorLength y k < t.toNat) : vaughanBilinearTensorCoeff vaughanMangoldtCoeff b y d (vaughanCanonicalDyadicBlock N v l) t = 0

Outside the short shell length the actual tensor coefficient vanishes.

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorEnergy_canonical_eq_short (b : ℕ → ℂ) (y N u v k l : ℕ) : vaughanBilinearTensorEnergy vaughanMangoldtCoeff b y (vaughanCanonicalDyadicBlock N u k) (vaughanCanonicalDyadicBlock N v l) = vaughanCanonicalShortTensorEnergy vaughanMangoldtCoeff b y N u v k l

The old ambient t ≤ y energy is exactly the energy on the short support.

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

The complete prefix maximum in the collected variable t, row by row.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanCanonicalTensorPrefixMaxEnergy b y N u v k l q χ = ∑ d ∈ AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock N u k, AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixMaxSquare (fun (t : ℤ) => AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorCoeff AnalyticNumberTheory.LargeSieve.vaughanMangoldtCoeff b y d (AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock N v l) t) 0 (AnalyticNumberTheory.LargeSieve.vaughanCanonicalTensorLength y k) q χ

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanCanonicalTensorPrefix (b : ℕ → ℂ) (y N u v k l Q : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, vaughanBilinearCoeffEnergy vaughanMoebiusCoeff (vaughanCanonicalDyadicBlock N u k) * vaughanCanonicalTensorPrefixMaxEnergy b y N u v k l q χ ≤ vaughanBilinearCoeffEnergy vaughanMoebiusCoeff (vaughanCanonicalDyadicBlock N u k) * ↑((vaughanCanonicalTensorLength y k).log2 + 1) ^ 2 * primitiveLargeSieveConstant (vaughanCanonicalTensorLength y k) Q * vaughanCanonicalShortTensorEnergy vaughanMangoldtCoeff b y N u v k l

Prefix-maximal primitive LS charged at y / 2^k, uniformly for every row of the canonical shell. The maximum remains inside the character sum.

theorem AnalyticNumberTheory.LargeSieve.vaughanMoebiusCoeffEnergy_canonical_le_pow (N u k : ℕ) : vaughanBilinearCoeffEnergy vaughanMoebiusCoeff (vaughanCanonicalDyadicBlock N u k) ≤ ↑(2 ^ k)

Möbius energy on level k is at most 2^k.

theorem AnalyticNumberTheory.LargeSieve.pow_mul_vaughanCanonicalTensorLength_le (y k : ℕ) : 2 ^ k * vaughanCanonicalTensorLength y k ≤ y

Exact natural cancellation of shell size against short length. This also covers k=0, where 2^0=1 and the quotient is exactly y.

theorem AnalyticNumberTheory.LargeSieve.pow_mul_primitiveLargeSieveConstant_short_le (y k Q : ℕ) : ↑(2 ^ k) * primitiveLargeSieveConstant (vaughanCanonicalTensorLength y k) Q ≤ ↑y + ↑(2 ^ k) * ((2 * ↑⌈Real.log (↑Q ^ 2) / Real.log 2⌉₊ + 12) * ↑Q ^ 2)

Expanded scale audit: after paying the 2^k outer energy, the length part is at most y, while the modulus part is exactly charged by 2^k Q^2.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanCanonicalTensorPrefix_explicit (b : ℕ → ℂ) (y N u v k l Q : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, vaughanBilinearCoeffEnergy vaughanMoebiusCoeff (vaughanCanonicalDyadicBlock N u k) * vaughanCanonicalTensorPrefixMaxEnergy b y N u v k l q χ ≤ ↑((vaughanCanonicalTensorLength y k).log2 + 1) ^ 2 * (↑y + ↑(2 ^ k) * ((2 * ↑⌈Real.log (↑Q ^ 2) / Real.log 2⌉₊ + 12) * ↑Q ^ 2)) * vaughanCanonicalShortTensorEnergy vaughanMangoldtCoeff b y N u v k l

Primitive row-prefix bound with the shell energy already paid and the short large-sieve constant expanded. This is the formal cancellation 2^k * (y / 2^k) ≤ y; only the modulus term retains 2^k.

theorem AnalyticNumberTheory.LargeSieve.imprimitive_conductor_window_family_le_linear_typeII (F : (d : ℕ) → PrimitiveCharacter d → ℝ) (hF : ∀ (d : ℕ) (ψ : PrimitiveCharacter d), 0 ≤ F d ψ) (Q C : ℕ) (hC : 0 < C) : ∑ d ∈ Finset.Icc C (2 * C), imprimitiveConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, F d ψ ≤ ↑(Q / C) * conductorHarmonicFactor (Q / C) * ∑ d ∈ Finset.Icc 1 (2 * C), ↑d / ↑d.totient * ∑ ψ : PrimitiveCharacter d, F d ψ

Generic linear-harmonic transport of a nonnegative primitive family over a conductor window. This is the conductor aggregation used by the short Type-II row-prefix bound.

theorem AnalyticNumberTheory.LargeSieve.imprimitive_conductor_window_vaughanCanonicalTensorPrefix (b : ℕ → ℂ) (y N Q C u v k l : ℕ) (hC : 0 < C) : ∑ d ∈ Finset.Icc C (2 * C), imprimitiveConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, vaughanBilinearCoeffEnergy vaughanMoebiusCoeff (vaughanCanonicalDyadicBlock N u k) * vaughanCanonicalTensorPrefixMaxEnergy b y N u v k l d ψ ≤ ↑(Q / C) * conductorHarmonicFactor (Q / C) * (vaughanBilinearCoeffEnergy vaughanMoebiusCoeff (vaughanCanonicalDyadicBlock N u k) * ↑((vaughanCanonicalTensorLength y k).log2 + 1) ^ 2 * primitiveLargeSieveConstant (vaughanCanonicalTensorLength y k) (2 * C) * vaughanCanonicalShortTensorEnergy vaughanMangoldtCoeff b y N u v k l)

Conductor-window summary for the complete row-prefix maximum. Combining this with weighted_primitive_vaughanCanonicalTensorPrefix at cap 2*C and pow_mul_primitiveLargeSieveConstant_short_le yields the advertised shell charge O(y) + O(2^k C^2), times only the displayed prefix/conductor logs and the short tensor energy.

theorem AnalyticNumberTheory.LargeSieve.imprimitive_conductor_window_vaughanCanonicalTensorPrefix_explicit (b : ℕ → ℂ) (y N Q C u v k l : ℕ) (hC : 0 < C) : ∑ d ∈ Finset.Icc C (2 * C), imprimitiveConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, vaughanBilinearCoeffEnergy vaughanMoebiusCoeff (vaughanCanonicalDyadicBlock N u k) * vaughanCanonicalTensorPrefixMaxEnergy b y N u v k l d ψ ≤ ↑(Q / C) * conductorHarmonicFactor (Q / C) * (↑((vaughanCanonicalTensorLength y k).log2 + 1) ^ 2 * (↑y + ↑(2 ^ k) * ((2 * ↑⌈Real.log (↑(2 * C) ^ 2) / Real.log 2⌉₊ + 12) * ↑(2 * C) ^ 2)) * vaughanCanonicalShortTensorEnergy vaughanMangoldtCoeff b y N u v k l)

Fully expanded conductor-window summary. The complete t-prefix maximum is retained, conductor multiplicity is linear-harmonic, and the primitive charge is y + 2^k * O(C^2) rather than 2^k * (y + O(C^2)).