ThreePrimeAnalyticReduction.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.quantitativeThreePrimeLowerBound_of_mangoldt_singular_error line 13
Source documentation
The uniform lower bound on the singular series supplies a quadratic main term. This bridge has an explicit analytic error hypothesis and asserts no estimate for prime exponential sums.
```
theorem quantitativeThreePrimeLowerBound_of_mangoldt_singular_error
    (A : ℝ) (hA : 0 < A)
    (herror : ∀ᶠ u : ℕ in atTop, Odd u →
      |mangoldtTripleSum u - A * threePrimeSingularSeries u * (u : ℝ) ^ 2| ≤
        (A / 2) * (u : ℝ) ^ 2) :
    QuantitativeThreePrimeLowerBound := by
…
```
Mentions: OAI.Problem337.mangoldtTripleSum, OAI.Problem337.threePrimeSingularSeries, OAI.Problem337.QuantitativeThreePrimeLowerBound
def OAI.Problem337.TernaryMangoldtAsymptotic line 32
Source documentation
The classical ternary Mangoldt asymptotic, stated as a proposition to keep the genuinely unproved analytic input explicit. Its main term is the singular series times the area of the positive fixed-sum simplex, namely u²/2.
```
def TernaryMangoldtAsymptotic : Prop :=
…
```
theorem OAI.Problem337.quantitativeThreePrimeLowerBound_of_ternary_mangoldt_asymptotic line 39
Source documentation
Uniform singular-series positivity, prime-power removal, and unweighting are all discharged. Only the stated ternary asymptotic remains as an input.
```
theorem quantitativeThreePrimeLowerBound_of_ternary_mangoldt_asymptotic
    (h : TernaryMangoldtAsymptotic) : QuantitativeThreePrimeLowerBound := by
…
```
Mentions: OAI.Problem337.TernaryMangoldtAsymptotic, OAI.Problem337.QuantitativeThreePrimeLowerBound