Actual tensor energy and rectangle aggregation for Vaughan Type II

This module bounds the coefficient obtained after collecting t=e*m by Cauchy on the actual fibre. The subsequent sum remains a sum in (d,t); it is never repackaged pointwise in n=d*e*m.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTensorFiber (y d : ℕ) (ES : Finset ℕ) (t : ℤ) : Finset ℕ

The actual e-fibre above t, including the physical cutoff on m.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTensorFiber y d ES t = {e ∈ ES | ∃ m ∈ Finset.Icc 1 (y / (d * e)), ↑(e * m) = t}

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTensorFiberMultiplicity (y d : ℕ) (ES : Finset ℕ) (t : ℤ) : ℕ

Number of representations in the actual t=e*m fibre.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTensorFiberMultiplicity y d ES t = (AnalyticNumberTheory.LargeSieve.vaughanTensorFiber y d ES t).card

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTensorFiberMangoldtEnergy (y d : ℕ) (ES : Finset ℕ) (t : ℤ) : ℝ

The Λ square-energy on one actual fibre.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTensorFiberMangoldtEnergy y d ES t = ∑ e ∈ AnalyticNumberTheory.LargeSieve.vaughanTensorFiber y d ES t, ‖AnalyticNumberTheory.LargeSieve.vaughanMangoldtCoeff e‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanActualTensorCoeffEnergy (b : ℕ → ℂ) (y : ℕ) (DS ES : Finset ℕ) : ℝ

The external coefficient energy with precisely the multiplicity and Λ-energy generated by fibre Cauchy. Keeping this as a (d,t) sum is the key distinction from a pointwise estimate after n=d*e*m.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanActualTensorCoeffEnergy b y DS ES = ∑ d ∈ DS, ∑ t ∈ Finset.Icc 1 ↑y, ↑(AnalyticNumberTheory.LargeSieve.vaughanTensorFiberMultiplicity y d ES t) * AnalyticNumberTheory.LargeSieve.vaughanTensorFiberMangoldtEnergy y d ES t * ‖b (d * t.toNat)‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorCoeff_eq_fiber (b : ℕ → ℂ) (y d : ℕ) (ES : Finset ℕ) (t : ℤ) (hES : ∀ e ∈ ES, 0 < e) : vaughanBilinearTensorCoeff vaughanMangoldtCoeff b y d ES t = ∑ e ∈ vaughanTensorFiber y d ES t, vaughanMangoldtCoeff e * b (d * t.toNat)

Exact fibre form of the actual Vaughan tensor coefficient.

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorCoeff_norm_sq_le_fiber (b : ℕ → ℂ) (y d : ℕ) (ES : Finset ℕ) (t : ℤ) (hES : ∀ e ∈ ES, 0 < e) : ‖vaughanBilinearTensorCoeff vaughanMangoldtCoeff b y d ES t‖ ^ 2 ≤ ↑(vaughanTensorFiberMultiplicity y d ES t) * vaughanTensorFiberMangoldtEnergy y d ES t * ‖b (d * t.toNat)‖ ^ 2

Cauchy on the actual divisor fibre. Its two factors are the literal fibre multiplicity and the literal Λ square-energy.

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorEnergy_le_actual (b : ℕ → ℂ) (y : ℕ) (DS ES : Finset ℕ) (hES : ∀ e ∈ ES, 0 < e) : vaughanBilinearTensorEnergy vaughanMangoldtCoeff b y DS ES ≤ vaughanActualTensorCoeffEnergy b y DS ES

The actual tensor energy is compressed without leaving the full (d,t) sum. No pointwise D²E² coefficient estimate occurs.

theorem AnalyticNumberTheory.LargeSieve.vaughanTensorFiberMangoldtEnergy_nonneg (y d : ℕ) (ES : Finset ℕ) (t : ℤ) : 0 ≤ vaughanTensorFiberMangoldtEnergy y d ES t

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorEnergy_le_of_fiber_caps (b : ℕ → ℂ) (y : ℕ) (DS ES : Finset ℕ) (Δ LΛ B : ℝ) (hES : ∀ e ∈ ES, 0 < e) (hΔ : ∀ d ∈ DS, ∀ t ∈ Finset.Icc 1 ↑y, ↑(vaughanTensorFiberMultiplicity y d ES t) ≤ Δ) (hΛ : ∀ d ∈ DS, ∀ t ∈ Finset.Icc 1 ↑y, vaughanTensorFiberMangoldtEnergy y d ES t ≤ LΛ) (hB : ∑ d ∈ DS, ∑ t ∈ Finset.Icc 1 ↑y, ‖b (d * t.toNat)‖ ^ 2 ≤ B) (hΔ0 : 0 ≤ Δ) (hΛ0 : 0 ≤ LΛ) : vaughanBilinearTensorEnergy vaughanMangoldtCoeff b y DS ES ≤ Δ * LΛ * B

A scalar consumer of the exact (d,t) ledger. Δ is a divisor-fibre multiplicity cap, LΛ a fibrewise Mangoldt-energy cap, and B the summed external coefficient energy.

theorem AnalyticNumberTheory.LargeSieve.vaughanMoebiusCoeffEnergy_le_card (DS : Finset ℕ) : vaughanBilinearCoeffEnergy vaughanMoebiusCoeff DS ≤ ↑DS.card

Möbius has unit pointwise square budget, hence its energy is at most the literal outer-block cardinality.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanCanonicalBilinear_actual (b : ℕ → ℂ) (y N u v k l Q : ℕ) (Δ LΛ B : ℝ) (hQ : 0 < Q) (hΔ : ∀ d ∈ vaughanCanonicalDyadicBlock N u k, ∀ t ∈ Finset.Icc 1 ↑y, ↑(vaughanTensorFiberMultiplicity y d (vaughanCanonicalDyadicBlock N v l) t) ≤ Δ) (hΛ : ∀ d ∈ vaughanCanonicalDyadicBlock N u k, ∀ t ∈ Finset.Icc 1 ↑y, vaughanTensorFiberMangoldtEnergy y d (vaughanCanonicalDyadicBlock N v l) t ≤ LΛ) (hB : ∑ d ∈ vaughanCanonicalDyadicBlock N u k, ∑ t ∈ Finset.Icc 1 ↑y, ‖b (d * t.toNat)‖ ^ 2 ≤ B) (hΔ0 : 0 ≤ Δ) (hΛ0 : 0 ≤ LΛ) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖vaughanTypeIICanonicalBilinearBlock b y N u v k l q χ‖ ^ 2 ≤ ↑(vaughanCanonicalDyadicBlock N u k).card * vaughanBilinearLargeSieveConstant y Q * (Δ * LΛ * B)

Actual canonical-block primitive bound after inserting the fibre and external-coefficient energies.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIIFullPrefix_norm_sq_le_rectangles (b : ℕ → ℂ) (y N u v q : ℕ) (χ : PrimitiveCharacter q) (hyN : y ≤ N) : ‖vaughanTypeIIFullPrefix b y u v q χ‖ ^ 2 ≤ ↑(Nat.log 2 N + 1) ^ 2 * ∑ kl ∈ vaughanCanonicalDyadicRectangles N u v, ‖vaughanTypeIICanonicalBilinearBlock b y N u v kl.1 kl.2 q χ‖ ^ 2

Rectangle-count Cauchy, in the exact form used to reconstruct the full Type-II prefix.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanTypeIIFullPrefix (b : ℕ → ℂ) (y N u v Q : ℕ) (hQ : 0 < Q) (hyN : y ≤ N) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖vaughanTypeIIFullPrefix b y u v q χ‖ ^ 2 ≤ ↑(Nat.log 2 N + 1) ^ 2 * ∑ kl ∈ vaughanCanonicalDyadicRectangles N u v, vaughanBilinearCoeffEnergy vaughanMoebiusCoeff (vaughanCanonicalDyadicBlock N u kl.1) * vaughanBilinearLargeSieveConstant y Q * vaughanBilinearTensorEnergy vaughanMangoldtCoeff b y (vaughanCanonicalDyadicBlock N u kl.1) (vaughanCanonicalDyadicBlock N v kl.2)

Full weighted primitive maximal ledger. Rectangle Cauchy costs exactly (log₂ N+1)²; the right side is the sum of the already proved canonical-block primitive energies, so no second pointwise coefficient loss is introduced.