ChebyshevRealBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.ChebyshevRealBounds.eventually_psi_lower_real line 13
Source documentation
Floor transfer of the stronger elementary lower bound to all real endpoints. The threshold is uniform in the endpoint; no prime number theorem is used.
```
theorem eventually_psi_lower_real {c : ℝ} (hc : c < lowerConstant) :
    ∀ᶠ x : ℝ in atTop, c * x ≤ Chebyshev.psi x := by
…
```
theorem OAI.Problem337.ChebyshevRealBounds.eventually_theta_lower_real line 31
Source documentation
The same lower coefficient holds for the log-weighted sum over primes alone.
```
theorem eventually_theta_lower_real {c : ℝ} (hc : c < lowerConstant) :
    ∀ᶠ x : ℝ in atTop, c * x ≤ Chebyshev.theta x := by
…
```
theorem OAI.Problem337.ChebyshevRealBounds.eventually_theta_lower line 52
Source documentation
Natural endpoints for direct use in finite exceptional-prime deletion.
```
theorem eventually_theta_lower {c : ℝ} (hc : c < lowerConstant) :
    ∀ᶠ N : ℕ in atTop, c * N ≤ Chebyshev.theta N :=
…
```

theorem OAI.Problem337.ChebyshevRealBounds.eventually_primeCounting_lower_real line 58

Source documentation

The sharp elementary prime-count lower bound at a real endpoint.

theorem eventually_primeCounting_lower_real {c : ℝ} (hc : c < lowerConstant) :
    ∀ᶠ x : ℝ in atTop, c * x / Real.log x ≤ (Nat.primeCounting ⌊x⌋₊ : ℝ) := by
…