SupplyBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.rational_supply_forces_size line 11
Source documentation
A supply of at most B rational divisors can only represent integers up to B*K, since each positive rational divisor is at most K.
```
theorem rational_supply_forces_size (m K B : ℕ) (hm : 1 ≤ m) (hK : 0 < K)
    (hsupply : HasRationalDivisorSupply m K B) : m ^ 4 ≤ B * K := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSupply
theorem OAI.Problem337.rational_supply_forces_large_auxiliary line 42
Source documentation
With sixteen summands, the full supply already forces the auxiliary integer to exceed the marker by a large margin.
```
theorem rational_supply_forces_large_auxiliary (m K : ℕ) (hm : 4 ≤ m)
    (hK : 0 < K) (hsupply : HasRationalDivisorSupply m K 16) : m ^ 2 ≤ K := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSupply