Explicit Q-dependent bilinear tensor moment bound

Expanding the outer d-sum and applying Cauchy only in d reduces the bilinear tensor second moment (the mixed fourth moment for rank-one tensors) to one nonmaximal weighted primitive large sieve for every row. Thus the exact rowwise charge is

D * (M + c(Q) * Q^2) * coefficientEnergy,

where c(Q) = 2 * ceil (log(Q^2) / log 2) + 12. This module also compares that expression with the genuine bilinear scale and gives an unconditional producer for the canonical Vaughan block. No prefix maximum is present; a prefix version should be obtained separately by the dyadic/Rademacher--Menshov reduction, paying its displayed logarithm squared.

noncomputable def AnalyticNumberTheory.LargeSieve.primitiveBilinearQFactor (Q : ℕ) : ℝ

The explicit logarithmic coefficient in the current primitive large sieve.

Equations

• AnalyticNumberTheory.LargeSieve.primitiveBilinearQFactor Q = 2 * ↑⌈Real.log (↑Q ^ 2) / Real.log 2⌉₊ + 12

theorem AnalyticNumberTheory.LargeSieve.primitiveBilinearQFactor_nonneg (Q : ℕ) : 0 ≤ primitiveBilinearQFactor Q

theorem AnalyticNumberTheory.LargeSieve.one_le_primitiveBilinearQFactor (Q : ℕ) : 1 ≤ primitiveBilinearQFactor Q

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_bilinearTensor_explicit (A : ℕ → ℤ → ℂ) (DS : Finset ℕ) (D M Q : ℕ) (hQ : 0 < Q) (hcard : DS.card ≤ D) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖bilinearTensorCharacterForm A DS M q χ‖ ^ 2 ≤ ↑D * (↑M + primitiveBilinearQFactor Q * ↑Q ^ 2) * bilinearTensorCoeffEnergy A DS M

Explicit generic nonmaximal bilinear tensor inequality. Cauchy in d and the existing weighted primitive large sieve give exactly the rowwise scale D * (M + c(Q) Q^2) times the full Frobenius energy.

theorem AnalyticNumberTheory.LargeSieve.rowwise_bilinear_scale_le_polylog_product (D M Q : ℕ) : ↑D * (↑M + primitiveBilinearQFactor Q * ↑Q ^ 2) ≤ primitiveBilinearQFactor Q * bilinearMultiplicativeScale D M Q

The rowwise explicit scale is bounded by the genuine bilinear product scale, with only the displayed logarithmic factor c(Q).

def AnalyticNumberTheory.LargeSieve.QDependentBilinearTensorFourthMomentBound (K : ℕ → ℝ) : Prop

Q-dependent version of the generic frontier. Unlike BilinearTensorFourthMomentBound K, its coefficient is allowed to display the unavoidable current Q-logarithm.

Equations

• AnalyticNumberTheory.LargeSieve.QDependentBilinearTensorFourthMomentBound K = ∀ (A : ℕ → ℤ → ℂ) (DS : Finset ℕ) (D M Q : ℕ), 0 < 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 Q * AnalyticNumberTheory.LargeSieve.bilinearMultiplicativeScale D M Q * AnalyticNumberTheory.LargeSieve.bilinearTensorCoeffEnergy A DS M

theorem AnalyticNumberTheory.LargeSieve.qDependentBilinearTensorFourthMomentBound_producer : QDependentBilinearTensorFourthMomentBound primitiveBilinearQFactor

Unconditional producer for the generic Q-dependent bilinear tensor bound.

theorem AnalyticNumberTheory.LargeSieve.vaughanCanonicalBilinearBlock_eq_bilinearTensorCharacterForm (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_coeffEnergy_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_unconditional (b : ℕ → ℂ) (y N u v k l Q : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖vaughanTypeIICanonicalBilinearBlock b y N u v k l q χ‖ ^ 2 ≤ primitiveBilinearQFactor Q * bilinearMultiplicativeScale (2 ^ k) (vaughanCanonicalTensorLength y k) Q * vaughanCanonicalShortTensorEnergy vaughanMangoldtCoeff b y N u v k l

Canonical Vaughan-block producer with no frozen fourth-moment hypothesis. This is the nonmaximal rectangle bound at the product scale, with the explicit current Q-logarithm.