New miniproject: Chebyshev bounds

Stream: PrimeNumberTheorem+

[Terence Tao]

One of the inputs needed in FKS2 / BKLNW is the upper bound $\psi(x) \leq 1.03883 x$ of Rosser and Schoenfeld, valid for all $x>0$, with the constant $1.03883$ being optimal (attained at $x=113$). However, the proof of Rosser and Schoenfeld required proving a prime number theorem that has long since been superseded by modern prime number theorems. Such a bound can probably be obtained more easily once we formalize the recent work of Helfgott and Chirre. Until then, I thought it might be nice to formalize the earlier elementary bound $\psi(x) \leq 1.1 x$ of Chebyshev (as well as some lower bounds), which does not require any Riemann zeta function facts, and has a self-contained proof, and which may already be good enough for some number theoretic applications. I have thus created tasks PNT#831 PNT#832 PNT#833 PNT#834 PNT#835 PNT#836 PNT#837 PNT#838 PNT#839 PNT#840 PNT#841 PNT#842 PNT#843 PNT#844 to formalize these bounds. Most of these are quite simple and suitable for beginners; there are a few that require some numerical computation, particularly the final theorem which will also require a numerical verification of $\psi(x) \leq 1.1 x$ for various small $x$ (I have not worked out exactly how much numerics will be needed).

[Pietro Monticone]

Aristotle disproved E_nu_eq_one as follows:

theorem E_nu_eq_one (x : ℝ) (hx : x ∈ Set.Icc 1 6) : E ν x = 1 := by
  -- Wait, there's a mistake. We can actually prove the opposite.
  negate_state
  -- Proof starts here:
  -- Let's choose any $x$ in the interval $[1, 6]$.
  use 6; norm_num [Chebyshev.E]
  -- By definition of $ν$, we know that its sum is zero.
  simp [Chebyshev.ν] at *
  -- Let's simplify the expression for $E(6)$.
  simp [Finsupp.sum] at *
  erw [Finset.sum_subset] <;> norm_num [Finsupp.support_add, Finsupp.support_sub, Finsupp.support_single_ne_zero] at * ; norm_cast at * ; simp_all +decide [Nat.floor_div_natCast]
  any_goals exact { 1, 2, 3, 5, 30 }
  · -- Let's simplify the expression for $E(6)$ and show it is not equal to 1.
    simp [Finsupp.single_apply] at *; norm_num at *
  · intro x hx; contrapose! hx; simp_all +decide [Finsupp.single_apply, Finset.sum_apply']
  · aesop

[Terence Tao]

Ah, right, it should be Set.Ico 1 6 rather than Set.Icc 1 6, but it looks like this has already been fixed in the most recent version.

[Aayush Rajasekaran]

Here is a PR for PNT#841 and PNT#842

[Alastair Irving]

There isn't an issue for psi_num, proving the bound for $x\le 30$. I have most of a very ugly proof and will hopefully make a PR later.

[Terence Tao]

I'll be interested to see how Lean handles these sorts of tedious small numerical checks that involve just enough floating point arithmetic to not be able to be delegated to decide.

[Alastair Irving]

psi_num is proved in PNT#892. It's quite messy. Even worse than the numerics is the fact that I had to manually evaluate each $\Lambda n$ depending on if $n$ is prime, prime power or not. Any simplification to that would be great, maybe we need a simproc to do this. The numerics are also a little painful, a tactic that can prove estimates on log/exp by working out how many terms of the taylor series we need would be helpful.

[Alejandro Radisic]

Following up on this thread, PNT#1007 proves psi_upper_clean (ψ(x) ≤ 1.11x for all x > 0), closing #844

For psi_num_2 (x ≤ 11723): LeanCert brute-forces ψ(N) ≤ 1.11N for all N = 1..11723 directly, no sparse checkpoint ladder needed. checkAllPsiLeMulWith is an O(N) incremental accumulator, walks each natural number, adds a computable von Mangoldt upper bound via interval arithmetic on log(p), checks the running sum stays below 1.11·N. A bridge theorem proves once that if the loop returns true, each individual bound holds. native_decide runs it in ~20-30 seconds.

For psi_upper_clean: strong induction on ⌊x⌋, using psi_num_2 as base case and psi_diff_upper for the inductive step. The log bound (5 log y − 5 ≤ 0.0037y for y > 11723) is closed by interval_decide.