Liu's Selberg assembly on the even filter

This module instantiates the source-facing Selberg argument with the explicit optimizer liuSelbergOptimalLambda N epsilon. Evenness is carried by the filter rather than requested for all natural numbers. It retains the componentwise source-input route and also supplies the canonical aggregate Pan--Wang--Ding route.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuEvenAssemblyEpsilon0 : ℝ

A fixed epsilon endpoint below both the denominator margin used for M₁ and 1 / 2.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuEvenAssemblyEpsilon0 = 1 / 10000000000

theorem MathlibNt.SieveTheory.LiuWeight.liuEvenAssemblyEpsilon0_pos : 0 < liuEvenAssemblyEpsilon0

theorem MathlibNt.SieveTheory.LiuWeight.liuEvenAssemblyEpsilon0_lt_m1_margin : liuEvenAssemblyEpsilon0 < liuM1Delta / (2 * (8 + liuM1Delta))

theorem MathlibNt.SieveTheory.LiuWeight.liuEvenAssemblyEpsilon0_lt_half : liuEvenAssemblyEpsilon0 < 1 / 2

theorem MathlibNt.SieveTheory.LiuWeight.eventually_one_le_paperQSourceCutoff_of_le_evenAssemblyEpsilon0 {epsilon : ℝ} (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) : ∀ᶠ (N : ℕ) in Filter.atTop, 1 ≤ paperQSourceCutoff N epsilon

For every epsilon in the fixed assembly interval, the source cutoff eventually contains 1.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuSelbergOptimalLambda_admissible_even {epsilon : ℝ} (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) : ∀ᶠ (N : ℕ) in Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}, LiuSelbergLambdaAdmissible N epsilon (liuSelbergOptimalLambda N epsilon)

The explicit optimal coefficients are eventually admissible along the even natural numbers.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuSelbergOptimalLambda_mainTermUpperBound_even (kappa : ℝ) (hκ : 0 ≤ kappa) {epsilon : ℝ} (_hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) : ∀ᶠ (N : ℕ) in Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}, LiuSelbergMainTermUpperBound kappa N epsilon (liuSelbergOptimalLambda N epsilon)

The explicit optimal coefficients satisfy Liu's printed M₁ bound eventually along the even natural numbers.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_abs_liuSelbergOptimalRemainder_le_even_of_sourceInputs (kappa epsilon A B C1 C2 C3 : ℝ) (u v : ℕ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hB : 0 ≤ B) (hI : ∀ᶠ (N : ℕ) in Filter.atTop, LiuMainPanTypeIPieceBoundAt N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C1 u) (hII : ∀ᶠ (N : ℕ) in Filter.atTop, LiuMainPanTypeIIPieceBoundAt N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C2 u v) (hresidual : ∀ᶠ (N : ℕ) in Filter.atTop, LiuMainPanSignedResidualBoundAt (liuLogarithmicIntegral kappa) N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C3 u v) : ∀ᶠ (N : ℕ) in Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}, |liuSelbergRemainder (liuLogarithmicIntegral kappa) N epsilon (liuSelbergOptimalLambda N epsilon)| ≤ (C1 + C2 + C3) * ↑N / Real.log ↑N ^ A + 15 * liuLogarithmicIntegralUpperConstant kappa * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2

The three Pan source-family bounds give the explicit Selberg remainder bound for the optimal coefficients along the even filter.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuSelbergOptimalSwitchedCount_le_even_of_sourceInputs (kappa epsilon A B C1 C2 C3 : ℝ) (u v : ℕ) (hκ : 0 ≤ kappa) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hB : 0 ≤ B) (hI : ∀ᶠ (N : ℕ) in Filter.atTop, LiuMainPanTypeIPieceBoundAt N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C1 u) (hII : ∀ᶠ (N : ℕ) in Filter.atTop, LiuMainPanTypeIIPieceBoundAt N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C2 u v) (hresidual : ∀ᶠ (N : ℕ) in Filter.atTop, LiuMainPanSignedResidualBoundAt (liuLogarithmicIntegral kappa) N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C3 u v) : ∀ᶠ (N : ℕ) in Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}, liuSelbergSwitchedCount N epsilon (liuSelbergOptimalLambda N epsilon) ≤ 3.94033 * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 + ((C1 + C2 + C3) * ↑N / Real.log ↑N ^ A + 15 * liuLogarithmicIntegralUpperConstant kappa * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2)

Liu's switched Selberg count has the printed main term plus the explicit remainder bound along the even filter.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuSelbergOptimalSquareCount_le_even_of_sourceInputs (kappa epsilon A B C1 C2 C3 : ℝ) (u v : ℕ) (hκ : 0 ≤ kappa) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hB : 0 ≤ B) (hI : ∀ᶠ (N : ℕ) in Filter.atTop, LiuMainPanTypeIPieceBoundAt N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C1 u) (hII : ∀ᶠ (N : ℕ) in Filter.atTop, LiuMainPanTypeIIPieceBoundAt N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C2 u v) (hresidual : ∀ᶠ (N : ℕ) in Filter.atTop, LiuMainPanSignedResidualBoundAt (liuLogarithmicIntegral kappa) N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C3 u v) : ∀ᶠ (N : ℕ) in Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}, liuSelbergSquareCount N epsilon (liuSelbergOptimalLambda N epsilon) ≤ 3.94033 * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 + ((C1 + C2 + C3) * ↑N / Real.log ↑N ^ A + 15 * liuLogarithmicIntegralUpperConstant kappa * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2)

Liu's original squared-divisor Selberg count has the same bound along the even filter.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanCanonicalCoprimeTheorem.eventually_abs_liuSelbergOptimalRemainder_le_even (hPan : LiuPanCanonicalCoprimeTheorem) (epsilon A : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}, |liuSelbergRemainder (liuLogarithmicIntegral 2) N epsilon (liuSelbergOptimalLambda N epsilon)| ≤ C * ↑N / Real.log ↑N ^ A

The canonical coprime consumer interface gives arbitrary logarithmic saving for the actual optimal Selberg remainder along the even filter.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanCanonicalCoprimeTheorem.eventually_liuSelbergOptimalSwitchedCount_le_even (hPan : LiuPanCanonicalCoprimeTheorem) (epsilon A : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}, liuSelbergSwitchedCount N epsilon (liuSelbergOptimalLambda N epsilon) ≤ 3.94033 * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 + C * ↑N / Real.log ↑N ^ A

The canonical coprime consumer interface and the proved optimal main-term estimate bound Liu's switched Selberg count without componentwise Pan inputs.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanCanonicalCoprimeTheorem.eventually_liuSelbergOptimalSquareCount_le_even (hPan : LiuPanCanonicalCoprimeTheorem) (epsilon A : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}, liuSelbergSquareCount N epsilon (liuSelbergOptimalLambda N epsilon) ≤ 3.94033 * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 + C * ↑N / Real.log ↑N ^ A

The same canonical consumer bound holds for Liu's original squared-divisor Selberg count by the exact square expansion.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingTheorem.eventually_abs_liuSelbergOptimalRemainder_le_even (hPan : LiuPanWangDingTheorem) (epsilon A : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}, |liuSelbergRemainder (liuLogarithmicIntegral 2) N epsilon (liuSelbergOptimalLambda N epsilon)| ≤ C * ↑N / Real.log ↑N ^ A

Backward-compatible optimal-remainder wrapper for the stronger canonical Pan--Wang--Ding endpoint contract.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingTheorem.eventually_liuSelbergOptimalSwitchedCount_le_even (hPan : LiuPanWangDingTheorem) (epsilon A : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}, liuSelbergSwitchedCount N epsilon (liuSelbergOptimalLambda N epsilon) ≤ 3.94033 * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 + C * ↑N / Real.log ↑N ^ A

Backward-compatible switched-count wrapper for the stronger canonical Pan--Wang--Ding endpoint contract.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingTheorem.eventually_liuSelbergOptimalSquareCount_le_even (hPan : LiuPanWangDingTheorem) (epsilon A : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}, liuSelbergSquareCount N epsilon (liuSelbergOptimalLambda N epsilon) ≤ 3.94033 * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 + C * ↑N / Real.log ↑N ^ A

Backward-compatible square-count wrapper for the stronger canonical Pan--Wang--Ding endpoint contract.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingCorollary230.eventually_abs_liuSelbergOptimalRemainder_le_even (hPan : LiuPanWangDingCorollary230) (epsilon A : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}, |liuSelbergRemainder (liuLogarithmicIntegral 2) N epsilon (liuSelbergOptimalLambda N epsilon)| ≤ C * ↑N / Real.log ↑N ^ A

Source-faithful optimal-remainder wrapper from literal Corollary (2.30).

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingCorollary230.eventually_liuSelbergOptimalSwitchedCount_le_even (hPan : LiuPanWangDingCorollary230) (epsilon A : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}, liuSelbergSwitchedCount N epsilon (liuSelbergOptimalLambda N epsilon) ≤ 3.94033 * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 + C * ↑N / Real.log ↑N ^ A

Source-faithful switched-count wrapper from literal Corollary (2.30).

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingCorollary230.eventually_liuSelbergOptimalSquareCount_le_even (hPan : LiuPanWangDingCorollary230) (epsilon A : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}, liuSelbergSquareCount N epsilon (liuSelbergOptimalLambda N epsilon) ≤ 3.94033 * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 + C * ↑N / Real.log ↑N ^ A

Source-faithful square-count wrapper from literal Corollary (2.30).