Liu's genuine-li Selberg main-term instantiation

This module combines the proved reciprocal-log transfer and optimized Selberg coefficient with the finite component-bound theorem. The source-facing result retains the evenness and nonempty-cutoff implications required by the optimized weight construction.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuGenuineLiWeightMainSumBound (kappa : ℝ) (hκ : 0 ≤ kappa) (eta : ℝ) (heta : 0 < eta) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → LiuGenuineLiWeightMainSumBound kappa (0.49254 + eta) N

Unconditional eventual form of Liu's genuine logarithmic-integral weight-sum estimate.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuM1Delta : ℝ

Exact coefficient error used in the assembled M₁ estimate.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuM1Delta = 1 / 10000000

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuM1Eta : ℝ

Exact genuine-logarithmic-integral error used in the assembled M₁ estimate.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuM1Eta = 1 / 10000000

theorem MathlibNt.SieveTheory.LiuWeight.liuM1Delta_pos : 0 < liuM1Delta

theorem MathlibNt.SieveTheory.LiuWeight.liuM1Eta_pos : 0 < liuM1Eta

theorem MathlibNt.SieveTheory.LiuWeight.liuM1DeltaEta_margin : 8 * liuM1Eta + 0.49254 * liuM1Delta + liuM1Delta * liuM1Eta ≤ 1e-5

theorem MathlibNt.SieveTheory.LiuWeight.eventually_exists_liuGenuineLiSelbergMainTermUpperBound (kappa : ℝ) (hκ : 0 ≤ kappa) : ∃ (epsilon0 : ℝ), 0 < epsilon0 ∧ ∀ (epsilon : ℝ), 0 < epsilon → epsilon ≤ epsilon0 → ∀ᶠ (N : ℕ) in Filter.atTop, Even N → 1 ≤ paperQSourceCutoff N epsilon → ∃ (SW : SelbergUpperBound.SelbergWeights N epsilon), LiuSelbergLambdaAdmissible N epsilon SW.lambda ∧ LiuSelbergMainTermUpperBound kappa N epsilon SW.lambda

For every nonnegative normalization, Liu's proved source estimates furnish an eventual family of admissible Selberg weights satisfying the printed M₁ main-term bound.