Divisor-square moments for the actual Vaughan Type-II tensor energy

The fibre Cauchy bound is summed in (d,t) before any pointwise estimate in n = d*t. Each actual e*m=t fibre injects into the divisors of t, and its Mangoldt energy is bounded by the same divisor count times log (y+1)^2. Thus a whole fixed-d row is controlled by a divisor-square prefix at length y/d.

The only frozen analytic input below is the classical divisor-square moment bound. It is stated for that scalar prefix, not for the tensor energy or for the final Type-II conclusion.

noncomputable def AnalyticNumberTheory.LargeSieve.divisorSquarePrefix (X : ℕ) : ℝ

The scalar divisor-square prefix, written on the integer interval used by the primitive large-sieve modules. On this interval t.toNat is positive.

Equations

• AnalyticNumberTheory.LargeSieve.divisorSquarePrefix X = ∑ t ∈ Finset.Icc 1 ↑X, ↑t.toNat.divisors.card ^ 2

def AnalyticNumberTheory.LargeSieve.DivisorSquareMomentBound (C : ℝ) : Prop

The minimal classical analytic input: an explicit X log^3(X+1) upper bound for the second moment of the divisor function.

Equations

• AnalyticNumberTheory.LargeSieve.DivisorSquareMomentBound C = ∀ (X : ℕ), AnalyticNumberTheory.LargeSieve.divisorSquarePrefix X ≤ C * ↑X * Real.log ↑(X + 1) ^ 3

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanQuotientMass (y : ℕ) (DS : Finset ℕ) : ℝ

The quotient mass left after applying the divisor moment row by row.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanQuotientMass y DS = ∑ d ∈ DS, ↑(y / d)

theorem AnalyticNumberTheory.LargeSieve.vaughanTensorFiber_subset_divisors (y d : ℕ) (ES : Finset ℕ) (t : ℤ) (ht : t ∈ Finset.Icc 1 ↑y) : vaughanTensorFiber y d ES t ⊆ t.toNat.divisors

theorem AnalyticNumberTheory.LargeSieve.vaughanTensorFiberMultiplicity_le_divisors (y d : ℕ) (ES : Finset ℕ) (t : ℤ) (ht : t ∈ Finset.Icc 1 ↑y) : vaughanTensorFiberMultiplicity y d ES t ≤ t.toNat.divisors.card

theorem AnalyticNumberTheory.LargeSieve.vaughanTensorFiber_support (y d : ℕ) (ES : Finset ℕ) (t : ℤ) (hd : 0 < d) (ht : t ∈ Finset.Icc 1 ↑y) (hne : (vaughanTensorFiber y d ES t).Nonempty) : d * t.toNat ≤ y

theorem AnalyticNumberTheory.LargeSieve.vaughanTensorFiberMangoldtEnergy_le (y d : ℕ) (ES : Finset ℕ) (t : ℤ) (hES : ∀ e ∈ ES, 0 < e) (ht : t ∈ Finset.Icc 1 ↑y) : vaughanTensorFiberMangoldtEnergy y d ES t ≤ ↑t.toNat.divisors.card * Real.log ↑(y + 1) ^ 2

theorem AnalyticNumberTheory.LargeSieve.vaughanTensorFiber_weight_le_divisor_sq (y d : ℕ) (ES : Finset ℕ) (t : ℤ) (hES : ∀ e ∈ ES, 0 < e) (ht : t ∈ Finset.Icc 1 ↑y) : ↑(vaughanTensorFiberMultiplicity y d ES t) * vaughanTensorFiberMangoldtEnergy y d ES t ≤ ↑t.toNat.divisors.card ^ 2 * Real.log ↑(y + 1) ^ 2

Pointwise only at the divisor weight (never at ambient length y): the multiplicity times Mangoldt energy is at most tau(t)^2 log(y+1)^2.

theorem AnalyticNumberTheory.LargeSieve.vaughanActualTensorCoeffEnergy_le_divisorSquarePrefixes (b : ℕ → ℂ) (y : ℕ) (DS ES : Finset ℕ) (B : ℝ) (hDS : ∀ d ∈ DS, 0 < d) (hES : ∀ e ∈ ES, 0 < e) (hB : ∀ n ≤ y, ‖b n‖ ≤ B) : vaughanActualTensorCoeffEnergy b y DS ES ≤ B ^ 2 * Real.log ↑(y + 1) ^ 2 * ∑ d ∈ DS, divisorSquarePrefix (y / d)

Finite combinatorial rearrangement: after summing over all (d,t), the actual tensor coefficient energy is bounded by a sum of divisor-square moments at the physical row lengths y/d.

theorem AnalyticNumberTheory.LargeSieve.vaughanActualTensorCoeffEnergy_le_of_divisorSquareMoment (b : ℕ → ℂ) (y : ℕ) (DS ES : Finset ℕ) (B C : ℝ) (hDS : ∀ d ∈ DS, 0 < d) (hES : ∀ e ∈ ES, 0 < e) (hB : ∀ n ≤ y, ‖b n‖ ≤ B) (hMoment : DivisorSquareMomentBound C) (hC : 0 ≤ C) : vaughanActualTensorCoeffEnergy b y DS ES ≤ C * B ^ 2 * Real.log ↑(y + 1) ^ 5 * vaughanQuotientMass y DS

Consequence of the frozen scalar divisor-square moment. No tensor-energy or Type-II conclusion occurs in the premise.

theorem AnalyticNumberTheory.LargeSieve.card_vaughanCanonicalDyadicBlock_le_pow (N u k : ℕ) : (vaughanCanonicalDyadicBlock N u k).card ≤ 2 ^ k

A canonical binary shell has at most its lower endpoint 2^k integers. This is the finite cardinality input that cancels the row length.

theorem AnalyticNumberTheory.LargeSieve.vaughanQuotientMass_canonical_le (y N u k : ℕ) : vaughanQuotientMass y (vaughanCanonicalDyadicBlock N u k) ≤ ↑y

On one canonical d-shell, the sum of physical row lengths y/d is at most y; no pointwise ambient-y loss is paid for every d.

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

Premise-minimal canonical-row closure. The classical divisor-square moment alone gives actual tensor energy O(y log^5 y) on every dyadic shell; the shell cardinality cancels against the physical row length.

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

The same canonical closure in the tensor-energy slot consumed by the weighted primitive full Type-II rectangle ledger.

theorem AnalyticNumberTheory.LargeSieve.vaughanActualTensorCoeffEnergy_le_BVScale (b : ℕ → ℂ) (y : ℕ) (DS ES : Finset ℕ) (B C : ℝ) (hDS : ∀ d ∈ DS, 0 < d) (hES : ∀ e ∈ ES, 0 < e) (hB : ∀ n ≤ y, ‖b n‖ ≤ B) (hMoment : DivisorSquareMomentBound C) (hC : 0 ≤ C) (hQuotient : vaughanQuotientMass y DS ≤ ↑y * Real.log ↑(y + 1)) : vaughanActualTensorCoeffEnergy b y DS ES ≤ C * B ^ 2 * ↑y * Real.log ↑(y + 1) ^ 6

BV-compatible scalar scale: a harmonic quotient-mass estimate of size y log(y+1) turns the second divisor moment into y log^6(y+1).

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearTensorEnergy_le_BVScale (b : ℕ → ℂ) (y : ℕ) (DS ES : Finset ℕ) (B C : ℝ) (hDS : ∀ d ∈ DS, 0 < d) (hES : ∀ e ∈ ES, 0 < e) (hB : ∀ n ≤ y, ‖b n‖ ≤ B) (hMoment : DivisorSquareMomentBound C) (hC : 0 ≤ C) (hQuotient : vaughanQuotientMass y DS ≤ ↑y * Real.log ↑(y + 1)) : vaughanBilinearTensorEnergy vaughanMangoldtCoeff b y DS ES ≤ C * B ^ 2 * ↑y * Real.log ↑(y + 1) ^ 6

The actual-energy estimate closes the tensor-energy slot used by the full Type-II rectangle ledger. Its premises are only the scalar divisor moment, a coefficient supremum, and the explicit quotient-mass estimate.