Liu's Selberg denominator asymptotic

The moving source cutoff has the expected logarithmic scale. Combining this with the uniform harmonic remainder and the triangular Euler error gives the sharp normalized asymptotic for Liu's finite Selberg denominator, and hence the optimized coefficient input.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_log_floor_rpow_div_log (beta : ℝ) (hbeta : 0 < beta) : Filter.Tendsto (fun (N : ℕ) => Real.log ↑⌊↑N ^ beta⌋₊ / Real.log ↑N) Filter.atTop (nhds beta)

Flooring a positive real power does not change its logarithmic scale.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_log_paperQSourceCutoff_div_log (epsilon : ℝ) (hbeta : 0 < 1 / 4 - epsilon / 2) : Filter.Tendsto (fun (N : ℕ) => Real.log ↑(paperQSourceCutoff N epsilon) / Real.log ↑N) Filter.atTop (nhds (1 / 4 - epsilon / 2))

The paper's moving cutoff has logarithmic scale 1/4 - epsilon/2.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_liuSelbergDenominator_normalized_even (epsilon : ℝ) (hbeta : 0 < 1 / 4 - epsilon / 2) : Filter.Tendsto (fun (N : ℕ) => liuSelbergDenominator N epsilon * SingularSeries.liuSingularSeries N / Real.log ↑N) (Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}) (nhds ((1 / 4 - epsilon / 2) / 2))

Along the even integers, Liu's denominator has the sharp normalized limit.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergDenominatorLowerBound_of_lt_margin {delta epsilon : ℝ} (hdelta : 0 < delta) (hmargin : epsilon < delta / (2 * (8 + delta))) : LiuSelbergDenominatorLowerBound delta epsilon

A strict epsilon margin converts the normalized limit into the required eventual lower bound.

theorem MathlibNt.SieveTheory.LiuWeight.exists_liuSelbergDenominatorLowerBound (delta : ℝ) : delta > 0 → ∃ epsilon0 > 0, ∀ (epsilon : ℝ), 0 < epsilon → epsilon ≤ epsilon0 → LiuSelbergDenominatorLowerBound delta epsilon

Every positive loss admits a positive epsilon interval on which the sharp Selberg denominator lower bound holds.

theorem MathlibNt.SieveTheory.LiuWeight.liuOptimizedSelbergCoefficientInput : LegacySelberg.LiuOptimizedSelbergCoefficientInput

Liu's optimized Selberg coefficient input follows from the proved denominator lower bound; the definition itself remains unchanged.