The only analytic input below is the explicitly conditional unweighted Pan (1975) Theorem 2 specialization for the actual convolution error. The weight payment is modern finite Cauchy, as in Maynard Lemma 5.2 (5.19)--(5.20). It is not an application of ordinary prime Bombieri--Vinogradov to a convolution.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanActualError (κ : ℝ) (N : ℕ) (B : ℝ) (q : ℕ) : ℝ

Exactly the same interval, normalization and residue maximum as the weighted source.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanActualError κ N B q = MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeIntervalMaxL (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral κ) N (MathlibNt.SieveTheory.LiuWeight.liuPanSourceIntervalLower N B) (MathlibNt.SieveTheory.LiuWeight.liuPanSourceIntervalUpper N) q (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N))

theorem MathlibNt.SieveTheory.LiuWeight.liuPanActualError_nonneg (κ : ℝ) (N : ℕ) (B : ℝ) (q : ℕ) : 0 ≤ liuPanActualError κ N B q

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanUnweightedTheorem2Sum (κ : ℝ) (N : ℕ) (B : ℝ) : ℝ

The actual source mass with both μ² and 3^ω removed, not a prime discrepancy.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanUnweightedTheorem2Sum κ N B = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panSourceStrictModulusCutoff N B), MathlibNt.SieveTheory.LiuWeight.liuPanActualError κ N B q

def MathlibNt.SieveTheory.LiuWeight.LiuPanUnweightedTheorem2Specialization : Prop

Still-unproved analytic input: a Liu specialization of Pan (1975), Theorem 2. κ is fixed before U; U is the saving exponent, not the cutoff exponent B.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPanUnweightedTheorem2Specialization = ∃ (κ : ℝ), ∀ (U : ℝ), 0 < U → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → MathlibNt.SieveTheory.LiuWeight.liuPanUnweightedTheorem2Sum κ N B ≤ C * ↑N / Real.log ↑N ^ U

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSquarefreeCarrier (N : ℕ) (B : ℝ) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSquarefreeCarrier N B = Finset.filter Squarefree (Finset.range (MathlibNt.SieveTheory.LiuWeight.panSourceStrictModulusCutoff N B))

theorem MathlibNt.SieveTheory.LiuWeight.liuPanWeightedSum_eq_squarefree (κ : ℝ) (N : ℕ) (B : ℝ) : liuPanWangDingCorollary230Sum κ N B = Richert1969.threeOmegaErrorMass (liuPanSquarefreeCarrier N B) (liuPanActualError κ N B)

theorem MathlibNt.SieveTheory.LiuWeight.panSourceStrictModulusCutoff_mem_le {N q : ℕ} {B : ℝ} (hN : 1 ≤ N) (hlog : 1 ≤ Real.log ↑N) (hB : 0 ≤ B) (hq : q ∈ Finset.range (panSourceStrictModulusCutoff N B)) : q ≤ N

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSquarefreeCarrier_subset {N : ℕ} {B : ℝ} (hN : 1 ≤ N) (hlog : 1 ≤ Real.log ↑N) (hB : 0 ≤ B) : liuPanSquarefreeCarrier N B ⊆ Finset.range (N + 1)

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSquarefreeErrorSum_le_unweighted (κ : ℝ) (N : ℕ) (B : ℝ) : ∑ q ∈ liuPanSquarefreeCarrier N B, liuPanActualError κ N B q ≤ liuPanUnweightedTheorem2Sum κ N B

theorem MathlibNt.SieveTheory.LiuWeight.exists_liuPanWeightedSum_sq_le_unweighted : ∃ (C₉ : ℝ), 0 < C₉ ∧ ∀ (κ : ℝ) (N : ℕ) (B : ℝ), 2 ≤ N → 1 ≤ Real.log ↑N → 0 ≤ B → liuPanWangDingCorollary230Sum κ N B ^ 2 ≤ C₉ * Real.log (↑N + 2) ^ 9 * (liuActualEnvelopeConstant κ * ↑N * (1 + Real.log ↑N) ^ 2 * liuPanUnweightedTheorem2Sum κ N B)

A single global ninth-moment constant is fixed before κ,N,B. No distribution assumption or extra envelope hypothesis remains in this finite theorem.