Explicit moment bound for the long-variable Vaughan Type-I coefficient

The two truncated convolutions are opened before summing over n. The Möbius factor has absolute value at most one. In the middle convolution the nonnegative truncated Λ-sum is enlarged to the full divisor sum and then identified with log. Consequently each Type-I piece is bounded by τ(n) log (N+1), uniformly in both cutoffs. The divisor-square moment with constant 27 then gives an N log^5(N+1) coefficient moment.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeI_abs_le_two_divisors_mul_log {n N u v : ℕ} (hn : 0 < n) (hnN : n ≤ N) : |vaughanTypeI n u v| ≤ 2 * ↑n.divisors.card * Real.log ↑(N + 1)

Uniform pointwise Type-I estimate obtained from the opened μ * log and μ * Λ convolutions. In particular it has no polynomial dependence on the cutoffs u,v.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeILongCoeff_norm_sq_le_divisor_sq (b : ℤ → ℂ) (N u v : ℕ) (B : ℝ) (n : ℤ) (hn : n ∈ Finset.Icc 1 ↑N) (hB : ‖b n‖ ≤ B) : ‖vaughanTypeILongCoeff b u v n‖ ^ 2 ≤ 4 * B ^ 2 * ↑n.toNat.divisors.card ^ 2 * Real.log ↑(N + 1) ^ 2

Pointwise square bound for the actual long-variable coefficient.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeILongCoeffMoment_le_explicit (b : ℤ → ℂ) (N u v : ℕ) (B : ℝ) (hB : ∀ n ∈ Finset.Icc 1 ↑N, ‖b n‖ ≤ B) : vaughanTypeILongCoeffMoment b N u v ≤ 108 * B ^ 2 * ↑N * Real.log ↑(N + 1) ^ 5

Explicit N log^5(N+1) moment bound. The constant is 4 * 27 = 108; all dependence on N,u,v is displayed (and the estimate is uniform in u,v).

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeILongCoeffMomentBound_of_bounded (b : ℤ → ℂ) (N u v : ℕ) (B : ℝ) (hB : ∀ n ∈ Finset.Icc 1 ↑N, ‖b n‖ ≤ B) : VaughanTypeILongCoeffMomentBound b N u v (108 * B ^ 2) 5

Concrete inhabitant of the frozen Type-I coefficient-moment interface.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanTypeILong_unconditional (b : ℤ → ℂ) (N Q u v : ℕ) (B : ℝ) (hQ : 0 < Q) (hB : ∀ n ∈ Finset.Icc 1 ↑N, ‖b n‖ ≤ B) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare (vaughanTypeILongCoeff b u v) 0 N q χ ≤ ↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N Q * (108 * B ^ 2 * ↑N * Real.log ↑(N + 1) ^ 5)

Premise-free-in-the-moment weighted primitive Type-I prefix-maximal bound. The only coefficient assumption is the displayed finite B-bound; no analytic moment hypothesis remains.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanTypeILong_rearranged_unconditional (b : ℤ → ℂ) (N Q u v : ℕ) (B : ℝ) (hQ : 0 < Q) (hB : ∀ n ∈ Finset.Icc 1 ↑N, ‖b n‖ ≤ B) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, vaughanTypeILongPrefixMaxSquare b N u v q χ ≤ ↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N Q * (108 * B ^ 2 * ↑N * Real.log ↑(N + 1) ^ 5)

The same unconditional result with the left side written as the exact short-times-long rearranged Type-I prefixes.