MathlibNt.SieveTheory.Arithmetic.LiuSingularSeries

Liu's source singular series omits the prime 2. This file first separates its exact finite truncation from the legacy sieve-normalized proxy.

Source: Liu, main.tex, lines 98--102.

noncomputable def MathlibNt.SieveTheory.SingularSeries.liuLocalFactor (p N : ℕ) : ℝ

Liu's local factor at an odd prime.

Equations

• MathlibNt.SieveTheory.SingularSeries.liuLocalFactor p N = if p ∣ N then ↑p / (↑p - 1) else ↑p * (↑p - 2) / (↑p - 1) ^ 2

theorem MathlibNt.SieveTheory.SingularSeries.liuLocalFactor_of_dvd {p N : ℕ} (hp2 : 2 < p) (hpdvd : p ∣ N) : liuLocalFactor p N = (↑p - 1) / (↑p - 2) * (1 - 1 / (↑p - 1) ^ 2)

The divisor factor is the source product of the correction and base factors.

theorem MathlibNt.SieveTheory.SingularSeries.liuLocalFactor_of_not_dvd {p N : ℕ} (hp2 : 2 < p) (hpn : ¬p ∣ N) : liuLocalFactor p N = 1 - 1 / (↑p - 1) ^ 2

A nondivisor contributes exactly Liu's universal base factor.

theorem MathlibNt.SieveTheory.SingularSeries.liuLocalFactor_eq_localFactor {p N : ℕ} (hp2 : 2 < p) : liuLocalFactor p N = localFactor p N

Away from 2, Liu's local factor is the legacy local factor.

noncomputable def MathlibNt.SieveTheory.SingularSeries.liuSingularSeriesTruncated (N z : ℕ) : ℝ

Liu's source-normalized finite truncation: only odd primes p ≤ z.

Equations

• MathlibNt.SieveTheory.SingularSeries.liuSingularSeriesTruncated N z = ∏ p ∈ Finset.range (z + 1) with Nat.Prime p ∧ 2 < p, MathlibNt.SieveTheory.SingularSeries.liuLocalFactor p N

theorem MathlibNt.SieveTheory.SingularSeries.liuSingularSeriesTruncated_pos (N z : ℕ) : 0 < liuSingularSeriesTruncated N z

theorem MathlibNt.SieveTheory.SingularSeries.singularSeriesTruncated_eq_two_mul_liuSingularSeriesTruncated (N z : ℕ) (hN : Even N) (hz : 2 ≤ z) : singularSeriesTruncated N z = 2 * liuSingularSeriesTruncated N z

For even N, the legacy truncation differs from Liu's finite truncation by exactly the local factor 2.

theorem MathlibNt.SieveTheory.SingularSeries.singularSeries_eq_two_mul_liuSingularSeriesTruncatedAtN (N : ℕ) (hN : Even N) (hN2 : 2 ≤ N) : singularSeries N = 2 * liuSingularSeriesTruncated N N

At the legacy cutoff N, the proxy is exactly twice Liu's finite source-normalized truncation.

noncomputable def MathlibNt.SieveTheory.SingularSeries.liuBaseDeviation (p : ℕ) : ℝ

The deviation from 1 in Liu's universal odd-prime product.

Equations

• MathlibNt.SieveTheory.SingularSeries.liuBaseDeviation p = if Nat.Prime p ∧ 2 < p then -1 / (↑p - 1) ^ 2 else 0

theorem MathlibNt.SieveTheory.SingularSeries.summable_liuBaseDeviation_bound : Summable fun (p : ℕ) => 1 / (↑p - 1) ^ 2

theorem MathlibNt.SieveTheory.SingularSeries.summable_norm_liuBaseDeviation : Summable fun (p : ℕ) => ‖liuBaseDeviation p‖

theorem MathlibNt.SieveTheory.SingularSeries.one_add_liuBaseDeviation_pos (p : ℕ) : 0 < 1 + liuBaseDeviation p

theorem MathlibNt.SieveTheory.SingularSeries.one_add_liuBaseDeviation_le_one (p : ℕ) : 1 + liuBaseDeviation p ≤ 1

theorem MathlibNt.SieveTheory.SingularSeries.multipliable_one_add_liuBaseDeviation : Multipliable fun (p : ℕ) => 1 + liuBaseDeviation p

noncomputable def MathlibNt.SieveTheory.SingularSeries.liuUniversalProduct : ℝ

The convergent universal product ∏_{p > 2 prime} (1 - 1 / (p - 1)^2) in Liu's source.

Equations

• MathlibNt.SieveTheory.SingularSeries.liuUniversalProduct = ∏' (p : ℕ), (1 + MathlibNt.SieveTheory.SingularSeries.liuBaseDeviation p)

theorem MathlibNt.SieveTheory.SingularSeries.liuUniversalProduct_ne_zero : liuUniversalProduct ≠ 0

theorem MathlibNt.SieveTheory.SingularSeries.liuUniversalProduct_nonneg : 0 ≤ liuUniversalProduct

theorem MathlibNt.SieveTheory.SingularSeries.liuUniversalProduct_pos : 0 < liuUniversalProduct

noncomputable def MathlibNt.SieveTheory.SingularSeries.liuUniversalProductTruncated (z : ℕ) : ℝ

Finite truncation of Liu's universal product through z. Non-prime and even indices contribute 1.

Equations

• MathlibNt.SieveTheory.SingularSeries.liuUniversalProductTruncated z = ∏ p ∈ Finset.range (z + 1), (1 + MathlibNt.SieveTheory.SingularSeries.liuBaseDeviation p)

theorem MathlibNt.SieveTheory.SingularSeries.liuUniversalProductTruncated_pos (z : ℕ) : 0 < liuUniversalProductTruncated z

theorem MathlibNt.SieveTheory.SingularSeries.tendsto_liuUniversalProductTruncated : Filter.Tendsto liuUniversalProductTruncated Filter.atTop (nhds liuUniversalProduct)

theorem MathlibNt.SieveTheory.SingularSeries.liuUniversalProduct_le_truncated (z : ℕ) : liuUniversalProduct ≤ liuUniversalProductTruncated z

Every finite universal product dominates the full product. This is the monotone Euler-tail inequality; unlike pointwise convergence, it is uniform in the source integer.

noncomputable def MathlibNt.SieveTheory.SingularSeries.liuCorrectionFactor (p : ℕ) : ℝ

The finite correction attached to an odd prime divisor of N.

Equations

• MathlibNt.SieveTheory.SingularSeries.liuCorrectionFactor p = (↑p - 1) / (↑p - 2)

theorem MathlibNt.SieveTheory.SingularSeries.liuCorrectionFactor_pos {p : ℕ} (hp2 : 2 < p) : 0 < liuCorrectionFactor p

theorem MathlibNt.SieveTheory.SingularSeries.one_le_liuCorrectionFactor {p : ℕ} (hp2 : 2 < p) : 1 ≤ liuCorrectionFactor p

noncomputable def MathlibNt.SieveTheory.SingularSeries.liuCorrection (N : ℕ) : ℝ

The finite product of Liu's correction factors over odd prime divisors.

Equations

• MathlibNt.SieveTheory.SingularSeries.liuCorrection N = {p ∈ N.primeFactors | 2 < p}.prod MathlibNt.SieveTheory.SingularSeries.liuCorrectionFactor

theorem MathlibNt.SieveTheory.SingularSeries.liuCorrection_pos (N : ℕ) : 0 < liuCorrection N

theorem MathlibNt.SieveTheory.SingularSeries.one_le_liuCorrection (N : ℕ) : 1 ≤ liuCorrection N

noncomputable def MathlibNt.SieveTheory.SingularSeries.liuCorrectionTruncated (N z : ℕ) : ℝ

The correction product through z, written on the same index set as the finite universal product.

Equations

• MathlibNt.SieveTheory.SingularSeries.liuCorrectionTruncated N z = ∏ p ∈ Finset.range (z + 1) with Nat.Prime p ∧ 2 < p, if p ∣ N then MathlibNt.SieveTheory.SingularSeries.liuCorrectionFactor p else 1

theorem MathlibNt.SieveTheory.SingularSeries.liuCorrectionTruncated_pos (N z : ℕ) : 0 < liuCorrectionTruncated N z

theorem MathlibNt.SieveTheory.SingularSeries.one_add_liuBaseDeviation_eq_baseFactor {p : ℕ} (hp : Nat.Prime p) (hp2 : 2 < p) : 1 + liuBaseDeviation p = 1 - 1 / (↑p - 1) ^ 2

theorem MathlibNt.SieveTheory.SingularSeries.liuLocalFactor_eq_correction_mul_base {p N : ℕ} (hp : Nat.Prime p) (hp2 : 2 < p) : liuLocalFactor p N = (if p ∣ N then liuCorrectionFactor p else 1) * (1 + liuBaseDeviation p)

theorem MathlibNt.SieveTheory.SingularSeries.liuUniversalProductTruncated_eq_oddPrimeProd (z : ℕ) : liuUniversalProductTruncated z = ∏ p ∈ Finset.range (z + 1) with Nat.Prime p ∧ 2 < p, (1 + liuBaseDeviation p)

theorem MathlibNt.SieveTheory.SingularSeries.liuSingularSeriesTruncated_factorization (N z : ℕ) : liuSingularSeriesTruncated N z = liuCorrectionTruncated N z * liuUniversalProductTruncated z

theorem MathlibNt.SieveTheory.SingularSeries.liuCorrectionTruncated_eq_liuCorrection {N z : ℕ} (hN : 0 < N) (hz : N ≤ z) : liuCorrectionTruncated N z = liuCorrection N

theorem MathlibNt.SieveTheory.SingularSeries.liuCorrectionTruncated_le_liuCorrection (N z : ℕ) (hN : 0 < N) : liuCorrectionTruncated N z ≤ liuCorrection N

Truncating the divisor correction can only decrease it. Unlike the exact identity above, this comparison applies at cutoffs below N.

noncomputable def MathlibNt.SieveTheory.SingularSeries.liuSingularSeries (N : ℕ) : ℝ

Liu's genuine source singular series: its finite divisor correction times the convergent universal odd-prime product.

Equations

• MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N = MathlibNt.SieveTheory.SingularSeries.liuCorrection N * MathlibNt.SieveTheory.SingularSeries.liuUniversalProduct

theorem MathlibNt.SieveTheory.SingularSeries.liuSingularSeries_source_formula (N : ℕ) : liuSingularSeries N = (∏ p ∈ N.primeFactors with 2 < p, (↑p - 1) / (↑p - 2)) * ∏' (p : ℕ), (1 + liuBaseDeviation p)

theorem MathlibNt.SieveTheory.SingularSeries.liuSingularSeries_pos (N : ℕ) : 0 < liuSingularSeries N

theorem MathlibNt.SieveTheory.SingularSeries.liuUniversalProduct_le_liuSingularSeries (N : ℕ) : liuUniversalProduct ≤ liuSingularSeries N

Liu's singular series is uniformly bounded below by its positive universal Euler product; every divisor correction factor is at least one.

theorem MathlibNt.SieveTheory.SingularSeries.tendsto_liuSingularSeriesTruncated (N : ℕ) (hN : 0 < N) : Filter.Tendsto (liuSingularSeriesTruncated N) Filter.atTop (nhds (liuSingularSeries N))

theorem MathlibNt.SieveTheory.SingularSeries.eventually_liuUniversalProductTruncated_le (η : ℝ) (hη : 0 < η) : ∀ᶠ (z : ℕ) in Filter.atTop, liuUniversalProductTruncated z ≤ (1 + η) * liuUniversalProduct

The universal Euler truncations approach the full product from above, uniformly enough for the varying source integer used in Chen's sieve.

theorem MathlibNt.SieveTheory.SingularSeries.eventually_liuSingularSeriesTruncated_le (η : ℝ) (hη : 0 < η) : ∀ᶠ (z : ℕ) in Filter.atTop, ∀ (N : ℕ), 0 < N → liuSingularSeriesTruncated N z ≤ (1 + η) * liuSingularSeries N

Uniform upper comparison of every source truncation with Liu's genuine singular series. Missing divisor factors only decrease the correction, while the universal Euler tail is independent of N.

noncomputable def MathlibNt.SieveTheory.SingularSeries.liuSingularSeriesTail (z : ℕ) : ℝ

The positive tail quotient omitted by the universal truncation through z.

Equations

• MathlibNt.SieveTheory.SingularSeries.liuSingularSeriesTail z = MathlibNt.SieveTheory.SingularSeries.liuUniversalProduct / MathlibNt.SieveTheory.SingularSeries.liuUniversalProductTruncated z

theorem MathlibNt.SieveTheory.SingularSeries.liuSingularSeriesTail_pos (z : ℕ) : 0 < liuSingularSeriesTail z

theorem MathlibNt.SieveTheory.SingularSeries.liuSingularSeriesTail_le_one (z : ℕ) : liuSingularSeriesTail z ≤ 1

theorem MathlibNt.SieveTheory.SingularSeries.tendsto_liuSingularSeriesTail_one : Filter.Tendsto liuSingularSeriesTail Filter.atTop (nhds 1)

theorem MathlibNt.SieveTheory.SingularSeries.liuSingularSeriesTruncatedAtN_eq_div_tail (N : ℕ) (hN : 0 < N) : liuSingularSeriesTruncated N N = liuSingularSeries N / liuSingularSeriesTail N

theorem MathlibNt.SieveTheory.SingularSeries.singularSeries_eq_two_mul_liuSingularSeries_div_tail (N : ℕ) (hNeven : Even N) (hN : 2 ≤ N) : singularSeries N = 2 * (liuSingularSeries N / liuSingularSeriesTail N)

For even source integers, the legacy sieve proxy is exactly twice the true Liu series divided by its positive finite-cutoff tail. Since that tail tends to 1, the proxy has the wrong asymptotic normalization by a factor 2.

theorem MathlibNt.SieveTheory.SingularSeries.two_mul_liuSingularSeries_le_singularSeries (N : ℕ) (hNeven : Even N) (hN : 2 ≤ N) : 2 * liuSingularSeries N ≤ singularSeries N

The finite sieve-normalized proxy dominates twice Liu's genuine series. The proof uses only the sign of the universal Euler tail, not fixed-N convergence.