Primitive-character bilinear large sieve for Vaughan Type II rectangles

The inner e,m packet is first collected by the product t=e*m. Its coefficient is independent of the character, so the weighted primitive Bombieri--Davenport inequality can be applied for each outer d. Cauchy is used only in d; no coefficient is ever repackaged and squared by n=d*e*m.

def AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorCoeff (β c : ℕ → ℂ) (y d : ℕ) (ES : Finset ℕ) (t : ℤ) : ℂ

The character-free tensor coefficient obtained by collecting all pairs (e,m) in the inner packet with product t=e*m.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorCoeff β c y d ES t = ∑ e ∈ ES, ∑ m ∈ Finset.Icc 1 (y / (d * e)), if ↑(e * m) = t then β e * c (d * t.toNat) else 0

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanBilinearCoeffEnergy (α : ℕ → ℂ) (DS : Finset ℕ) : ℝ

Raw coefficient energy in the outer variable.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanBilinearCoeffEnergy α DS = ∑ d ∈ DS, ‖α d‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorEnergy (β c : ℕ → ℂ) (y : ℕ) (DS ES : Finset ℕ) : ℝ

The consumable tensor energy after the second (e,m → t) rearrangement.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorEnergy β c y DS ES = ∑ d ∈ DS, ∑ t ∈ Finset.Icc 1 ↑y, ‖AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorCoeff β c y d ES t‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanBilinearBlockOn (α β c : ℕ → ℂ) (y : ℕ) (DS ES : Finset ℕ) (q : ℕ) (χ : PrimitiveCharacter q) : ℂ

A bilinear rectangle over arbitrary positive finite d and e supports.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanBilinearBlockOn α β c y DS ES q χ = ∑ d ∈ DS, α d * ↑χ ↑d * ∑ e ∈ ES, β e * ↑χ ↑e * ∑ m ∈ Finset.Icc 1 (y / (d * e)), c (d * e * m) * ↑χ ↑m

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearInner_eq_tensor (β c : ℕ → ℂ) (y d : ℕ) (ES : Finset ℕ) (q : ℕ) (χ : PrimitiveCharacter q) (hd : 0 < d) (hES : ∀ e ∈ ES, 0 < e) : ∑ e ∈ ES, β e * ↑χ ↑e * ∑ m ∈ Finset.Icc 1 (y / (d * e)), c (d * e * m) * ↑χ ↑m = ∑ t ∈ Finset.Icc 1 ↑y, vaughanBilinearTensorCoeff β c y d ES t * ↑χ ↑t

Exact second rearrangement of the inner packet. The right-hand coefficients contain no occurrence of χ.

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearBlockOn_eq_tensor (α β c : ℕ → ℂ) (y : ℕ) (DS ES : Finset ℕ) (q : ℕ) (χ : PrimitiveCharacter q) (hDS : ∀ d ∈ DS, 0 < d) (hES : ∀ e ∈ ES, 0 < e) : vaughanBilinearBlockOn α β c y DS ES q χ = ∑ d ∈ DS, α d * ↑χ ↑d * ∑ t ∈ Finset.Icc 1 ↑y, vaughanBilinearTensorCoeff β c y d ES t * ↑χ ↑t

Whole-block tensor form, obtained before any analytic estimate.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanBilinearLargeSieveConstant (y Q : ℕ) : ℝ

The primitive-character large-sieve constant at physical packet length y and conductor cap Q.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanBilinearLargeSieveConstant y Q = AnalyticNumberTheory.LargeSieve.largeSieveBound y (1 / ↑Q ^ 2)

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearLargeSieveConstant_eq_explicit (y Q : ℕ) (hQ : 0 < Q) : vaughanBilinearLargeSieveConstant y Q = ↑y + (2 * ↑⌈Real.log (↑Q ^ 2) / Real.log 2⌉₊ + 12) * ↑Q ^ 2

Expanded physical constant inherited from the reduced-Farey large sieve.

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearBlockOn_norm_sq_le (α β c : ℕ → ℂ) (y : ℕ) (DS ES : Finset ℕ) (q : ℕ) (χ : PrimitiveCharacter q) (hDS : ∀ d ∈ DS, 0 < d) (hES : ∀ e ∈ ES, 0 < e) : ‖vaughanBilinearBlockOn α β c y DS ES q χ‖ ^ 2 ≤ vaughanBilinearCoeffEnergy α DS * ∑ d ∈ DS, ‖∑ t ∈ Finset.Icc 1 ↑y, vaughanBilinearTensorCoeff β c y d ES t * ↑χ ↑t‖ ^ 2

Cauchy only in the outer variable, after the packet has become a genuine one-variable character sum.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanBilinearBlockOn (α β c : ℕ → ℂ) (y Q : ℕ) (DS ES : Finset ℕ) (hQ : 0 < Q) (hDS : ∀ d ∈ DS, 0 < d) (hES : ∀ e ∈ ES, 0 < e) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖vaughanBilinearBlockOn α β c y DS ES q χ‖ ^ 2 ≤ vaughanBilinearCoeffEnergy α DS * vaughanBilinearLargeSieveConstant y Q * vaughanBilinearTensorEnergy β c y DS ES

Weighted primitive-character bilinear large sieve over a finite positive rectangle. The two energies are kept separate: the raw d-coefficient energy and the character-free (d,t) tensor energy.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanBilinearDyadic (α β c : ℕ → ℂ) (y D E Q : ℕ) (hQ : 0 < Q) (hD : 0 < D) (hE : 0 < E) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖vaughanBilinearBlockOn α β c y (vaughanDyadicBlock D) (vaughanDyadicBlock E) q χ‖ ^ 2 ≤ vaughanBilinearCoeffEnergy α (vaughanDyadicBlock D) * vaughanBilinearLargeSieveConstant y Q * vaughanBilinearTensorEnergy β c y (vaughanDyadicBlock D) (vaughanDyadicBlock E)

Dyadic specialization. The parameters D,E,y,Q remain literal and the coefficient energies are not replaced by pointwise cardinality bounds.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanBilinearDyadic_explicit (α β c : ℕ → ℂ) (y D E Q : ℕ) (hQ : 0 < Q) (hD : 0 < D) (hE : 0 < E) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖vaughanBilinearBlockOn α β c y (vaughanDyadicBlock D) (vaughanDyadicBlock E) q χ‖ ^ 2 ≤ vaughanBilinearCoeffEnergy α (vaughanDyadicBlock D) * (↑y + (2 * ↑⌈Real.log (↑Q ^ 2) / Real.log 2⌉₊ + 12) * ↑Q ^ 2) * vaughanBilinearTensorEnergy β c y (vaughanDyadicBlock D) (vaughanDyadicBlock E)

Fully expanded dyadic form: all four physical parameters D,E,y,Q and both coefficient energies remain visible.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanCanonicalBilinear (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 ≤ vaughanBilinearCoeffEnergy vaughanMoebiusCoeff (vaughanCanonicalDyadicBlock N u k) * vaughanBilinearLargeSieveConstant y Q * vaughanBilinearTensorEnergy vaughanMangoldtCoeff b y (vaughanCanonicalDyadicBlock N u k) (vaughanCanonicalDyadicBlock N v l)

Canonical-rectangle specialization used by the full Type-II ledger.