ChebyshevUpperSharp.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.ChebyshevUpperSharp.upperConstant line 12
Source documentation
The classical upper Chebyshev constant, approximately 1.10555.
```
def upperConstant : ℝ := 6 * ChebyshevLowerSharp.lowerConstant / 5
```
Mentions: OAI.Problem337.ChebyshevLowerSharp.lowerConstant
lemma OAI.Problem337.ChebyshevUpperSharp.upperConstant_pos line 14
lemma OAI.Problem337.ChebyshevUpperSharp.upperConstant_lt_1106_div_1000 line 19
theorem OAI.Problem337.ChebyshevUpperSharp.eventually_psi_upper line 25
Source documentation
The exact finite dilation recurrence and the factorial ratio limit give the classical sharp elementary upper coefficient for psi.
```
theorem eventually_psi_upper (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop,
      Chebyshev.psi N ≤ (upperConstant + ε) * (N : ℝ) := by
…
```
Mentions: OAI.Problem337.ChebyshevUpperSharp.upperConstant
theorem OAI.Problem337.ChebyshevUpperSharp.eventually_theta_upper line 41
theorem OAI.Problem337.ChebyshevUpperSharp.eventually_primeCounting_upper_of_theta line 50
Source documentation
The classical partial-summation remainder is already lower order. Hence an improved eventual coefficient for theta transfers without a fixed loss to the actual prime counting function.
```
theorem eventually_primeCounting_upper_of_theta (c ε : ℝ) (hε : 0 < ε)
    (hθ : ∀ᶠ N : ℕ in atTop, Chebyshev.theta N ≤ c * (N : ℝ)) :
    ∀ᶠ N : ℕ in atTop,
      (Nat.primeCounting N : ℝ) ≤ (c + ε) * (N : ℝ) / Real.log (N : ℝ) := by
…
```
theorem OAI.Problem337.ChebyshevUpperSharp.eventually_primeCounting_upper line 74
Source documentation
The classical upper Chebyshev coefficient transfers to actual primes.
```
theorem eventually_primeCounting_upper (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop,
      (Nat.primeCounting N : ℝ) ≤
        (upperConstant + ε) * (N : ℝ) / Real.log (N : ℝ) := by
…
```
Mentions: OAI.Problem337.ChebyshevUpperSharp.upperConstant
theorem OAI.Problem337.ChebyshevUpperSharp.eventually_primeCounting_upper_1106 line 84