MarkedThreePrimeReduction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.markedSupplyMultiplier_eq_supplyInteger line 13
Source documentation
The marked supply multiplier equals the prime-product supply integer.
```
lemma markedSupplyMultiplier_eq_supplyInteger (m : ℕ) :
    markedSupplyMultiplier m = supplyInteger (16 / Real.log 2) m := rfl
```
Mentions: OAI.Problem337.markedSupplyMultiplier, OAI.Problem337.supplyInteger
theorem OAI.Problem337.eventual_marked_list_supply_of_three_primes line 18
Source documentation
The finite-indexed three-prime supply feeds the canonical list supply. The quantitative three-prime lower bound remains an explicit hypothesis.
```
theorem eventual_marked_list_supply_of_three_primes
    (hthree : QuantitativeThreePrimeLowerBound) :
    ∀ᶠ m : ℕ in atTop,
      HasRationalDivisorSupply m (markedSupplyMultiplier m) 16 := by
…
```
Mentions: OAI.Problem337.QuantitativeThreePrimeLowerBound, OAI.Problem337.HasRationalDivisorSupply, OAI.Problem337.markedSupplyMultiplier

theorem OAI.Problem337.quantitative_marked_length_of_three_prime_lower_bound line 28

Source documentation

The quantitative marked-length bound follows from the explicit quantitative three-prime lower bound.

theorem quantitative_marked_length_of_three_prime_lower_bound
    (hthree : QuantitativeThreePrimeLowerBound) :
    ∀ ε : ℝ, 0 < ε → ∃ M : ℕ, 2 ≤ M ∧
      ∀ m : ℕ, M ≤ m → ∃ k : ℕ, ∃ n : Fin k → ℕ,
        IsOneExpansion n ∧ (∃ i, n i = m) ∧
        (k : ℝ) ≤ (257 / Real.log 2 + ε) * Real.log (Real.log (m : ℝ)) := by
…

Mentions: OAI.Problem337.QuantitativeThreePrimeLowerBound, OAI.Problem337.IsOneExpansion