Canonical Type-II shell scale and the bilinear fourth-moment frontier

This module makes two logically separate points precise.

• On a d-shell of cardinality/size D and collected length M, the actual short tensor energy has scale D*M (up to the divisor-square logarithms). The e-shell contributes no further polynomial factor: its divisors are already absorbed by the divisor-square moment.
• Substitution into the existing rowwise short-length large sieve still leaves an extra factor equal to that row mass. We therefore freeze a generic bilinear tensor fourth-moment inequality, not a Bombieri--Vinogradov conclusion, and prove that it is exactly sufficient for a per-rectangle bound with scale (D+Q^2)(M+Q^2).

def AnalyticNumberTheory.LargeSieve.bilinearMultiplicativeScale (D M Q : ℕ) : ℝ

Polynomial scale of a genuine two-variable multiplicative large sieve.

Equations

• AnalyticNumberTheory.LargeSieve.bilinearMultiplicativeScale D M Q = ↑D * ↑M + ↑Q ^ 2 * (↑D + ↑M) + ↑Q ^ 4

theorem AnalyticNumberTheory.LargeSieve.bilinearMultiplicativeScale_eq (D M Q : ℕ) : bilinearMultiplicativeScale D M Q = (↑D + ↑Q ^ 2) * (↑M + ↑Q ^ 2)

The scale is the product of the two one-variable large-sieve scales.

theorem AnalyticNumberTheory.LargeSieve.bilinearMultiplicativeScale_nonneg (D M Q : ℕ) : 0 ≤ bilinearMultiplicativeScale D M Q

noncomputable def AnalyticNumberTheory.LargeSieve.bilinearTensorCharacterForm (A : ℕ → ℤ → ℂ) (DS : Finset ℕ) (M q : ℕ) (χ : PrimitiveCharacter q) : ℂ

A generic character form with genuinely two-dimensional coefficients. The row coefficients may depend on d; no rank-one/separability assumption is hidden in the interface.

Equations

• AnalyticNumberTheory.LargeSieve.bilinearTensorCharacterForm A DS M q χ = ∑ d ∈ DS, ∑ t ∈ Finset.Icc 1 ↑M, A d t * ↑χ ↑d * ↑χ ↑t

noncomputable def AnalyticNumberTheory.LargeSieve.bilinearTensorCoeffEnergy (A : ℕ → ℤ → ℂ) (DS : Finset ℕ) (M : ℕ) : ℝ

Frobenius coefficient energy of the generic bilinear tensor.

Equations

• AnalyticNumberTheory.LargeSieve.bilinearTensorCoeffEnergy A DS M = ∑ d ∈ DS, ∑ t ∈ Finset.Icc 1 ↑M, ‖A d t‖ ^ 2

def AnalyticNumberTheory.LargeSieve.BilinearTensorFourthMomentBound (K : ℝ) : Prop

Minimal analytic frontier: a weighted primitive-character fourth-moment bound for an arbitrary bilinear tensor. It is deliberately generic and per-rectangle; it mentions neither Vaughan coefficients nor a final BV error. For rank-one A d t = a d * b t, its left side is the mixed fourth moment sum |sum a_d χ(d)|^2 |sum b_t χ(t)|^2.

Equations

• AnalyticNumberTheory.LargeSieve.BilinearTensorFourthMomentBound K = ∀ (A : ℕ → ℤ → ℂ) (DS : Finset ℕ) (D M Q : ℕ), DS.card ≤ D → (∀ d ∈ DS, d < 2 * D) → ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.bilinearTensorCharacterForm A DS M q χ‖ ^ 2 ≤ K * AnalyticNumberTheory.LargeSieve.bilinearMultiplicativeScale D M Q * AnalyticNumberTheory.LargeSieve.bilinearTensorCoeffEnergy A DS M

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanCanonicalBilinearTensor (b : ℕ → ℂ) (y N v l : ℕ) : ℕ → ℤ → ℂ

The canonical short tensor, including the outer Möbius coefficient.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanCanonicalBilinearTensor b y N v l d t = AnalyticNumberTheory.LargeSieve.vaughanMoebiusCoeff d * AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorCoeff AnalyticNumberTheory.LargeSieve.vaughanMangoldtCoeff b y d (AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock N v l) t

theorem AnalyticNumberTheory.LargeSieve.vaughanCanonicalBilinearBlock_eq_shortTensorForm (b : ℕ → ℂ) (y N u v k l q : ℕ) (χ : PrimitiveCharacter q) : vaughanTypeIICanonicalBilinearBlock b y N u v k l q χ = bilinearTensorCharacterForm (vaughanCanonicalBilinearTensor b y N v l) (vaughanCanonicalDyadicBlock N u k) (vaughanCanonicalTensorLength y k) q χ

theorem AnalyticNumberTheory.LargeSieve.vaughanCanonicalBilinearTensor_energy_le (b : ℕ → ℂ) (y N u v k l : ℕ) : bilinearTensorCoeffEnergy (vaughanCanonicalBilinearTensor b y N v l) (vaughanCanonicalDyadicBlock N u k) (vaughanCanonicalTensorLength y k) ≤ vaughanCanonicalShortTensorEnergy vaughanMangoldtCoeff b y N u v k l

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanCanonicalBilinear_of_fourthMoment (K : ℝ) (hK : 0 ≤ K) (hFourth : BilinearTensorFourthMomentBound K) (b : ℕ → ℂ) (y N u v k l Q : ℕ) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖vaughanTypeIICanonicalBilinearBlock b y N u v k l q χ‖ ^ 2 ≤ K * bilinearMultiplicativeScale (2 ^ k) (vaughanCanonicalTensorLength y k) Q * vaughanCanonicalShortTensorEnergy vaughanMangoldtCoeff b y N u v k l

The frozen generic fourth moment is sufficient for the actual canonical Vaughan rectangle. This is only a per-shell second-moment consumer, not a BV conclusion.

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorCoeff_eq_zero_of_eShell_above_length (b : ℕ → ℂ) (y N v k l d : ℕ) (t : ℤ) (ht : t ∈ Finset.Icc 1 ↑(vaughanCanonicalTensorLength y k)) (hEM : vaughanCanonicalTensorLength y k < 2 ^ l) : vaughanBilinearTensorCoeff vaughanMangoldtCoeff b y d (vaughanCanonicalDyadicBlock N v l) t = 0

An e-shell whose lower endpoint exceeds the collected length is literally inactive: no product e*m=t with m≥1 can occur.

theorem AnalyticNumberTheory.LargeSieve.vaughanCanonicalShortTensorEnergy_eq_zero_of_eShell_above_length (b : ℕ → ℂ) (y N u v k l : ℕ) (hEM : vaughanCanonicalTensorLength y k < 2 ^ l) : vaughanCanonicalShortTensorEnergy vaughanMangoldtCoeff b y N u v k l = 0

Precise e-shell dichotomy: above M the short tensor energy is zero; on active shells the polynomial bound below is independent of E=2^l.

theorem AnalyticNumberTheory.LargeSieve.vaughanQuotientMass_canonical_le_pow_mul_length (y N u k : ℕ) : vaughanQuotientMass y (vaughanCanonicalDyadicBlock N u k) ≤ ↑(2 ^ k) * ↑(vaughanCanonicalTensorLength y k)

Exact d-shell quotient-mass bound before using D*M ≤ y.

theorem AnalyticNumberTheory.LargeSieve.vaughanCanonicalShortTensorEnergy_le_shellScale (b : ℕ → ℂ) (y N u v k l : ℕ) (B C : ℝ) (hB : ∀ n ≤ y, ‖b n‖ ≤ B) (hMoment : DivisorSquareMomentBound C) (hC : 0 ≤ C) : vaughanCanonicalShortTensorEnergy vaughanMangoldtCoeff b y N u v k l ≤ C * B ^ 2 * (↑(2 ^ k) * ↑(vaughanCanonicalTensorLength y k)) * Real.log ↑(y + 1) ^ 5

True canonical short-tensor scale. l (and hence the e-shell size) is present but contributes no polynomial factor. The divisor-square moment has already paid for all collisions e*m=t.

def AnalyticNumberTheory.LargeSieve.rowwiseShortTypeIIScale (D M Q energy : ℝ) : ℝ

Abstract scale of the currently proved rowwise short-length route.

Equations

• AnalyticNumberTheory.LargeSieve.rowwiseShortTypeIIScale D M Q energy = D * (M + Q ^ 2) * energy

theorem AnalyticNumberTheory.LargeSieve.rowwiseShortTypeIIScale_after_shellEnergy {D M Q energy C L : ℝ} (hD : 0 ≤ D) (hM : 0 ≤ M) (henergy : energy ≤ C * (D * M) * L) : rowwiseShortTypeIIScale D M Q energy ≤ C * (D * M) * (D * (M + Q ^ 2)) * L

Substituting the true shell energy C*D*M*L into the rowwise route leaves one complete row-mass factor D*M.

theorem AnalyticNumberTheory.LargeSieve.rowwiseShortTypeIIScale_as_N {N D M Q C L : ℝ} (hN : N = D * M) : C * (D * M) * (D * (M + Q ^ 2)) * L = C * N * (N + D * Q ^ 2) * L

With N=D*M, the preceding scale is C*N*(N+D*Q^2)*L; it is not (N+Q^2(D+M)+Q^4)*polylog by itself.

theorem AnalyticNumberTheory.LargeSieve.bilinearMultiplicativeScale_as_N (N D M Q : ℕ) (hN : N = D * M) : bilinearMultiplicativeScale D M Q = ↑N + ↑Q ^ 2 * (↑D + ↑M) + ↑Q ^ 4

The desired bilinear coefficient is exactly N + Q^2(D+M) + Q^4 when N=D*M.