RationalSupplyFromThreePrimes.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.eventual_marked_rational_supply_of_three_primes line 12
Source documentation
The full rational-divisor supply, including the specified logarithmic prime products and factorial fallback, follows from the one explicit quantitative three-prime input.
```
theorem eventual_marked_rational_supply_of_three_primes
    (hthree : QuantitativeThreePrimeLowerBound) :
    ∀ᶠ m : ℕ in atTop, ∀ s : ℕ, 1 ≤ s → s ≤ m ^ 4 →
      HasRationalDivisorSum (supplyInteger (16 / Real.log 2) m) (s : ℚ) 16 := by
…
```
Mentions: OAI.Problem337.QuantitativeThreePrimeLowerBound, OAI.Problem337.HasRationalDivisorSum, OAI.Problem337.supplyInteger

theorem OAI.Problem337.marked_rational_supply_package_of_three_primes line 28

Source documentation

Simultaneous size and representation guarantees for the supply integer. This does not assert the unproved three-prime hypothesis.

theorem marked_rational_supply_package_of_three_primes
    (hthree : QuantitativeThreePrimeLowerBound) (ε : ℝ) (hε : 0 < ε) :
    ∃ M : ℕ, 2 ≤ M ∧ ∀ m : ℕ, M ≤ m →
      m < supplyInteger (16 / Real.log 2) m ∧
      Real.log (supplyInteger (16 / Real.log 2) m : ℝ) ≤
        (32 / Real.log 2 + ε) * Real.log (m : ℝ) * Real.log (Real.log (m : ℝ)) ∧
      ∀ s : ℕ, 1 ≤ s → s ≤ m ^ 4 →
        HasRationalDivisorSum (supplyInteger (16 / Real.log 2) m) (s : ℚ) 16 := by
…

Mentions: OAI.Problem337.QuantitativeThreePrimeLowerBound, OAI.Problem337.supplyInteger, OAI.Problem337.HasRationalDivisorSum