ThreePrimeMangoldtBridge.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.primeTripleLogSum_eq_weightedSupplyPrimeTriples line 11
Source documentation
The independently defined prime-weighted counts are identical.
```
lemma primeTripleLogSum_eq_weightedSupplyPrimeTriples (u : ℕ) :
    primeTripleLogSum u = weightedSupplyPrimeTriples u := rfl
```
Mentions: OAI.Problem337.primeTripleLogSum, OAI.Problem337.weightedSupplyPrimeTriples
theorem OAI.Problem337.quantitativeThreePrimeLowerBound_of_mangoldt line 17
Source documentation
The standard quadratic lower bound for the von Mangoldt convolution is sufficient for the exact arithmetic hypothesis used in the Egyptian-fraction construction. The genuinely analytic lower bound remains an explicit premise.
```
theorem quantitativeThreePrimeLowerBound_of_mangoldt
    (hmain : ∃ c : ℝ, 0 < c ∧ ∀ᶠ u : ℕ in atTop, Odd u →
      c * (u : ℝ) ^ 2 ≤ mangoldtTripleSum u) :
    QuantitativeThreePrimeLowerBound := by
…
```
Mentions: OAI.Problem337.mangoldtTripleSum, OAI.Problem337.QuantitativeThreePrimeLowerBound