ThreePrimeWeighted.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.weightedSupplyPrimeTriples line 12
Source documentation
The logarithmically weighted ordered prime triple count, with exactly the same triples as the rational-divisor supply reduction.
```
def weightedSupplyPrimeTriples (u : ℕ) : ℝ :=
…
```
lemma OAI.Problem337.weightedSupplyPrimeTriples_le line 16
theorem OAI.Problem337.quantitativeThreePrimeLowerBound_of_weighted line 44
Source documentation
Positive quadratic logarithmically weighted count is enough for the precise unweighted lower-bound interface already used by the solution.
```
theorem quantitativeThreePrimeLowerBound_of_weighted
    (hweighted : ∃ c : ℝ, 0 < c ∧ ∀ᶠ u : ℕ in atTop, Odd u →
      c * (u : ℝ) ^ 2 ≤ weightedSupplyPrimeTriples u) :
    QuantitativeThreePrimeLowerBound := by
…
```
Mentions: OAI.Problem337.weightedSupplyPrimeTriples, OAI.Problem337.QuantitativeThreePrimeLowerBound