ThreePrimeMangoldtAsymptotics.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.primeTripleLogSum_le_mangoldtTripleSum line 11
Source documentation
Removing higher prime powers can only reduce a nonnegative convolution.
```
lemma primeTripleLogSum_le_mangoldtTripleSum (u : ℕ) :
    primeTripleLogSum u ≤ mangoldtTripleSum u := by
…
```
Mentions: OAI.Problem337.primeTripleLogSum, OAI.Problem337.mangoldtTripleSum
theorem OAI.Problem337.abs_mangoldtTripleSum_sub_primeTripleLogSum_le line 25
Source documentation
Two-sided control of the actual convolution error, without an analytic hypothesis.
```
theorem abs_mangoldtTripleSum_sub_primeTripleLogSum_le (u : ℕ) :
    |mangoldtTripleSum u - primeTripleLogSum u| ≤
      3 * (u : ℝ) * Real.log (u : ℝ) ^ 2 *
        (Chebyshev.psi u - Chebyshev.theta u) := by
…
```
Mentions: OAI.Problem337.mangoldtTripleSum, OAI.Problem337.primeTripleLogSum
theorem OAI.Problem337.mangoldtTripleSum_sub_primeTripleLogSum_isLittleO line 33
Source documentation
Higher prime powers do not affect the normalized quadratic main term.
```
theorem mangoldtTripleSum_sub_primeTripleLogSum_isLittleO :
    (fun u : ℕ => mangoldtTripleSum u - primeTripleLogSum u) =o[atTop]
      (fun u : ℕ => (u : ℝ) ^ 2) := by
…
```
Mentions: OAI.Problem337.mangoldtTripleSum, OAI.Problem337.primeTripleLogSum
theorem OAI.Problem337.tendsto_mangoldtTripleSum_sub_primeTripleLogSum_div_sq line 46
Source documentation
The normalized difference converges to zero along all natural integers.
```
theorem tendsto_mangoldtTripleSum_sub_primeTripleLogSum_div_sq :
    Tendsto (fun u : ℕ =>
      (mangoldtTripleSum u - primeTripleLogSum u) / (u : ℝ) ^ 2)
      atTop (nhds 0) :=
…
```
Mentions: OAI.Problem337.mangoldtTripleSum, OAI.Problem337.primeTripleLogSum
theorem OAI.Problem337.mangoldt_prime_quadratic_asymptotic_iff_filter line 55
Source documentation
Any quadratic asymptotic, including a varying singular-series coefficient, is equivalent for the Mangoldt and prime-only convolutions. This is only an error-transfer theorem: neither asymptotic formula is asserted.
```
theorem mangoldt_prime_quadratic_asymptotic_iff_filter
    (l : Filter ℕ) (hl : l ≤ atTop) (σ : ℕ → ℝ) :
    ((fun u : ℕ => mangoldtTripleSum u - σ u * (u : ℝ) ^ 2) =o[l]
      (fun u : ℕ => (u : ℝ) ^ 2)) ↔
    ((fun u : ℕ => primeTripleLogSum u - σ u * (u : ℝ) ^ 2) =o[l]
      (fun u : ℕ => (u : ℝ) ^ 2)) := by
…
```
Mentions: OAI.Problem337.mangoldtTripleSum, OAI.Problem337.primeTripleLogSum

theorem OAI.Problem337.mangoldt_prime_quadratic_asymptotic_iff line 71

Source documentation

The same transfer without restricting the parameter (the filter version also applies directly to the odd integers).

theorem mangoldt_prime_quadratic_asymptotic_iff (σ : ℕ → ℝ) :
    ((fun u : ℕ => mangoldtTripleSum u - σ u * (u : ℝ) ^ 2) =o[atTop]
      (fun u : ℕ => (u : ℝ) ^ 2)) ↔
    ((fun u : ℕ => primeTripleLogSum u - σ u * (u : ℝ) ^ 2) =o[atTop]
      (fun u : ℕ => (u : ℝ) ^ 2)) :=
…

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