DenseModularSupply.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.rational_divisor_supply_of_two_thirds line 13
Source documentation
A supply on more than two thirds of an initial interval gives supply for every smaller positive integer at twice the original budget. The multiplier is removed by changing only the rational summands' denominators.
```
theorem rational_divisor_supply_of_two_thirds
    (K B N : ℕ) (G : Finset ℕ) (hG : G ⊆ Finset.Icc 1 N)
    (hcard : 2 * N < 3 * G.card)
    (hgood : ∀ u ∈ G, HasRationalDivisorSum K (u : ℚ) B) :
    ∀ s : ℕ, 1 ≤ s → s ≤ N → HasRationalDivisorSum K (s : ℚ) (2 * B) := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum

theorem OAI.Problem337.rational_divisor_supply_of_third_exception line 34

Source documentation

Complement-cardinality version: fewer than a third of the initial interval may be exceptional. Good elements outside that interval are irrelevant.

theorem rational_divisor_supply_of_third_exception
    (K B N : ℕ) (G : Finset ℕ)
    (hbad : 3 * (Finset.Icc 1 N \ G).card < N)
    (hgood : ∀ u ∈ G, HasRationalDivisorSum K (u : ℚ) B) :
    ∀ s : ℕ, 1 ≤ s → s ≤ N → HasRationalDivisorSum K (s : ℚ) (2 * B) := by
…

Mentions: OAI.Problem337.HasRationalDivisorSum

theorem OAI.Problem337.marked_rational_supply_of_third_exception line 51
Source documentation
The sharper finite density completion in the canonical marked-grouping interface. This does not supply the density or the good-modulus estimates.
```
theorem marked_rational_supply_of_third_exception
    (m K B : ℕ) (G : Finset ℕ)
    (hbad : 3 * (Finset.Icc 1 (m ^ 4) \ G).card < m ^ 4)
    (hgood : ∀ u ∈ G, HasRationalDivisorSum K (u : ℚ) B) :
    HasRationalDivisorSupply m K (2 * B) := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum, OAI.Problem337.HasRationalDivisorSupply