Liu's source Selberg coefficient

This module identifies the legacy Selberg-weight API with Liu's source modulus and finite coefficient carrier. The optimized numerical estimate is kept as a transparent eventual input; the legacy pointwise existence theorem does not provide it.

theorem MathlibNt.SieveTheory.LiuWeight.LegacySelberg.selbergQ_eq_liuPaperQModulus (N : ℕ) (epsilon : ℝ) : SelbergUpperBound.selbergQ N epsilon = liuPaperQModulus N epsilon

The legacy modulus is exactly Liu's source modulus. Both use the non-strict real cutoff p ≤ N^(1/4-epsilon/2), represented by the same floor.

theorem MathlibNt.SieveTheory.LiuWeight.LegacySelberg.SelbergWeights.liuSelbergLambdaAdmissible {N : ℕ} {epsilon : ℝ} (SW : SelbergUpperBound.SelbergWeights N epsilon) : LiuSelbergLambdaAdmissible N epsilon SW.lambda

Every legacy Selberg weight has Liu's source support and absolute bound.

theorem MathlibNt.SieveTheory.LiuWeight.LegacySelberg.SelbergWeights.lambda_one_source {N : ℕ} {epsilon : ℝ} (SW : SelbergUpperBound.SelbergWeights N epsilon) : SW.lambda 1 = 1

The source normalization is separate from admissibility because the latter is exactly the support-and-size interface needed by the remainder argument.

theorem MathlibNt.SieveTheory.LiuWeight.LegacySelberg.SelbergWeights.divisors_quadraticSum_eq_liuSelbergCoefficientFactor {N : ℕ} {epsilon : ℝ} (SW : SelbergUpperBound.SelbergWeights N epsilon) : ∑ d1 ∈ (SelbergUpperBound.selbergQ N epsilon).divisors, ∑ d2 ∈ (SelbergUpperBound.selbergQ N epsilon).divisors, SW.lambda d1 * SW.lambda d2 / ↑(d1.lcm d2).totient = liuSelbergCoefficientFactor N epsilon SW.lambda

Restricting the legacy divisor quadratic sum to Liu's filtered source carrier is exact. Terms outside the cutoff vanish by the legacy support condition; they are not silently discarded.

def MathlibNt.SieveTheory.LiuWeight.LegacySelberg.LiuOptimizedSelbergCoefficientEstimate (delta epsilon : ℝ) : Prop

The actual sharp input missing from the legacy development: for every sufficiently large even source parameter whose cutoff contains 1, an optimized Selberg weight exists. The conditional formulation avoids demanding impossible weights at small parameters with cutoff zero.

Equations

• MathlibNt.SieveTheory.LiuWeight.LegacySelberg.LiuOptimizedSelbergCoefficientEstimate delta epsilon = ∀ᶠ (N : ℕ) in Filter.atTop, Even N → 1 ≤ MathlibNt.SieveTheory.LiuWeight.paperQSourceCutoff N epsilon → ∃ (SW : MathlibNt.SieveTheory.SelbergUpperBound.SelbergWeights N epsilon), MathlibNt.SieveTheory.LiuWeight.LiuSelbergCoefficientFactorBound delta N epsilon SW.lambda

def MathlibNt.SieveTheory.LiuWeight.LegacySelberg.LiuOptimizedSelbergCoefficientInput : Prop

Source-faithful optimized Selberg input: an error tolerance first fixes a small epsilon range, and every epsilon in that range has an eventual family of optimized coefficients.

Equations

• MathlibNt.SieveTheory.LiuWeight.LegacySelberg.LiuOptimizedSelbergCoefficientInput = ∀ delta > 0, ∃ epsilon0 > 0, ∀ (epsilon : ℝ), 0 < epsilon → epsilon ≤ epsilon0 → MathlibNt.SieveTheory.LiuWeight.LegacySelberg.LiuOptimizedSelbergCoefficientEstimate delta epsilon