[TMEEMT/Buthe]: Fill theorem_a/b from the existing Buthe.lean statements

[Chessing234]

Description

The TMEEMT file says to fill sorrys that are already stated elsewhere. Close Buthe.theorem_a and Buthe.theorem_b in TMEEMT.lean as restatements of the existing Buthe.lean theorems:

• theorem_a: |ψ(x) - x| ≤ 0.94 √x for 11 < x ≤ 10^19 is the absolute-error form of Buthe.theorem_2a (Eψ x ≤ 0.94 / √x).
• theorem_b: 0 < li(x) - π(x) ≤ (√x / log x) (1.95 + 3.9/log x + 19.5/(log x)²) for 2 ≤ x ≤ 10^19 is Buthe.theorem_2f and Buthe.theorem_2e.

Blueprint

thm:buthe-a and thm:buthe-b in TMEEMT.lean.

Zulip

TBA

[Chessing234]

claim

[github-actions]

@Chessing234 this issue isn't on the PNT+ Project board yet, so it can't be claimed. A maintainer needs to add it first.

[Chessing234]

not on the board yet, same as #1692. happy to take it once it's added.

[Chessing234]

propose #1764