Liu's factored Selberg main term

This module separates the exact finite factorization of Liu's M₁ from the two analytic estimates needed to bound its factors. The component bounds below are transparent propositions; no Selberg or logarithmic-integral estimate is asserted.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergReciprocalTotient : ArithmeticFunction ℝ

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergReciprocalTotient = { toFun := fun (d : ℕ) => if d = 0 then 0 else 1 / ↑d.totient, map_zero' := MathlibNt.SieveTheory.LiuWeight.liuSelbergReciprocalTotient._proof_1 }

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergReciprocalTotient_isMultiplicative : liuSelbergReciprocalTotient.IsMultiplicative

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergCoefficientFactor (N : ℕ) (epsilon : ℝ) (lambda : ℕ → ℝ) : ℝ

The quadratic Selberg coefficient factor on Liu's finite source carrier.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergCoefficientFactor N epsilon lambda = ∑ d1 ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergLambdaSourceCarrier N epsilon, ∑ d2 ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergLambdaSourceCarrier N epsilon, lambda d1 * lambda d2 / ↑(d1.lcm d2).totient

theorem MathlibNt.SieveTheory.LiuWeight.prime_dvd_liuPaperQModulus {N p : ℕ} {epsilon : ℝ} (hp : Nat.Prime p) : p ∣ liuPaperQModulus N epsilon ↔ p ≤ paperQSourceCutoff N epsilon ∧ ¬p ∣ N

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergBoundingSieve (N : ℕ) (epsilon : ℝ) (hNeven : Even N) : BoundingSieve

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergBoundingSieve N epsilon hNeven = { support := ∅, prodPrimes := MathlibNt.SieveTheory.LiuWeight.liuPaperQModulus N epsilon, prodPrimes_squarefree := ⋯, weights := fun (x : ℕ) => 0, weights_nonneg := MathlibNt.SieveTheory.LiuWeight.liuSelbergBoundingSieve._proof_1, totalMass := 0, nu := MathlibNt.SieveTheory.LiuWeight.liuSelbergReciprocalTotient, nu_mult := MathlibNt.SieveTheory.LiuWeight.liuSelbergReciprocalTotient_isMultiplicative, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

theorem MathlibNt.SieveTheory.LiuWeight.fullDivisors_quadraticSum_eq_liuSelbergCoefficientFactor_of_support {N : ℕ} {epsilon : ℝ} {lambda : ℕ → ℝ} (hlambda : ∀ (d : ℕ), lambda d ≠ 0 → d ∣ liuPaperQModulus N epsilon ∧ d ≤ paperQSourceCutoff N epsilon) : ∑ d1 ∈ (liuPaperQModulus N epsilon).divisors, ∑ d2 ∈ (liuPaperQModulus N epsilon).divisors, lambda d1 * lambda d2 / ↑(d1.lcm d2).totient = liuSelbergCoefficientFactor N epsilon lambda

Expanding the source carrier back to all divisors of the source modulus loses only terms whose lambda coefficient vanishes off the source support.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCoefficientFactor_eq_mainSum_lambdaSquared_of_support {N : ℕ} {epsilon : ℝ} {lambda : ℕ → ℝ} (hNeven : Even N) (hlambda : ∀ (d : ℕ), lambda d ≠ 0 → d ∣ liuPaperQModulus N epsilon ∧ d ≤ paperQSourceCutoff N epsilon) : BoundingSieve.mainSum (BoundingSieve.lambdaSquared lambda) = liuSelbergCoefficientFactor N epsilon lambda

The coefficient/diagonal-main-sum identity needs only source support, not the separate absolute bound used by Liu's remainder estimate.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCoefficientFactor_eq_mainSum_lambdaSquared {N : ℕ} {epsilon : ℝ} {lambda : ℕ → ℝ} (hNeven : Even N) (hlambda : LiuSelbergLambdaAdmissible N epsilon lambda) : BoundingSieve.mainSum (BoundingSieve.lambdaSquared lambda) = liuSelbergCoefficientFactor N epsilon lambda

Under the source support hypotheses and Even N, the Selberg coefficient factor is the diagonal main sum of a BoundingSieve with ν(d) = 1/φ(d).

theorem MathlibNt.SieveTheory.LiuWeight.fullDivisors_quadraticSum_eq_liuSelbergCoefficientFactor {N : ℕ} {epsilon : ℝ} {lambda : ℕ → ℝ} (hlambda : LiuSelbergLambdaAdmissible N epsilon lambda) : ∑ d1 ∈ (liuPaperQModulus N epsilon).divisors, ∑ d2 ∈ (liuPaperQModulus N epsilon).divisors, lambda d1 * lambda d2 / ↑(d1.lcm d2).totient = liuSelbergCoefficientFactor N epsilon lambda

The admissible-weight specialization of the support-only carrier identity.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCoefficientFactor_nonneg_of_admissible_even {N : ℕ} {epsilon : ℝ} {lambda : ℕ → ℝ} (hNeven : Even N) (hlambda : LiuSelbergLambdaAdmissible N epsilon lambda) : 0 ≤ liuSelbergCoefficientFactor N epsilon lambda

Under the source support hypotheses and Even N, the Selberg coefficient factor is a nonnegative diagonal sum of squares.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergMainTerm_eq_coefficientFactor_mul_weightMainSum (main : ℝ → ℝ) (N : ℕ) (epsilon : ℝ) (lambda : ℕ → ℝ) : liuSelbergMainTerm main N epsilon lambda = liuSelbergCoefficientFactor N epsilon lambda * liuWeightMainSum main N

Exact finite factorization of Liu's arbitrary-model Selberg main term.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergMainTerm_logarithmicIntegral_eq (kappa : ℝ) (N : ℕ) (epsilon : ℝ) (lambda : ℕ → ℝ) : liuSelbergMainTerm (liuLogarithmicIntegral kappa) N epsilon lambda = liuSelbergCoefficientFactor N epsilon lambda * liuWeightMainSum (liuLogarithmicIntegral kappa) N

Source-facing specialization of the finite factorization to Liu's genuine logarithmic-integral family.

def MathlibNt.SieveTheory.LiuWeight.LiuSelbergCoefficientFactorBound (delta : ℝ) (N : ℕ) (epsilon : ℝ) (lambda : ℕ → ℝ) : Prop

The sharp source Selberg coefficient upper estimate needed for Liu's M₁. Its sign is a theorem, not part of this input.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuSelbergCoefficientFactorBound delta N epsilon lambda = (MathlibNt.SieveTheory.LiuWeight.liuSelbergCoefficientFactor N epsilon lambda ≤ (8 + delta) * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N / Real.log ↑N)

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergMainTerm_le_of_componentBounds (kappa delta K : ℝ) (N : ℕ) (epsilon : ℝ) (lambda : ℕ → ℝ) (hNeven : Even N) (hlambda : LiuSelbergLambdaAdmissible N epsilon lambda) (hdelta : 0 ≤ 8 + delta) (hseries : 0 ≤ SingularSeries.liuSingularSeries N) (hlog : 0 < Real.log ↑N) (hcoefficient : LiuSelbergCoefficientFactorBound delta N epsilon lambda) (hweight : LiuGenuineLiWeightMainSumBound kappa K N) : liuSelbergMainTerm (liuLogarithmicIntegral kappa) N epsilon lambda ≤ (8 + delta) * K * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

Multiplying the two component estimates gives the M₁ coefficient (8 + delta) * K, with no numerical approximation.

theorem MathlibNt.SieveTheory.LiuWeight.liuM1_threePointNineFourZeroThreeThree_margin (delta eta : ℝ) (hmargin : 8 * eta + 0.49254 * delta + delta * eta ≤ 1e-5) : (8 + delta) * (0.49254 + eta) ≤ 3.94033

Exact decimal margin after writing K = 0.49254 + eta: the base product is 3.94032, leaving precisely 0.00001 for the linear and quadratic errors.

theorem MathlibNt.SieveTheory.LiuWeight.liuM1_threePointNineFourZeroThreeThree_margin_of_K_le (delta eta K : ℝ) (hdelta : 0 ≤ 8 + delta) (hK : K ≤ 0.49254 + eta) (hmargin : 8 * eta + 0.49254 * delta + delta * eta ≤ 1e-5) : (8 + delta) * K ≤ 3.94033

A version of the exact margin allowing any K ≤ 0.49254 + eta.

theorem MathlibNt.SieveTheory.LiuWeight.LiuSelbergMainTermUpperBound.of_componentBounds (kappa delta eta K : ℝ) (N : ℕ) (epsilon : ℝ) (lambda : ℕ → ℝ) (hNeven : Even N) (hlambda : LiuSelbergLambdaAdmissible N epsilon lambda) (hdelta : 0 ≤ 8 + delta) (hseries : 0 ≤ SingularSeries.liuSingularSeries N) (hlog : 0 < Real.log ↑N) (hK : K ≤ 0.49254 + eta) (hmargin : 8 * eta + 0.49254 * delta + delta * eta ≤ 1e-5) (hcoefficient : LiuSelbergCoefficientFactorBound delta N epsilon lambda) (hweight : LiuGenuineLiWeightMainSumBound kappa K N) : LiuSelbergMainTermUpperBound kappa N epsilon lambda

The printed 3.94033 bound follows only from the two explicit analytic component hypotheses, positivity, and the exact finite-algebra margin.