CompositeRationalSupply.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.HasRationalDivisorSum.mul line 13
Source documentation
Multiplication convolves the two positive lists. Numerators divide the product of the original supplies, and the term budgets multiply.
```
theorem HasRationalDivisorSum.mul {K L B C : ℕ} {x y : ℚ}
    (hx : HasRationalDivisorSum K x B) (hy : HasRationalDivisorSum L y C) :
    HasRationalDivisorSum (K * L) (x * y) (B * C) := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum
theorem OAI.Problem337.HasRationalDivisorSum.pow line 34
Source documentation
Taking powers is therefore available without any primality requirement.
```
theorem HasRationalDivisorSum.pow {K B : ℕ} {x : ℚ}
    (h : HasRationalDivisorSum K x B) (r : ℕ) :
    HasRationalDivisorSum (K ^ r) (x ^ r) (B ^ r) := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum
theorem OAI.Problem337.rational_divisor_supply_of_dense_set line 48
Source documentation
A dense supply on a single interval gives supply for every smaller positive integer. First represent its largest multiple below the endpoint as a sum of two good integers, then divide by the multiplier. No finite exceptional range or additional factorial factor is required for this completion step.
```
theorem rational_divisor_supply_of_dense_set
    (K B N : ℕ) (G : Finset ℕ) (hN : 4 < N)
    (hbad : ((Finset.Icc 1 N \ G).card : ℝ) ≤ (N : ℝ) / 8)
    (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_dense_set line 76
Source documentation
Dense composite-modulus supply can be fed directly to the canonical list interface used in marked grouping. The density and good-modulus supply remain explicit arithmetic hypotheses.
```
theorem marked_rational_supply_of_dense_set
    (m K B : ℕ) (G : Finset ℕ) (hm : 2 ≤ m)
    (hbad : ((Finset.Icc 1 (m ^ 4) \ G).card : ℝ) ≤ (m : ℝ) ^ 4 / 8)
    (hgood : ∀ u ∈ G, HasRationalDivisorSum K (u : ℚ) B) :
    HasRationalDivisorSupply m K (2 * B) := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum, OAI.Problem337.HasRationalDivisorSupply