A monotone error envelope for the actual prime counting function

The ordinary PNT is reused from the byte-frozen nine-module source closure. The comparator is t / log t, so Abel summation against its derivative has an additional explicit 1 / log t ^ 2 term.

noncomputable def LiLiuPrereqBuchstab.primePi (t : ℝ) : ℝ

Equations

• LiLiuPrereqBuchstab.primePi t = ↑⌊t⌋₊.primeCounting

noncomputable def LiLiuPrereqBuchstab.primeRelativeError (t : ℝ) : ℝ

Equations

• LiLiuPrereqBuchstab.primeRelativeError t = |LiLiuPrereqBuchstab.primePi t / (t / Real.log t) - 1|

theorem LiLiuPrereqBuchstab.primePi_asymptotic : Asymptotics.IsEquivalent Filter.atTop primePi fun (t : ℝ) => t / Real.log t

theorem LiLiuPrereqBuchstab.tendsto_primeRelativeError : Filter.Tendsto primeRelativeError Filter.atTop (nhds 0)

noncomputable def LiLiuPrereqBuchstab.primeErrorStart : ℝ

Equations

• LiLiuPrereqBuchstab.primeErrorStart = Classical.choose LiLiuPrereqBuchstab.exists_primeError_start✝

theorem LiLiuPrereqBuchstab.primeErrorStart_spec : 3 ≤ primeErrorStart ∧ Real.exp 1 ≤ primeErrorStart ∧ ∀ t ≥ primeErrorStart, primeRelativeError t ≤ 1

noncomputable def LiLiuPrereqBuchstab.primeErrorEnvelope (y : ℝ) : ℝ

A genuine tail supremum, clamped below a fixed PNT threshold.

Equations

• LiLiuPrereqBuchstab.primeErrorEnvelope y = sSup (LiLiuPrereqBuchstab.primeRelativeError '' Set.Ici (max LiLiuPrereqBuchstab.primeErrorStart y))

theorem LiLiuPrereqBuchstab.primeRelativeError_le_envelope {y t : ℝ} (ht : max primeErrorStart y ≤ t) : primeRelativeError t ≤ primeErrorEnvelope y

theorem LiLiuPrereqBuchstab.primeErrorEnvelope_nonneg (y : ℝ) : 0 ≤ primeErrorEnvelope y

theorem LiLiuPrereqBuchstab.primeErrorEnvelope_le_one (y : ℝ) : primeErrorEnvelope y ≤ 1

theorem LiLiuPrereqBuchstab.antitone_primeErrorEnvelope : Antitone primeErrorEnvelope

theorem LiLiuPrereqBuchstab.tendsto_primeErrorEnvelope : Filter.Tendsto primeErrorEnvelope Filter.atTop (nhds 0)

theorem LiLiuPrereqBuchstab.primePi_error_le {y t : ℝ} (hy : primeErrorStart ≤ y) (hyt : y ≤ t) : |primePi t - t / Real.log t| ≤ primeErrorEnvelope y * (t / Real.log t)

One threshold controls the actual PNT error at every larger real point.

theorem LiLiuPrereqBuchstab.primePi_le_two_mul {t : ℝ} (ht : primeErrorStart ≤ t) : primePi t ≤ 2 * (t / Real.log t)

theorem LiLiuPrereqBuchstab.div_log_mono {s t : ℝ} (hs : primeErrorStart ≤ s) (hst : s ≤ t) : s / Real.log s ≤ t / Real.log t

The elementary monotonicity needed for the prime-weighted boundary error.