A quick subproject: Costa Pereira inequality

Stream: PrimeNumberTheorem+

[Terence Tao]

While working on the blueprint for FKS2, I saw a reference to the following inequalities
$\psi(x^{1/2}) + \psi(x^{1/3}) + \psi(x^{1/7}) \leq \psi(x) - \vartheta(x) \leq \psi(x^{1/2}) + \psi(x^{1/3}) + \psi(x^{1/5})$
by Costa Pereira controlling the error between the two Chebyshev functions. These inequalities are not difficult to prove starting from the identity $\psi(x) = \sum_{k=1}^\infty \vartheta(x^{1/k})$, so I have created some small formalization tasks PNT#676 PNT#677 PNT#678 PNT#679 PNT#680 PNT#681 PNT#682 PNT#683 PNT#684 PNT#685 to establish these inequalities. These should be very small tasks, suitable for beginners (or for autoformalization tools).

[Alastair Irving]

There's a possible misformalization in the statements here, ∑' k, seems to being treated as a sum over k in the reals (whatever that even means). An easy fix is to put ∑' (k : ℕ), but I wonder if it would be better to use finite sums throughout. The first lemma is then docs#Chebyshev.psi_eq_sum_theta.

[Pietro Monticone]

Yes, I'm going to claim it soon. I will fix the statement as follows before proving it:

theorem sublemma_1_1 {x : ℝ} (hx : 0 < x) : ψ x = ∑' (k : ℕ), θ (x ^ (1 / (k : ℝ))) := by sorry

[Pietro Monticone]

PNT#676

[Terence Tao]

I was on the fence as to whether to use infinite sums or finite sums here. If one uses finite sums then when one performs the various manipulations one has to keep track of all the ranges and sometimes they are incompatible.

One possible compromise is to develop a version of docs#Chebyshev.psi_eq_sum_theta in which the upper range is not required ⌊Real.log x / Real.log 2⌋₊, but rather any N which is at least as large as Real.log x / Real.log 2. (Or that it is true for Filter.Eventually all N.) Then one can work with finite sums without worrying too much about limits, absolute convergence, etc., and filter_upwards one's way out of trouble at the end.

EDIT: Maybe just have two versions sublemma_1_1 and sublemma_1_1' of the same result, one using infinite sums and the other using finite sums with a sufficiently large range? Then we get the best of both worlds. Thus:

theorem sublemma_1_1' {x : ℝ} (hx : 0 < x) : ∀ᶠ N in Filter.atTop, ψ x = ∑ k ∈ Finset.range N, θ (x ^ (1 / (k : ℝ))) := by sorry

[Morten Ness]

Hey guys, forgive me if this is a silly question, I just started learning Lean 3 days ago.

The solution to sublemma_1_6 relies on sublemma_1_5 using ∑' k. When defining ∑' (k : ℕ) in 1_5, sublemma_1_6 does not work. If I am not mistaken, sublemma_1_5 should look something like this:

theorem sublemma_1_5 {x : ℝ} (hx : 0 < x) :
    ψ (x ^ (1 / 3 : ℝ)) =
      ∑' (k : ℕ), θ (x ^ (1 / (6 * ((Nat.succ k : ℕ) : ℝ) - 3))) +
      ∑' (k : ℕ), θ (x ^ (1 / (6 * ((Nat.succ k : ℕ) : ℝ)))) := by

PTN#727

[Terence Tao]

Yes, you are right. PNT#730 hopefully fixes these issues and makes all sums range over the natural numbers rather the reals.

[Pietro Monticone]

Yep, that PR should solve all the type-annotation issues.

[Pietro Monticone]

Not really, all statements should use k.succ. Fixing the whole file now directly in PNT#734

[Ruben Van de Velde]

Do you mean "should use k + 1"?

[Pietro Monticone]

Aristotle proved all the remaining lemmas in CostaPereira.lean (PNT#737).