Liu's finite p₁p₂ weight

This module formalizes the finite characteristic function in Liu (2022), eqn-adef. The square-root cutoff is stored without rounding as p₁ * p₂ ^ 2 ≤ N; liuSizeCondition_iff_real_sqrt identifies it with the paper's real square-root inequality.

The exact identity below rewrites the non-coprime majorant as a finite sum over the unique admissible pair with p₁ ∣ d. The signed non-coprime sum is only bounded by that expression. No outer d ∣ Q weighted asymptotic estimate is asserted here.

def MathlibNt.SieveTheory.LiuWeight.LiuPairConditions (N z y p₁ p₂ : ℕ) : Prop

The arithmetic conditions on the ordered prime pair in Liu's eqn-adef. The last condition is the lossless natural-number form of p₂ ≤ sqrt (N / p₁).

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPairConditions N z y p₁ p₂ = (Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ z < p₁ ∧ p₁ ≤ y ∧ y < p₂ ∧ p₁ * p₂ ^ 2 ≤ N)

@[instance_reducible]

instance MathlibNt.SieveTheory.LiuWeight.instDecidableLiuPairConditions (N z y p₁ p₂ : ℕ) : Decidable (LiuPairConditions N z y p₁ p₂)

Equations

• MathlibNt.SieveTheory.LiuWeight.instDecidableLiuPairConditions N z y p₁ p₂ = id inferInstance

theorem MathlibNt.SieveTheory.LiuWeight.liuPairConditions_factors_le {N z y p₁ p₂ : ℕ} (h : LiuPairConditions N z y p₁ p₂) : p₁ ≤ N ∧ p₂ ≤ N

Each factor in an admissible pair is at most N, so range (N + 1) contains every representation.

theorem MathlibNt.SieveTheory.LiuWeight.liuSizeCondition_iff_real_sqrt {N p₁ p₂ : ℕ} (hp₁ : 0 < p₁) : p₁ * p₂ ^ 2 ≤ N ↔ ↑p₂ ≤ √(↑N / ↑p₁)

The root-free cutoff is exactly the intended real square-root cutoff when p₁ is positive.

def MathlibNt.SieveTheory.LiuWeight.liuWeightPairs (N z y : ℕ) : Finset (ℕ × ℕ)

The finite set of ordered prime pairs occurring in Liu's weight.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N z y = {p ∈ (Finset.range (N + 1)).product (Finset.range (N + 1)) | MathlibNt.SieveTheory.LiuWeight.LiuPairConditions N z y p.1 p.2}

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.mem_liuWeightPairs {N z y p₁ p₂ : ℕ} : (p₁, p₂) ∈ liuWeightPairs N z y ↔ LiuPairConditions N z y p₁ p₂

def MathlibNt.SieveTheory.LiuWeight.LiuWeightSupport (N z y a : ℕ) : Prop

A visible finite witness that a has an admissible p₁p₂ representation.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuWeightSupport N z y a = ∃ p ∈ MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N z y, p.1 * p.2 = a

@[instance_reducible]

instance MathlibNt.SieveTheory.LiuWeight.instDecidableLiuWeightSupport (N z y a : ℕ) : Decidable (LiuWeightSupport N z y a)

Equations

• MathlibNt.SieveTheory.LiuWeight.instDecidableLiuWeightSupport N z y a = id inferInstance

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightSupport_iff {N z y a : ℕ} : LiuWeightSupport N z y a ↔ ∃ (p₁ : ℕ) (p₂ : ℕ), LiuPairConditions N z y p₁ p₂ ∧ a = p₁ * p₂

theorem MathlibNt.SieveTheory.LiuWeight.liuPairConditions_unique {N z y p₁ p₂ q₁ q₂ : ℕ} (hp : LiuPairConditions N z y p₁ p₂) (hq : LiuPairConditions N z y q₁ q₂) (heq : p₁ * p₂ = q₁ * q₂) : p₁ = q₁ ∧ p₂ = q₂

Admissible ordered prime representations are unique. Thus the characteristic function below never silently collapses multiplicities.

def MathlibNt.SieveTheory.LiuWeight.liuWeight (N z y a : ℕ) : ℝ

Liu's transparent finite characteristic weight: one exactly when the finite witness set contains an admissible pair whose product is a.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuWeight N z y a = if MathlibNt.SieveTheory.LiuWeight.LiuWeightSupport N z y a then 1 else 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuWeight_eq_one_iff {N z y a : ℕ} : liuWeight N z y a = 1 ↔ LiuWeightSupport N z y a

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuWeight_eq_zero_iff {N z y a : ℕ} : liuWeight N z y a = 0 ↔ ¬LiuWeightSupport N z y a

theorem MathlibNt.SieveTheory.LiuWeight.liuWeight_nonneg (N z y a : ℕ) : 0 ≤ liuWeight N z y a

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuWeight (N z y a : ℕ) : |liuWeight N z y a| = liuWeight N z y a

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuWeight_le_one (N z y a : ℕ) : |liuWeight N z y a| ≤ 1

Liu's source is a 0/1 indicator, hence satisfies Pan's coefficient bound.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuOrderedTriplePairMultiplicity (N z y p₁ p₂ p₃ : ℕ) : ℝ

The number of Liu source pairs obtained from a strict ordered triple by pairing its medium prime with either large prime.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuOrderedTriplePairMultiplicity N z y p₁ p₂ p₃ = MathlibNt.SieveTheory.LiuWeight.liuWeight N z y (p₁ * p₂) + MathlibNt.SieveTheory.LiuWeight.liuWeight N z y (p₁ * p₃)

theorem MathlibNt.SieveTheory.LiuWeight.liuOrderedTriplePairMultiplicity_eq_one_add_indicator {N z y p₁ p₂ p₃ : ℕ} (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) (hp₃ : Nat.Prime p₃) (hzp₁ : z < p₁) (hp₁y : p₁ ≤ y) (hyp₂ : y < p₂) (hp₂p₃ : p₂ < p₃) (hprod : p₁ * p₂ * p₃ ≤ N) : liuOrderedTriplePairMultiplicity N z y p₁ p₂ p₃ = 1 + if p₁ * p₃ ^ 2 ≤ N then 1 else 0

A strict ordered triple contributes once through its smaller large prime, and a second time exactly when the larger prime also satisfies Liu's square cutoff. Thus the source weight has multiplicity one or two, not uniformly two.

theorem MathlibNt.SieveTheory.LiuWeight.liuOrderedTriplePairMultiplicity_one_witness : liuOrderedTriplePairMultiplicity 1000 1 9 3 11 23 = 1

A concrete strict ordered triple for which Liu's source multiplicity is one. This is the local obstruction to dividing the source count by two.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightSupport_le {N z y a : ℕ} (ha : LiuWeightSupport N z y a) : a ≤ N

The exact finite size consequence retained in place of an unproved natural/real N^(2/3) floor bridge.

theorem MathlibNt.SieveTheory.LiuWeight.sum_liuWeightSupport_filter_eq_sum_pairs {R : Type u_1} [AddCommMonoid R] (N z y X : ℕ) (E : ℕ → Prop) [DecidablePred E] (F : ℕ → R) : ∑ a ∈ Finset.range (X + 1) with LiuWeightSupport N z y a ∧ E a, F a = ∑ p ∈ liuWeightPairs N z y with p.1 * p.2 ≤ X ∧ E (p.1 * p.2), F (p.1 * p.2)

Transport an arbitrary filtered kernel through the unique prime-pair product. The truncation is independent of N; no sign condition is imposed on the kernel.

theorem MathlibNt.SieveTheory.LiuWeight.sum_liuWeight_mul_eq_sum_pairs_of_support (N z y : ℕ) (F : ℕ → ℝ) : ∑ a ∈ Finset.range (N + 1), liuWeight N z y a * F a = ∑ p ∈ liuWeightPairs N z y, F (p.1 * p.2)

Reindex an arbitrary sum against Liu's characteristic source by its unique admissible ordered prime pair.

theorem MathlibNt.SieveTheory.LiuWeight.product_cube_le_sq {N p₁ p₂ : ℕ} (hp₁p₂ : p₁ ≤ p₂) (hsize : p₁ * p₂ ^ 2 ≤ N) : (p₁ * p₂) ^ 3 ≤ N ^ 2

The root-free N^(2/3) calculation in its minimal natural-number form. The two hypotheses say exactly that the smaller factor is first and that the paper's square-root cutoff holds.

theorem MathlibNt.SieveTheory.LiuWeight.liuPairConditions_product_cube_le_sq {N z y p₁ p₂ : ℕ} (h : LiuPairConditions N z y p₁ p₂) : (p₁ * p₂) ^ 3 ≤ N ^ 2

Every admissible Liu pair satisfies the exact root-free support bound (p₁p₂)^3 ≤ N^2. No floor or real-power comparison is used.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightSupport_cube_le_sq {N z y a : ℕ} (ha : LiuWeightSupport N z y a) : a ^ 3 ≤ N ^ 2

Product-support form of the exact root-free N^(2/3) bound.

theorem MathlibNt.SieveTheory.LiuWeight.le_rpow_two_thirds_of_cube_le_sq {N a : ℕ} (ha : a ^ 3 ≤ N ^ 2) : ↑a ≤ ↑N ^ (2 / 3)

The root-free support inequality converts to the intended N^(2/3) real scale. It belongs to the source weight itself and is reused by both the Pan source-interval bridge and the deterministic Abel estimate.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightSupport_le_rpow_two_thirds {N z y a : ℕ} (ha : LiuWeightSupport N z y a) : ↑a ≤ ↑N ^ (2 / 3)

Every nonzero Liu source index lies below the exact two-thirds scale.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeight_support_card_le_ceil_rpow_two_thirds (N z y : ℕ) : (Finset.filter (LiuWeightSupport N z y) (Finset.Icc 1 N)).card ≤ ⌈↑N ^ (2 / 3)⌉₊ + 1

The actual indicator support has the two-thirds cardinality scale forced by Liu's product-cube condition.

theorem MathlibNt.SieveTheory.LiuWeight.sum_liuWeight_Icc_eq_support_card (N z y : ℕ) : ∑ a ∈ Finset.Icc 1 N, liuWeight N z y a = ↑(Finset.filter (LiuWeightSupport N z y) (Finset.Icc 1 N)).card

Since liuWeight is an indicator, its supported source mass is the support cardinality.

theorem MathlibNt.SieveTheory.LiuWeight.sum_liuWeight_Icc_le_ceil_rpow_two_thirds (N z y : ℕ) : ∑ a ∈ Finset.Icc 1 N, liuWeight N z y a ≤ ↑(⌈↑N ^ (2 / 3)⌉₊ + 1)

Explicit O(N^(2/3)) mass bound for the actual Liu indicator.

theorem MathlibNt.SieveTheory.LiuWeight.sum_liuWeight_Icc_le_three_mul_rpow_two_thirds (N z y : ℕ) (hN : 1 ≤ N) : ∑ a ∈ Finset.Icc 1 N, liuWeight N z y a ≤ 3 * ↑N ^ (2 / 3)

A convenient real form of the source mass estimate.

theorem MathlibNt.SieveTheory.LiuWeight.not_coprime_mul_iff_p₁_dvd {w y p₁ p₂ d : ℕ} (hwy : w ≤ y) (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) (hyp₂ : y < p₂) (hd : ∀ (r : ℕ), Nat.Prime r → r ∣ d → r ≤ w) : ¬(p₁ * p₂).Coprime d ↔ p₁ ∣ d

If every prime divisor of d is at most w, then on an admissible pair the only possible common prime divisor is p₁. The larger factor p₂ cannot divide d because w ≤ y < p₂. The modulus cutoff w is independent of the lower weight cutoff z, which does not occur in this arithmetic statement.

theorem MathlibNt.SieveTheory.LiuWeight.primesInAPBelow_mul_eq_zero_of_dvd_modulus {Y p₁ p₂ d l : ℕ} (hp₁d : p₁ ∣ d) (hp₁l : ¬p₁ ∣ l) : AnalyticNumberTheory.Sieve.primesInAPBelow Y (p₁ * p₂) d l = 0

If a factor of a divides the modulus but not the residue, then the scaled prime progression defining primesInAPBelow is empty.

theorem MathlibNt.SieveTheory.LiuWeight.primesInAPBelow_mul_mod_eq_zero {N Y p₁ p₂ d : ℕ} (hp₁d : p₁ ∣ d) (hp₁N : ¬p₁ ∣ N) : AnalyticNumberTheory.Sieve.primesInAPBelow Y (p₁ * p₂) d (N % d) = 0

The residue-count collapse at l = N % d.

Main-term-parametric finite R₁ seam

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuScaledAPError (main : ℝ → ℝ) (Y a d l : ℕ) : ℝ

The source-facing scaled AP error with an arbitrary main-term model: π(Y; a, d, l) - main(Y/a)/φ(d).

No analytic, sign, or asymptotic property of main is assumed.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuScaledAPError main Y a d l = ↑(AnalyticNumberTheory.Sieve.primesInAPBelow Y a d l) - main (↑Y / ↑a) / ↑d.totient

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

The signed non-coprime part for an arbitrary main-term model.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainNoncoprimeSum 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

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

The termwise absolute non-coprime majorant for an arbitrary main-term model.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainNoncoprimeMajorant 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

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuScaledAPError_proxy (Y a d l : ℕ) : liuScaledAPError AnalyticNumberTheory.Sieve.logarithmicIntegral Y a d l = AnalyticNumberTheory.Sieve.panDistributionError Y a d l

ANT's historical Pan error is exactly the specialization to its x / log x compatibility proxy.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainNoncoprimeSum_proxy (Y X d l : ℕ) (f : ℕ → ℝ) : liuMainNoncoprimeSum AnalyticNumberTheory.Sieve.logarithmicIntegral Y X d l f = AnalyticNumberTheory.Sieve.panDistributionNoncoprimeSum Y X d l f

The legacy signed non-coprime Pan sum is exactly the proxy specialization.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainNoncoprimeMajorant_proxy (Y X d l : ℕ) (f : ℕ → ℝ) : liuMainNoncoprimeMajorant AnalyticNumberTheory.Sieve.logarithmicIntegral Y X d l f = AnalyticNumberTheory.Sieve.panDistributionNoncoprimeMajorant Y X d l f

The legacy non-coprime Pan majorant is exactly the proxy specialization.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuMainNoncoprimeSum_le (main : ℝ → ℝ) (Y X d l : ℕ) (f : ℕ → ℝ) : |liuMainNoncoprimeSum main Y X d l f| ≤ liuMainNoncoprimeMajorant main Y X d l f

The signed non-coprime sum is bounded by its main-parametric majorant.

theorem MathlibNt.SieveTheory.LiuWeight.liuScaledAPError_mul_eq_neg_main_div_totient (main : ℝ → ℝ) {Y p₁ p₂ d l : ℕ} (hp₁d : p₁ ∣ d) (hp₁l : ¬p₁ ∣ l) : liuScaledAPError main Y (p₁ * p₂) d l = -(main (↑Y / (↑p₁ * ↑p₂)) / ↑d.totient)

When the progression count vanishes, the arbitrary-model error is exactly the negative main term.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuScaledAPError_mul_eq_abs_main_div_totient (main : ℝ → ℝ) {Y p₁ p₂ d l : ℕ} (hp₁d : p₁ ∣ d) (hp₁l : ¬p₁ ∣ l) : |liuScaledAPError main Y (p₁ * p₂) d l| = |main (↑Y / (↑p₁ * ↑p₂))| / ↑d.totient

Absolute-value form of the zero-count reduction, with no sign assumption on main.

theorem MathlibNt.SieveTheory.LiuWeight.liuScaledAPError_mul_mod_eq_neg_main_div_totient (main : ℝ → ℝ) {N Y p₁ p₂ d : ℕ} (hp₁d : p₁ ∣ d) (hp₁N : ¬p₁ ∣ N) : liuScaledAPError main Y (p₁ * p₂) d (N % d) = -(main (↑Y / (↑p₁ * ↑p₂)) / ↑d.totient)

Zero-count reduction at the canonical residue N % d.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuScaledAPError_mul_mod_eq_abs_main_div_totient (main : ℝ → ℝ) {N Y p₁ p₂ d : ℕ} (hp₁d : p₁ ∣ d) (hp₁N : ¬p₁ ∣ N) : |liuScaledAPError main Y (p₁ * p₂) d (N % d)| = |main (↑Y / (↑p₁ * ↑p₂))| / ↑d.totient

Absolute-value zero-count reduction at the canonical residue N % d.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuP₁DividesMainSum (main : ℝ → ℝ) (N z y Y X d l : ℕ) : ℝ

The paper-shaped finite pair sum for an arbitrary main-term model.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuP₁DividesMainSum main N z y Y X d l = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N z y with p.1 * p.2 ≤ X ∧ p.1 ∣ d, |MathlibNt.SieveTheory.LiuWeight.liuScaledAPError main Y (p.1 * p.2) d l|

theorem MathlibNt.SieveTheory.LiuWeight.liuMainNoncoprimeMajorant_liuWeight_eq_support_sum (main : ℝ → ℝ) (N z y Y X d l : ℕ) : liuMainNoncoprimeMajorant main Y X d l (liuWeight N z y) = ∑ a ∈ Finset.range (X + 1) with LiuWeightSupport N z y a ∧ ¬a.Coprime d, |liuScaledAPError main Y a d l|

The main-parametric majorant is exactly the supported non-coprime sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainSupportNoncoprimeSum_eq_p₁DividesMainSum (main : ℝ → ℝ) (N z w y Y X d l : ℕ) (hwy : w ≤ y) (hd : ∀ (r : ℕ), Nat.Prime r → r ∣ d → r ≤ w) : ∑ a ∈ Finset.range (X + 1) with LiuWeightSupport N z y a ∧ ¬a.Coprime d, |liuScaledAPError main Y a d l| = liuP₁DividesMainSum main N z y Y X d l

Reindex the supported non-coprime sum by the unique admissible pair.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainNoncoprimeMajorant_liuWeight_eq_p₁DividesMainSum (main : ℝ → ℝ) (N z w y Y X d l : ℕ) (hwy : w ≤ y) (hd : ∀ (r : ℕ), Nat.Prime r → r ∣ d → r ≤ w) : liuMainNoncoprimeMajorant main Y X d l (liuWeight N z y) = liuP₁DividesMainSum main N z y Y X d l

Exact finite main-parametric reduction to the p₁ ∣ d pair sum.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuMainNoncoprimeSum_liuWeight_le_p₁DividesMainSum (main : ℝ → ℝ) (N z w y Y X d l : ℕ) (hwy : w ≤ y) (hd : ∀ (r : ℕ), Nat.Prime r → r ∣ d → r ≤ w) : |liuMainNoncoprimeSum main Y X d l (liuWeight N z y)| ≤ liuP₁DividesMainSum main N z y Y X d l

The signed arbitrary-model non-coprime sum is bounded by the same pair sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuP₁DividesMainSum_mod_eq_abs_main_sum (main : ℝ → ℝ) (N z y Y X d : ℕ) (havoid : ∀ (r : ℕ), Nat.Prime r → r ∣ d → ¬r ∣ N) : liuP₁DividesMainSum main N z y Y X d (N % d) = ∑ p ∈ liuWeightPairs N z y with p.1 * p.2 ≤ X ∧ p.1 ∣ d, |main (↑Y / (↑p.1 * ↑p.2))| / ↑d.totient

At N % d, the arbitrary-model pair sum is exactly the explicit |main(Y/(p₁p₂))|/φ(d) sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainNoncoprimeMajorant_liuWeight_mod_eq_abs_main_sum (main : ℝ → ℝ) (N z w y Y X d : ℕ) (hwy : w ≤ y) (hd : ∀ (r : ℕ), Nat.Prime r → r ∣ d → r ≤ w) (havoid : ∀ (r : ℕ), Nat.Prime r → r ∣ d → ¬r ∣ N) : liuMainNoncoprimeMajorant main Y X d (N % d) (liuWeight N z y) = ∑ p ∈ liuWeightPairs N z y with p.1 * p.2 ≤ X ∧ p.1 ∣ d, |main (↑Y / (↑p.1 * ↑p.2))| / ↑d.totient

Exact per-modulus arbitrary-model majorant after the zero-count reduction.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuMainNoncoprimeSum_liuWeight_mod_le_abs_main_sum (main : ℝ → ℝ) (N z w y Y X d : ℕ) (hwy : w ≤ y) (hd : ∀ (r : ℕ), Nat.Prime r → r ∣ d → r ≤ w) (havoid : ∀ (r : ℕ), Nat.Prime r → r ∣ d → ¬r ∣ N) : |liuMainNoncoprimeSum main Y X d (N % d) (liuWeight N z y)| ≤ ∑ p ∈ liuWeightPairs N z y with p.1 * p.2 ≤ X ∧ p.1 ∣ d, |main (↑Y / (↑p.1 * ↑p.2))| / ↑d.totient

Signed per-modulus arbitrary-model sum bounded by the explicit main sum.

Compatibility-proxy specializations

theorem MathlibNt.SieveTheory.LiuWeight.panDistributionError_mul_eq_neg_li_div_totient {Y p₁ p₂ d l : ℕ} (hp₁d : p₁ ∣ d) (hp₁l : ¬p₁ ∣ l) : AnalyticNumberTheory.Sieve.panDistributionError Y (p₁ * p₂) d l = -(AnalyticNumberTheory.Sieve.logarithmicIntegral (↑Y / (↑p₁ * ↑p₂)) / ↑d.totient)

Proxy specialization. With the progression count zero, ANT's historical Pan error is the negative x / log x main term.

theorem MathlibNt.SieveTheory.LiuWeight.abs_panDistributionError_mul_eq_abs_li_div_totient {Y p₁ p₂ d l : ℕ} (hp₁d : p₁ ∣ d) (hp₁l : ¬p₁ ∣ l) : |AnalyticNumberTheory.Sieve.panDistributionError Y (p₁ * p₂) d l| = |AnalyticNumberTheory.Sieve.logarithmicIntegral (↑Y / (↑p₁ * ↑p₂))| / ↑d.totient

The sign-free consequence retains |li|; no positivity of the logarithmic integral is assumed.

theorem MathlibNt.SieveTheory.LiuWeight.panDistributionError_mul_mod_eq_neg_li_div_totient {N Y p₁ p₂ d : ℕ} (hp₁d : p₁ ∣ d) (hp₁N : ¬p₁ ∣ N) : AnalyticNumberTheory.Sieve.panDistributionError Y (p₁ * p₂) d (N % d) = -(AnalyticNumberTheory.Sieve.logarithmicIntegral (↑Y / (↑p₁ * ↑p₂)) / ↑d.totient)

Specialization of the exact signed formula to the residue N % d.

theorem MathlibNt.SieveTheory.LiuWeight.abs_panDistributionError_mul_mod_eq_abs_li_div_totient {N Y p₁ p₂ d : ℕ} (hp₁d : p₁ ∣ d) (hp₁N : ¬p₁ ∣ N) : |AnalyticNumberTheory.Sieve.panDistributionError Y (p₁ * p₂) d (N % d)| = |AnalyticNumberTheory.Sieve.logarithmicIntegral (↑Y / (↑p₁ * ↑p₂))| / ↑d.totient

Specialization of the absolute-value formula to the residue N % d.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuP₁DividesSum (N z y Y X d l : ℕ) : ℝ

The paper-shaped finite sum after the p₂ ∤ d observation.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuP₁DividesSum N z y Y X d l = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N z y with p.1 * p.2 ≤ X ∧ p.1 ∣ d, |AnalyticNumberTheory.Sieve.panDistributionError Y (p.1 * p.2) d l|

theorem MathlibNt.SieveTheory.LiuWeight.liuP₁DividesMainSum_proxy (N z y Y X d l : ℕ) : liuP₁DividesMainSum AnalyticNumberTheory.Sieve.logarithmicIntegral N z y Y X d l = liuP₁DividesSum N z y Y X d l

The legacy finite pair sum is exactly the x / log x proxy specialization.

theorem MathlibNt.SieveTheory.LiuWeight.panDistributionNoncoprimeMajorant_liuWeight_eq_support_sum (N z y Y X d l : ℕ) : AnalyticNumberTheory.Sieve.panDistributionNoncoprimeMajorant Y X d l (liuWeight N z y) = ∑ a ∈ Finset.range (X + 1) with LiuWeightSupport N z y a ∧ ¬a.Coprime d, |AnalyticNumberTheory.Sieve.panDistributionError Y a d l|

The termwise non-coprime majorant is first exactly the sum over supported products that are not coprime to d.

theorem MathlibNt.SieveTheory.LiuWeight.liuSupportNoncoprimeSum_eq_p₁DividesSum (N z w y Y X d l : ℕ) (hwy : w ≤ y) (hd : ∀ (r : ℕ), Nat.Prime r → r ∣ d → r ≤ w) : ∑ a ∈ Finset.range (X + 1) with LiuWeightSupport N z y a ∧ ¬a.Coprime d, |AnalyticNumberTheory.Sieve.panDistributionError Y a d l| = liuP₁DividesSum N z y Y X d l

Exact reindexing of the supported non-coprime sum by the unique admissible pair.

theorem MathlibNt.SieveTheory.LiuWeight.panDistributionNoncoprimeMajorant_liuWeight_eq_p₁DividesSum (N z w y Y X d l : ℕ) (hwy : w ≤ y) (hd : ∀ (r : ℕ), Nat.Prime r → r ∣ d → r ≤ w) : AnalyticNumberTheory.Sieve.panDistributionNoncoprimeMajorant Y X d l (liuWeight N z y) = liuP₁DividesSum N z y Y X d l

Exact equality for the majorant. On moduli whose prime divisors are at most the independent cutoff w ≤ y, Liu's weight with lower cutoff z has non-coprime majorant precisely equal to the finite p₁ ∣ d pair sum.

theorem MathlibNt.SieveTheory.LiuWeight.abs_panDistributionNoncoprimeSum_liuWeight_le_p₁DividesSum (N z w y Y X d l : ℕ) (hwy : w ≤ y) (hd : ∀ (r : ℕ), Nat.Prime r → r ∣ d → r ≤ w) : |AnalyticNumberTheory.Sieve.panDistributionNoncoprimeSum Y X d l (liuWeight N z y)| ≤ liuP₁DividesSum N z y Y X d l

Termwise majorant, not an equality for the signed sum. This is the finite R₁ reduction available before the still-open outer d ∣ Q weighted asymptotic estimate.

theorem MathlibNt.SieveTheory.LiuWeight.liuP₁DividesSum_mod_eq_abs_li_sum (N z y Y X d : ℕ) (havoid : ∀ (r : ℕ), Nat.Prime r → r ∣ d → ¬r ∣ N) : liuP₁DividesSum N z y Y X d (N % d) = ∑ p ∈ liuWeightPairs N z y with p.1 * p.2 ≤ X ∧ p.1 ∣ d, |AnalyticNumberTheory.Sieve.logarithmicIntegral (↑Y / (↑p.1 * ↑p.2))| / ↑d.totient

Termwise residue collapse through Liu's finite p₁ ∣ d sum. The explicit hypothesis is exactly what is needed to pass from p₁ ∣ d to p₁ ∤ N; in the corrected Chen application it follows from d ∣ correctedChenSiftingProduct N.

theorem MathlibNt.SieveTheory.LiuWeight.panDistributionNoncoprimeMajorant_liuWeight_mod_eq_abs_li_sum (N z w y Y X d : ℕ) (hwy : w ≤ y) (hd : ∀ (r : ℕ), Nat.Prime r → r ∣ d → r ≤ w) (havoid : ∀ (r : ℕ), Nat.Prime r → r ∣ d → ¬r ∣ N) : AnalyticNumberTheory.Sieve.panDistributionNoncoprimeMajorant Y X d (N % d) (liuWeight N z y) = ∑ p ∈ liuWeightPairs N z y with p.1 * p.2 ≤ X ∧ p.1 ∣ d, |AnalyticNumberTheory.Sieve.logarithmicIntegral (↑Y / (↑p.1 * ↑p.2))| / ↑d.totient

Exact non-coprime majorant after every relevant prime divisor of d is known not to divide N. The absolute value on li is retained.

theorem MathlibNt.SieveTheory.LiuWeight.abs_panDistributionNoncoprimeSum_liuWeight_mod_le_abs_li_sum (N z w y Y X d : ℕ) (hwy : w ≤ y) (hd : ∀ (r : ℕ), Nat.Prime r → r ∣ d → r ≤ w) (havoid : ∀ (r : ℕ), Nat.Prime r → r ∣ d → ¬r ∣ N) : |AnalyticNumberTheory.Sieve.panDistributionNoncoprimeSum Y X d (N % d) (liuWeight N z y)| ≤ ∑ p ∈ liuWeightPairs N z y with p.1 * p.2 ≤ X ∧ p.1 ∣ d, |AnalyticNumberTheory.Sieve.logarithmicIntegral (↑Y / (↑p.1 * ↑p.2))| / ↑d.totient

Signed non-coprime sum bounded by the same exact finite |li| expression. No outer modulus sum, cutoff estimate, or logarithmic estimate is asserted.