ThreePrimeAsymptoticInterfaces.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.ternaryMangoldtAsymptotic_iff_isLittleO line 12
Source documentation
The explicit epsilon formulation and the standard little-oh formulation of the ternary asymptotic agree on the filter of odd integers tending to infinity.
```
theorem ternaryMangoldtAsymptotic_iff_isLittleO :
    TernaryMangoldtAsymptotic ↔
      ((fun u : ℕ => mangoldtTripleSum u -
        (1 / 2 : ℝ) * threePrimeSingularSeries u * (u : ℝ) ^ 2) =o[
          atTop ⊓ principal {u : ℕ | Odd u}]
        (fun u : ℕ => (u : ℝ) ^ 2)) := by
…
```
Mentions: OAI.Problem337.TernaryMangoldtAsymptotic, OAI.Problem337.mangoldtTripleSum, OAI.Problem337.threePrimeSingularSeries
theorem OAI.Problem337.ternaryMangoldtAsymptotic_iff_prime_isLittleO line 35
Source documentation
Prime-power removal preserves the actual varying singular-series main term, not just the existence of some positive lower-bound constant.
```
theorem ternaryMangoldtAsymptotic_iff_prime_isLittleO :
    TernaryMangoldtAsymptotic ↔
      ((fun u : ℕ => primeTripleLogSum u -
        (1 / 2 : ℝ) * threePrimeSingularSeries u * (u : ℝ) ^ 2) =o[
          atTop ⊓ principal {u : ℕ | Odd u}]
        (fun u : ℕ => (u : ℝ) ^ 2)) := by
…
```
Mentions: OAI.Problem337.TernaryMangoldtAsymptotic, OAI.Problem337.primeTripleLogSum, OAI.Problem337.threePrimeSingularSeries
theorem OAI.Problem337.quantitativeThreePrimeLowerBound_of_weighted_singular_isLittleO line 47
Source documentation
The canonical prime-weighted Fourier interface may be used directly in place of the Mangoldt convolution. The little-oh estimate remains a hypothesis.
```
theorem quantitativeThreePrimeLowerBound_of_weighted_singular_isLittleO
    (h : (fun u : ℕ => weightedSupplyPrimeTriples u -
      (1 / 2 : ℝ) * threePrimeSingularSeries u * (u : ℝ) ^ 2) =o[
        atTop ⊓ principal {u : ℕ | Odd u}]
      (fun u : ℕ => (u : ℝ) ^ 2)) : QuantitativeThreePrimeLowerBound := by
…
```
Mentions: OAI.Problem337.weightedSupplyPrimeTriples, OAI.Problem337.threePrimeSingularSeries, OAI.Problem337.QuantitativeThreePrimeLowerBound