RationalSupplyScaling.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.HasRationalDivisorSum.div_nat line 11
Source documentation
Dividing a rational-divisor representation by a positive integer does not change its numerators or its number of summands.
```
theorem HasRationalDivisorSum.div_nat {K B : ℕ} {x : ℚ}
    (h : HasRationalDivisorSum K x B) {d : ℕ} (hd : 0 < d) :
    HasRationalDivisorSum K (x / (d : ℚ)) B := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum
theorem OAI.Problem337.HasRationalDivisorSum.of_nat_multiple line 23
Source documentation
It suffices to represent any positive integral multiple of the desired integer. No upper bound on the multiplier is needed in this algebraic step.
```
theorem HasRationalDivisorSum.of_nat_multiple {K B d s : ℕ}
    (h : HasRationalDivisorSum K ((d * s : ℕ) : ℚ) B) (hd : 0 < d) :
    HasRationalDivisorSum K (s : ℚ) B := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum
theorem OAI.Problem337.HasRationalDivisorSum.finset_sum line 31
Source documentation
Finite sums combine rational-divisor representations with the exact sum of their budgets, without requiring the displayed summands to be distinct.
```
theorem HasRationalDivisorSum.finset_sum {ι : Type*} {K : ℕ}
    (I : Finset ι) (x : ι → ℚ) (B : ι → ℕ)
    (h : ∀ i ∈ I, HasRationalDivisorSum K (x i) (B i)) :
    HasRationalDivisorSum K (∑ i ∈ I, x i) (∑ i ∈ I, B i) := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum

theorem OAI.Problem337.HasRationalDivisorSum.sum_fin line 48

Source documentation

Uniform-budget version for a finite indexed family.

theorem HasRationalDivisorSum.sum_fin {K B n : ℕ} {x : Fin n → ℚ}
    (h : ∀ i, HasRationalDivisorSum K (x i) B) :
    HasRationalDivisorSum K (∑ i, x i) (n * B) := by
…

Mentions: OAI.Problem337.HasRationalDivisorSum

theorem OAI.Problem337.rational_divisor_sum_of_dvd_sum line 57
Source documentation
A positive integer sum divisible by s gives a rational representation of s with the same supply and budget. This is the precise positive-multiple interface; in particular its arithmetic premise is not an exact-sum premise.
```
theorem rational_divisor_sum_of_dvd_sum {K B n s : ℕ} (a : Fin n → ℕ)
    (hrep : ∀ i, HasRationalDivisorSum K (a i : ℚ) B)
    (hpos : 0 < ∑ i, a i) (hdiv : s ∣ ∑ i, a i) :
    HasRationalDivisorSum K (s : ℚ) (n * B) := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum
theorem OAI.Problem337.rational_divisor_sum_of_half_pair line 75
Source documentation
Each half of a represented pair has the same two-summand budget. This is the scaling step for a half-Goldbach additive basis.
```
theorem rational_divisor_sum_of_half_pair {K B p q s : ℕ}
    (hp : HasRationalDivisorSum K (p : ℚ) B)
    (hq : HasRationalDivisorSum K (q : ℚ) B)
    (hs : 2 * s = p + q) :
    HasRationalDivisorSum K (s : ℚ) (2 * B) := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum
theorem OAI.Problem337.rational_divisor_sum_of_half_pair_basis line 88
Source documentation
A sum of n members of a half-pair set lifts to a representation of its sum with 2*n*B rational divisors. All prime or density information belongs in the explicit hypotheses supplied to this elementary statement.
```
theorem rational_divisor_sum_of_half_pair_basis {K B n s : ℕ}
    (a p q : Fin n → ℕ) (hs : ∑ i, a i = s)
    (ha : ∀ i, 2 * a i = p i + q i)
    (hp : ∀ i, HasRationalDivisorSum K (p i : ℚ) B)
    (hq : ∀ i, HasRationalDivisorSum K (q i : ℚ) B) :
    HasRationalDivisorSum K (s : ℚ) (2 * n * B) := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum