Liu's eqn-r distribution majorant

This module formalizes the finite distribution majorant displayed in Liu (2022), eqn-r, for an arbitrary main-term model. The source expression is a sum of termwise absolute inner errors, not the absolute value of a signed outer sum. The coprime estimate remains an explicit analytic proposition; the non-coprime endpoint is supplied by the genuine logarithmic-integral development.

No Selberg remainder R, Pan Type I/II estimate, or signed-main-term estimate is asserted here.

Main-parametric inner sums

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuMainFullSum (main : ℝ → ℝ) (Y X d l : ℕ) (f : ℕ → ℝ) : ℝ

The unrestricted finite inner distribution sum for an arbitrary main-term model.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainFullSum main Y X d l f = ∑ a ∈ Finset.range (X + 1), f a * MathlibNt.SieveTheory.LiuWeight.liuScaledAPError main Y a d l

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuMainCoprimeSum (main : ℝ → ℝ) (Y X d l : ℕ) (f : ℕ → ℝ) : ℝ

The coprime finite inner distribution sum for an arbitrary main-term model.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainCoprimeSum main Y X d l f = ∑ a ∈ Finset.range (X + 1), if a.Coprime d then f a * MathlibNt.SieveTheory.LiuWeight.liuScaledAPError main Y a d l else 0

theorem MathlibNt.SieveTheory.LiuWeight.liuMainFullSum_eq_coprime_add_noncoprime (main : ℝ → ℝ) (Y X d l : ℕ) (f : ℕ → ℝ) : liuMainFullSum main Y X d l f = liuMainCoprimeSum main Y X d l f + liuMainNoncoprimeSum main Y X d l f

Exact finite partition of the unrestricted sum into its coprime and non-coprime parts.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainFullSum_proxy (Y X d l : ℕ) (f : ℕ → ℝ) : liuMainFullSum AnalyticNumberTheory.Sieve.logarithmicIntegral Y X d l f = AnalyticNumberTheory.Sieve.panDistributionFullSum Y X d l f

Proxy compatibility. The unrestricted main-parametric sum specializes to ANT's historical x / log x Pan object. This is not a true-li claim.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainCoprimeSum_proxy (Y X d l : ℕ) (f : ℕ → ℝ) : liuMainCoprimeSum AnalyticNumberTheory.Sieve.logarithmicIntegral Y X d l f = AnalyticNumberTheory.Sieve.panDistributionSum Y X d l f

Proxy compatibility. The coprime main-parametric sum specializes to ANT's historical x / log x Pan object. This is not a true-li claim.

Neutral signed weighted sums

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceFullSignedWeightedSum (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) : ℝ

The full signed weighted sum with the auxiliary cutoff D₂. It is a finite algebraic object and is not Liu's Selberg remainder R.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceFullSignedWeightedSum main N ε = ∑ d ∈ (MathlibNt.SieveTheory.LiuWeight.liuPaperQModulus N ε).divisors with d ≤ MathlibNt.SieveTheory.LiuWeight.liuSourceD2 N, 3 ^ d.primeFactors.card * MathlibNt.SieveTheory.LiuWeight.liuMainFullSum main N N d (N % d) (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N))

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceCoprimeSignedWeightedSum (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) : ℝ

The coprime signed weighted sum with the auxiliary cutoff D₂.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceCoprimeSignedWeightedSum main N ε = ∑ d ∈ (MathlibNt.SieveTheory.LiuWeight.liuPaperQModulus N ε).divisors with d ≤ MathlibNt.SieveTheory.LiuWeight.liuSourceD2 N, 3 ^ d.primeFactors.card * MathlibNt.SieveTheory.LiuWeight.liuMainCoprimeSum main N N d (N % d) (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N))

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceNoncoprimeSignedWeightedSum (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) : ℝ

The non-coprime signed weighted sum with the auxiliary cutoff D₂.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceNoncoprimeSignedWeightedSum main N ε = ∑ d ∈ (MathlibNt.SieveTheory.LiuWeight.liuPaperQModulus N ε).divisors with d ≤ MathlibNt.SieveTheory.LiuWeight.liuSourceD2 N, 3 ^ d.primeFactors.card * MathlibNt.SieveTheory.LiuWeight.liuMainNoncoprimeSum main N N d (N % d) (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N))

theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceFullSignedWeightedSum_eq_coprime_add_noncoprime (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) : liuPaperQSourceFullSignedWeightedSum main N ε = liuPaperQSourceCoprimeSignedWeightedSum main N ε + liuPaperQSourceNoncoprimeSignedWeightedSum main N ε

Exact partition of the neutral signed weighted sum.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPaperQSourceNoncoprimeSignedWeightedSum_le_majorant (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) : |liuPaperQSourceNoncoprimeSignedWeightedSum main N ε| ≤ liuPaperQSourceR1Majorant main N ε

The neutral non-coprime signed weighted sum is bounded by the existing termwise R₁ majorant.

The source eqn-r absolute majorants

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceDEpsilon (N : ℕ) (ε : ℝ) : ℕ

Liu's source divisor cutoff ⌊N^(1/2-ε)⌋ from eqn-r.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceDEpsilon N ε = ⌊↑N ^ (1 / 2 - ε)⌋₊

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceDEpsilon_le_liuSourceD2 (N : ℕ) (ε : ℝ) (hN : 1 ≤ N) (hε : 0 ≤ ε) : liuSourceDEpsilon N ε ≤ liuSourceD2 N

For nonnegative ε, the source cutoff Dε is no larger than the auxiliary cutoff D₂ = ⌊N^(1/2)⌋.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceFullDistributionMajorant (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) : ℝ

The exact full distribution majorant on the left side of Liu's eqn-r: the weight 3^ω(d) multiplies the absolute value of each inner full error.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceFullDistributionMajorant main N ε = ∑ d ∈ (MathlibNt.SieveTheory.LiuWeight.liuPaperQModulus N ε).divisors with d ≤ MathlibNt.SieveTheory.LiuWeight.liuSourceDEpsilon N ε, 3 ^ d.primeFactors.card * |MathlibNt.SieveTheory.LiuWeight.liuMainFullSum main N N d (N % d) (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N))|

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceCoprimeDistributionMajorant (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) : ℝ

The corresponding termwise absolute coprime distribution majorant.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceCoprimeDistributionMajorant main N ε = ∑ d ∈ (MathlibNt.SieveTheory.LiuWeight.liuPaperQModulus N ε).divisors with d ≤ MathlibNt.SieveTheory.LiuWeight.liuSourceDEpsilon N ε, 3 ^ d.primeFactors.card * |MathlibNt.SieveTheory.LiuWeight.liuMainCoprimeSum main N N d (N % d) (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N))|

theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceFullDistributionMajorant_le_coprime_add_r1 (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) (hN : 1 ≤ N) (hε : 0 ≤ ε) : liuPaperQSourceFullDistributionMajorant main N ε ≤ liuPaperQSourceCoprimeDistributionMajorant main N ε + liuPaperQSourceR1Majorant main N ε

Termwise triangle inequality followed by the nonnegative extension from Dε to D₂ bounds the exact full eqn-r distribution majorant by its coprime part and the established non-coprime majorant.

Conditional coprime input and genuine-integral endpoint

def MathlibNt.SieveTheory.LiuWeight.LiuPaperQCoprimeRBound (main : ℝ → ℝ) (N : ℕ) (ε A C : ℝ) : Prop

The remaining coprime Pan estimate for Liu's exact eqn-r absolute majorant. This proposition transparently contains the inverse-log inequality used by the outer bound.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPaperQCoprimeRBound main N ε A C = (MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceCoprimeDistributionMajorant main N ε ≤ C * ↑N / Real.log ↑N ^ A)

theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceFullDistributionMajorant_liuLogarithmicIntegral_le (κ : ℝ) (N : ℕ) (ε A Cpan : ℝ) (hN : 8 ≤ N) (hε : 0 ≤ ε) (hpan : LiuPaperQCoprimeRBound (liuLogarithmicIntegral κ) N ε A Cpan) : liuPaperQSourceFullDistributionMajorant (liuLogarithmicIntegral κ) N ε ≤ Cpan * ↑N / Real.log ↑N ^ A + 15 * liuLogarithmicIntegralUpperConstant κ * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2

Liu's exact eqn-r distribution majorant for the genuine normalized logarithmic integral, conditional only on the explicitly retained coprime inverse-log estimate. The N^(9/10) log(N)^2 term is not absorbed.