ThreePrimeMangoldtPowerError.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.mangoldt_triple_error_isLittleO_rpow line 10

Source documentation

The elementary prime-power error is smaller than every power above 3/2.

theorem mangoldt_triple_error_isLittleO_rpow
    (α : ℝ) (hα : 3 / 2 < α) :
    (fun x : ℝ => 3 * x * Real.log x ^ 2 *
      (Chebyshev.psi x - Chebyshev.theta x)) =o[atTop]
      (fun x : ℝ => x ^ α) := by
…

theorem OAI.Problem337.mangoldtTripleSum_sub_primeTripleLogSum_isLittleO_rpow line 39
Source documentation
Actual Mangoldt and prime-only convolutions differ by o(u^α) for α>3/2.
```
theorem mangoldtTripleSum_sub_primeTripleLogSum_isLittleO_rpow
    (α : ℝ) (hα : 3 / 2 < α) :
    (fun u : ℕ => mangoldtTripleSum u - primeTripleLogSum u) =o[atTop]
      (fun u : ℕ => (u : ℝ) ^ α) := by
…
```
Mentions: OAI.Problem337.mangoldtTripleSum, OAI.Problem337.primeTripleLogSum
theorem OAI.Problem337.weighted_prime_power_lower_bound_of_mangoldt line 55
Source documentation
A positive power lower bound for the Mangoldt convolution survives removing higher prime powers at any exponent above 3/2. The lower bound itself remains an explicit analytic premise.
```
theorem weighted_prime_power_lower_bound_of_mangoldt
    (α : ℝ) (hα : 3 / 2 < α) (c : ℝ) (hc : 0 < c)
    (hmain : ∀ᶠ u : ℕ in atTop, Odd u → c * (u : ℝ) ^ α ≤ mangoldtTripleSum u) :
    ∀ᶠ u : ℕ in atTop, Odd u →
      (c / 2) * (u : ℝ) ^ α ≤ primeTripleLogSum u := by
…
```
Mentions: OAI.Problem337.mangoldtTripleSum, OAI.Problem337.primeTripleLogSum

theorem OAI.Problem337.mangoldt_prime_rpow_asymptotic_iff_filter line 72

Source documentation

Transfer of an arbitrary power-scale asymptotic to genuine prime triples, including along the odd integers or any other subfilter tending to infinity.

theorem mangoldt_prime_rpow_asymptotic_iff_filter
    (α : ℝ) (hα : 3 / 2 < α) (l : Filter ℕ) (hl : l ≤ atTop) (σ : ℕ → ℝ) :
    ((fun u : ℕ => mangoldtTripleSum u - σ u * (u : ℝ) ^ α) =o[l]
      (fun u : ℕ => (u : ℝ) ^ α)) ↔
    ((fun u : ℕ => primeTripleLogSum u - σ u * (u : ℝ) ^ α) =o[l]
      (fun u : ℕ => (u : ℝ) ^ α)) := by
…

Mentions: OAI.Problem337.mangoldtTripleSum, OAI.Problem337.primeTripleLogSum