theorem AnalyticNumberTheory.LargeSieve.liuHarmonic_le_three_log_add_one (X : ℕ) : MathlibNt.SieveTheory.LiuWeight.liuHarmonic X ≤ 3 * Real.log ↑(X + 1)

theorem AnalyticNumberTheory.LargeSieve.sum_Icc_int_toNat_eq_sum_Icc {F : ℕ → ℝ} (X : ℕ) : ∑ t ∈ Finset.Icc 1 ↑X, F t.toNat = ∑ n ∈ Finset.Icc 1 X, F n

theorem AnalyticNumberTheory.LargeSieve.divisorSquareWeightedPrefix_le_fourth_harmonic (X : ℕ) : ∑ t ∈ Finset.Icc 1 X, ↑t.divisors.card ^ 2 * (↑t)⁻¹ ≤ MathlibNt.SieveTheory.LiuWeight.liuHarmonic X ^ 4

Weighted divisor-square energy in the form used in Chen's Lemma 3. The elementary four-harmonic proof keeps the endpoint X = 0 harmless.

theorem AnalyticNumberTheory.LargeSieve.divisorSquareMomentBound_27 : DivisorSquareMomentBound 27

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

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