Liu's lambda-pair Selberg remainder

This module represents the actual signed double sum in Liu's eqn-r. Its lambda coefficients are supported on divisors of the paper modulus at the paper's N^(1/4-epsilon/2) cutoff. Grouping pairs by their least common multiple bounds the signed remainder by the already verified 3^omega(d) full-distribution majorant.

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

The support and size conditions on Liu's Selberg coefficients needed for the remainder bound. No normalization at d = 1 is needed.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuSelbergLambdaAdmissible N epsilon lambda = ((∀ (d : ℕ), lambda d ≠ 0 → d ∣ MathlibNt.SieveTheory.LiuWeight.liuPaperQModulus N epsilon ∧ d ≤ MathlibNt.SieveTheory.LiuWeight.paperQSourceCutoff N epsilon) ∧ ∀ (d : ℕ), |lambda d| ≤ 1)

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergLambdaSourceCarrier (N : ℕ) (epsilon : ℝ) : Finset ℕ

The finite source carrier forced by admissibility.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergLambdaSourceCarrier N epsilon = {d ∈ (MathlibNt.SieveTheory.LiuWeight.liuPaperQModulus N epsilon).divisors | d ≤ MathlibNt.SieveTheory.LiuWeight.paperQSourceCutoff N epsilon}

theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQModulus_squarefree (N : ℕ) (epsilon : ℝ) : Squarefree (liuPaperQModulus N epsilon)

theorem MathlibNt.SieveTheory.LiuWeight.mem_liuSelbergLambdaSourceCarrier {N d : ℕ} {epsilon : ℝ} : d ∈ liuSelbergLambdaSourceCarrier N epsilon ↔ d ∣ liuPaperQModulus N epsilon ∧ d ≤ paperQSourceCutoff N epsilon

theorem MathlibNt.SieveTheory.LiuWeight.LiuSelbergLambdaAdmissible.support_dvd {N d : ℕ} {epsilon : ℝ} {lambda : ℕ → ℝ} (hlambda : LiuSelbergLambdaAdmissible N epsilon lambda) (hd : lambda d ≠ 0) : d ∣ liuPaperQModulus N epsilon

theorem MathlibNt.SieveTheory.LiuWeight.LiuSelbergLambdaAdmissible.support_le {N d : ℕ} {epsilon : ℝ} {lambda : ℕ → ℝ} (hlambda : LiuSelbergLambdaAdmissible N epsilon lambda) (hd : lambda d ≠ 0) : d ≤ paperQSourceCutoff N epsilon

theorem MathlibNt.SieveTheory.LiuWeight.LiuSelbergLambdaAdmissible.abs_le_one {N : ℕ} {epsilon : ℝ} {lambda : ℕ → ℝ} (hlambda : LiuSelbergLambdaAdmissible N epsilon lambda) (d : ℕ) : |lambda d| ≤ 1

theorem MathlibNt.SieveTheory.LiuWeight.LiuSelbergLambdaAdmissible.eq_zero_of_not_mem_sourceCarrier {N d : ℕ} {epsilon : ℝ} {lambda : ℕ → ℝ} (hlambda : LiuSelbergLambdaAdmissible N epsilon lambda) (hd : d ∉ liuSelbergLambdaSourceCarrier N epsilon) : lambda d = 0

Admissibility proves that the finite carrier loses no nonzero coefficient.

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

Liu's Selberg expression after expanding the square and interchanging the finite sums. The inner term is the actual weighted prime count in the progression a * p ≡ N (mod lcm d₁ d₂).

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergSwitchedCount N epsilon lambda = ∑ d1 ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergLambdaSourceCarrier N epsilon, ∑ d2 ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergLambdaSourceCarrier N epsilon, lambda d1 * lambda d2 * ∑ a ∈ Finset.range (N + 1), MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N) a * ↑(AnalyticNumberTheory.Sieve.primesInAPBelow N a (d1.lcm d2) (N % d1.lcm d2))

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

The main term paired with liuSelbergSwitchedCount for an arbitrary main-term model.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergMainTerm main N epsilon lambda = ∑ d1 ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergLambdaSourceCarrier N epsilon, ∑ d2 ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergLambdaSourceCarrier N epsilon, lambda d1 * lambda d2 * (1 / ↑(d1.lcm d2).totient * ∑ a ∈ Finset.range (N + 1), MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N) a * main (↑N / ↑a))

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

The actual lambda-pair Selberg remainder from Liu's eqn-r, represented on the finite carrier justified by LiuSelbergLambdaAdmissible.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergRemainder main N epsilon lambda = ∑ d1 ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergLambdaSourceCarrier N epsilon, ∑ d2 ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergLambdaSourceCarrier N epsilon, lambda d1 * lambda d2 * MathlibNt.SieveTheory.LiuWeight.liuMainFullSum main N N (d1.lcm d2) (N % d1.lcm d2) (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N))

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergSwitchedCount_eq_mainTerm_add_remainder (main : ℝ → ℝ) (N : ℕ) (epsilon : ℝ) (lambda : ℕ → ℝ) : liuSelbergSwitchedCount N epsilon lambda = liuSelbergMainTerm main N epsilon lambda + liuSelbergRemainder main N epsilon lambda

Exact finite decomposition of the switched Selberg count into its chosen main term and the actual signed remainder.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergSwitchedCount_eq_logarithmicIntegralMainTerm_add_remainder (kappa : ℝ) (N : ℕ) (epsilon : ℝ) (lambda : ℕ → ℝ) : liuSelbergSwitchedCount N epsilon lambda = liuSelbergMainTerm (liuLogarithmicIntegral kappa) N epsilon lambda + liuSelbergRemainder (liuLogarithmicIntegral kappa) N epsilon lambda

Source-facing specialization of the exact decomposition to Liu's genuine normalized logarithmic-integral family.

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

Liu's original finite Selberg expression before expanding the square.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergSquareCount N epsilon lambda = ∑ a ∈ Finset.range (N + 1), MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N) a * ∑ p ∈ Finset.range (N + 1) with Nat.Prime p ∧ a * p ≤ N, (∑ d ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergLambdaSourceCarrier N epsilon with d ∣ N - a * p, lambda d) ^ 2

theorem MathlibNt.SieveTheory.LiuWeight.primesInAPBelow_mod_eq_card_dvd_complement (N a q : ℕ) : ↑(AnalyticNumberTheory.Sieve.primesInAPBelow N a q (N % q)) = ↑{p ∈ {p ∈ Finset.range (N + 1) | Nat.Prime p ∧ a * p ≤ N} | q ∣ N - a * p}.card

At the canonical residue, the AP convention on a * p is exactly divisibility of the natural-number complement.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergSquareCount_eq_switchedCount (N : ℕ) (epsilon : ℝ) (lambda : ℕ → ℝ) : liuSelbergSquareCount N epsilon lambda = liuSelbergSwitchedCount N epsilon lambda

Finite square expansion and interchange: Liu's original squared-divisor expression equals the switched lambda-pair AP count.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergSquareCount_eq_logarithmicIntegralMainTerm_add_remainder (kappa : ℝ) (N : ℕ) (epsilon : ℝ) (lambda : ℕ → ℝ) : liuSelbergSquareCount N epsilon lambda = liuSelbergMainTerm (liuLogarithmicIntegral kappa) N epsilon lambda + liuSelbergRemainder (liuLogarithmicIntegral kappa) N epsilon lambda

Source-facing exact decomposition of Liu's original squared-divisor expression.

def MathlibNt.SieveTheory.LiuWeight.LiuSelbergMainTermUpperBound (kappa : ℝ) (N : ℕ) (epsilon : ℝ) (lambda : ℕ → ℝ) : Prop

The unproved numerical main-term estimate printed in Liu's source. This is a transparent proposition, not an asserted analytic theorem.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuSelbergMainTermUpperBound kappa N epsilon lambda = (MathlibNt.SieveTheory.LiuWeight.liuSelbergMainTerm (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral kappa) N epsilon lambda ≤ 3.94033 * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

theorem MathlibNt.SieveTheory.LiuWeight.liuSelberg_lcm_dvd_modulus_and_squarefree {N d1 d2 : ℕ} {epsilon : ℝ} (hd1 : d1 ∈ liuSelbergLambdaSourceCarrier N epsilon) (hd2 : d2 ∈ liuSelbergLambdaSourceCarrier N epsilon) : d1.lcm d2 ∣ liuPaperQModulus N epsilon ∧ Squarefree (d1.lcm d2)

Supported pairs have lcm dividing the squarefree paper modulus; in particular the lcm itself is squarefree.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelberg_lcm_le_mul {d1 d2 : ℕ} (hd1 : 0 < d1) (hd2 : 0 < d2) : d1.lcm d2 ≤ d1 * d2

The elementary lcm-product inequality used in the source cutoff.

theorem MathlibNt.SieveTheory.LiuWeight.paperQSourceCutoff_mul_le_liuSourceDEpsilon (N d1 d2 : ℕ) (epsilon : ℝ) (hN : 1 ≤ N) (hd1 : d1 ≤ paperQSourceCutoff N epsilon) (hd2 : d2 ≤ paperQSourceCutoff N epsilon) : d1 * d2 ≤ liuSourceDEpsilon N epsilon

Multiplying two source-cutoff divisors doubles the exponent exactly.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelberg_lcm_le_sourceDEpsilon_of_mem_sourceCarrier {N d1 d2 : ℕ} {epsilon : ℝ} (hN : 1 ≤ N) (hd1 : d1 ∈ liuSelbergLambdaSourceCarrier N epsilon) (hd2 : d2 ∈ liuSelbergLambdaSourceCarrier N epsilon) : d1.lcm d2 ≤ liuSourceDEpsilon N epsilon

Every pair in the source carrier has lcm inside Liu's eqn-r divisor cutoff. This records both lcm ≤ d1*d2 and the doubled-exponent estimate.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuSelbergRemainder_le_fullDistributionMajorant (main : ℝ → ℝ) (N : ℕ) (epsilon : ℝ) (lambda : ℕ → ℝ) (hN : 1 ≤ N) (hlambda : LiuSelbergLambdaAdmissible N epsilon lambda) : |liuSelbergRemainder main N epsilon lambda| ≤ liuPaperQSourceFullDistributionMajorant main N epsilon

The actual signed lambda-pair remainder is bounded by Liu's exact 3^omega(d) full-distribution majorant.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanCanonicalCoprimeTheorem.eventually_abs_liuSelbergRemainder_le (hPan : LiuPanCanonicalCoprimeTheorem) (l : Filter ℕ) (hl : l ≤ Filter.atTop) (epsilon A : ℝ) (lambda : ℕ → ℕ → ℝ) (hepsilon : 0 < epsilon) (hA : 0 < A) (hlambda : ∀ᶠ (N : ℕ) in l, LiuSelbergLambdaAdmissible N epsilon (lambda N)) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in l, |liuSelbergRemainder (liuLogarithmicIntegral 2) N epsilon (lambda N)| ≤ C * ↑N / Real.log ↑N ^ A

The canonical coprime consumer interface bounds the actual signed Selberg remainder for every eventually admissible coefficient family.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingTheorem.eventually_abs_liuSelbergRemainder_le (hPan : LiuPanWangDingTheorem) (l : Filter ℕ) (hl : l ≤ Filter.atTop) (epsilon A : ℝ) (lambda : ℕ → ℕ → ℝ) (hepsilon : 0 < epsilon) (hA : 0 < A) (hlambda : ∀ᶠ (N : ℕ) in l, LiuSelbergLambdaAdmissible N epsilon (lambda N)) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in l, |liuSelbergRemainder (liuLogarithmicIntegral 2) N epsilon (lambda N)| ≤ C * ↑N / Real.log ↑N ^ A

Backward-compatible remainder wrapper for the stronger canonical contract.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingCorollary230.eventually_abs_liuSelbergRemainder_le (hPan : LiuPanWangDingCorollary230) (l : Filter ℕ) (hl : l ≤ Filter.atTop) (epsilon A : ℝ) (lambda : ℕ → ℕ → ℝ) (hepsilon : 0 < epsilon) (hA : 0 < A) (hlambda : ∀ᶠ (N : ℕ) in l, LiuSelbergLambdaAdmissible N epsilon (lambda N)) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in l, |liuSelbergRemainder (liuLogarithmicIntegral 2) N epsilon (lambda N)| ≤ C * ↑N / Real.log ↑N ^ A

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

theorem MathlibNt.SieveTheory.LiuWeight.eventually_abs_liuSelbergRemainder_liuLogarithmicIntegral_le_of_sourceInputs (kappa epsilon A B C1 C2 C3 : ℝ) (u v : ℕ) (lambda : ℕ → ℕ → ℝ) (hepsilon : 0 < epsilon) (hB : 0 ≤ B) (hlambda : ∀ᶠ (N : ℕ) in Filter.atTop, LiuSelbergLambdaAdmissible N epsilon (lambda N)) (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, |liuSelbergRemainder (liuLogarithmicIntegral kappa) N epsilon (lambda N)| ≤ (C1 + C2 + C3) * ↑N / Real.log ↑N ^ A + 15 * liuLogarithmicIntegralUpperConstant kappa * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2

Eventual bound for the actual Liu remainder. The lambda admissibility and the three source-family analytic estimates remain separate explicit inputs.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuSelbergSwitchedCount_le_of_mainTermUpperBound_sourceInputs (kappa epsilon A B C1 C2 C3 : ℝ) (u v : ℕ) (lambda : ℕ → ℕ → ℝ) (hepsilon : 0 < epsilon) (hB : 0 ≤ B) (hmain : ∀ᶠ (N : ℕ) in Filter.atTop, LiuSelbergMainTermUpperBound kappa N epsilon (lambda N)) (hlambda : ∀ᶠ (N : ℕ) in Filter.atTop, LiuSelbergLambdaAdmissible N epsilon (lambda N)) (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, liuSelbergSwitchedCount N epsilon (lambda N) ≤ 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)

Conditional eventual bound for Liu's switched Selberg count. The numerical main-term estimate, lambda admissibility, and the three source-family analytic estimates are all retained as explicit inputs.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuSelbergSquareCount_le_of_mainTermUpperBound_sourceInputs (kappa epsilon A B C1 C2 C3 : ℝ) (u v : ℕ) (lambda : ℕ → ℕ → ℝ) (hepsilon : 0 < epsilon) (hB : 0 ≤ B) (hmain : ∀ᶠ (N : ℕ) in Filter.atTop, LiuSelbergMainTermUpperBound kappa N epsilon (lambda N)) (hlambda : ∀ᶠ (N : ℕ) in Filter.atTop, LiuSelbergLambdaAdmissible N epsilon (lambda N)) (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, liuSelbergSquareCount N epsilon (lambda N) ≤ 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)

Conditional eventual bound for Liu's original squared-divisor Selberg expression, obtained from the exact square expansion and switched-count bound.