Wu's real product endpoints

Wu (2004), printed p. 220, defines the prime count with m * p ≤ y and li(t) = ∫₂ᵗ du / log u. The frozen Pan count has a natural endpoint. These bridges retain the real argument of li and the coupled inverse residue.

The integral below is a total Lean expression. Analytic uses in this module require its argument to be at least 2; no convention across the singularity at 1 is inferred from totalization.

noncomputable def Wu2004MeanValue.wuLi (t : ℝ) : ℝ

Equations

• Wu2004MeanValue.wuLi t = MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral 0 t

noncomputable def Wu2004MeanValue.scaledPrimeSet (y : ℝ) (d b m : ℕ) : Finset ℕ

Equations

• Wu2004MeanValue.scaledPrimeSet y d b m = {p ∈ Finset.range (⌊y / ↑m⌋₊ + 1) | Nat.Prime p ∧ m * p ≡ b [MOD d]}

noncomputable def Wu2004MeanValue.scaledPrimeCount (y : ℝ) (d b m : ℕ) : ℕ

Equations

• Wu2004MeanValue.scaledPrimeCount y d b m = (Wu2004MeanValue.scaledPrimeSet y d b m).card

noncomputable def Wu2004MeanValue.ebar (y : ℝ) (d b m : ℕ) : ℝ

Equations

• Wu2004MeanValue.ebar y d b m = ↑(Wu2004MeanValue.scaledPrimeCount y d b m) - Wu2004MeanValue.wuLi (y / ↑m) / ↑d.totient

theorem Wu2004MeanValue.mem_scaledPrimeSet {y : ℝ} {d b m p : ℕ} (hy : 0 ≤ y) (hm : 0 < m) : p ∈ scaledPrimeSet y d b m ↔ Nat.Prime p ∧ ↑m * ↑p ≤ y ∧ m * p ≡ b [MOD d]

theorem Wu2004MeanValue.scaledPrimeCount_eq_frozen (y : ℝ) (d b m : ℕ) (hy : 0 ≤ y) (hm : 0 < m) : scaledPrimeCount y d b m = AnalyticNumberTheory.Sieve.primesInAPBelow ⌊y⌋₊ m d b

theorem Wu2004MeanValue.scaledPrimeCount_eq_inverse (y : ℝ) (d b m : ℕ) (hy : 0 ≤ y) (hm : 0 < m) (hmd : m.Coprime d) : scaledPrimeCount y d b m = AnalyticNumberTheory.Sieve.primesInAP ⌊y / ↑m⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * b % d)

theorem Wu2004MeanValue.scaledPrimeCount_residue_mod (y : ℝ) (d b m : ℕ) : scaledPrimeCount y d (b % d) m = scaledPrimeCount y d b m

theorem Wu2004MeanValue.ebar_residue_mod (y : ℝ) (d b m : ℕ) : ebar y d (b % d) m = ebar y d b m

theorem Wu2004MeanValue.wuLi_sub_frozen (t : ℝ) : wuLi t = MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) t - 2 / Real.log 2

theorem Wu2004MeanValue.wuLi_sub_wuLi (u v : ℝ) : wuLi u - wuLi v = MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) u - MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) v

theorem Wu2004MeanValue.ebar_eq_frozen_add_correction (y : ℝ) (d b m : ℕ) (hy : 0 ≤ y) (hm : 0 < m) : ebar y d b m = MathlibNt.SieveTheory.LiuWeight.liuScaledAPError (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2)) ⌊y⌋₊ m d b + (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (↑⌊y⌋₊ / ↑m) - MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (y / ↑m) + 2 / Real.log 2) / ↑d.totient

theorem Wu2004MeanValue.ebar_nat_eq_frozen (Y d b m : ℕ) (hm : 0 < m) : ebar (↑Y) d b m = MathlibNt.SieveTheory.LiuWeight.liuScaledAPError (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2)) Y m d b + 2 / Real.log 2 / ↑d.totient

theorem Wu2004MeanValue.ebar_moving_inverse (r : ℝ) (d b m : ℕ) (hr : 0 ≤ r) (hm : 0 < m) (hmd : m.Coprime d) : ebar (↑m * r) d b m = ↑(AnalyticNumberTheory.Sieve.primesInAP ⌊r⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * b % d)) - wuLi r / ↑d.totient

theorem Wu2004MeanValue.abs_ebar_sub_frozen_le (y : ℝ) (d b m : ℕ) (hy : 0 ≤ y) (hm : 0 < m) (hd : 0 < d) (hlo : 2 ≤ ↑⌊y⌋₊ / ↑m) : |ebar y d b m - MathlibNt.SieveTheory.LiuWeight.liuScaledAPError (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2)) ⌊y⌋₊ m d b| ≤ 3 / Real.log 2 / ↑d.totient

The real-to-natural correction is bounded, but is not zero.