RationalDivisorSupplyAlgebra.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.HasRationalDivisorSum line 12
Source documentation
A rational number is a sum of at most B positive rational summands, whose natural numerators divide the fixed common supply K.
```
def HasRationalDivisorSum (K : ℕ) (x : ℚ) (B : ℕ) : Prop :=
…
```
theorem OAI.Problem337.HasRationalDivisorSum.mono_budget line 17
theorem OAI.Problem337.HasRationalDivisorSum.mono_supply line 23
theorem OAI.Problem337.hasRationalDivisorSum_of_dvd line 30
theorem OAI.Problem337.hasRationalDivisorSum_of_common_denominator line 37
theorem OAI.Problem337.HasRationalDivisorSum.add line 43

theorem OAI.Problem337.rational_divisor_sum_three line 59

Source documentation

Three five-term prime representations give fifteen terms.

theorem rational_divisor_sum_three {K p q r : ℕ}
    (hp : HasRationalDivisorSum K (p : ℚ) 5)
    (hq : HasRationalDivisorSum K (q : ℚ) 5)
    (hr : HasRationalDivisorSum K (r : ℚ) 5) :
    HasRationalDivisorSum K ((p + q + r : ℕ) : ℚ) 15 := by
…

Mentions: OAI.Problem337.HasRationalDivisorSum

theorem OAI.Problem337.HasRationalDivisorSum.add_one line 67
Source documentation
An additional 1/1 fills the parity gap at a cost of one summand.
```
theorem HasRationalDivisorSum.add_one {K B : ℕ} {x : ℚ}
    (h : HasRationalDivisorSum K x B) :
    HasRationalDivisorSum K (x + 1) (B + 1) := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum
theorem OAI.Problem337.rational_divisor_sum_small line 73
Source documentation
Factorial factors absorb every fixed finite exceptional range.
```
theorem rational_divisor_sum_small {K N s : ℕ} (hNK : N.factorial ∣ K)
    (hs : 1 ≤ s) (hsN : s ≤ N) : HasRationalDivisorSum K (s : ℚ) 1 := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum
theorem OAI.Problem337.rational_divisor_supply_of_odd line 80
Source documentation
The final arithmetic passage in the rational-divisor supply lemma: odd integers use fifteen terms, even integers use one more, and a factorial factor covers the bounded initial interval.
```
theorem rational_divisor_supply_of_odd {K N Y : ℕ} (_hN : 1 ≤ N)
    (hNK : N.factorial ∣ K)
    (hodd : ∀ u : ℕ, N ≤ u → u ≤ Y → Odd u →
      HasRationalDivisorSum K (u : ℚ) 15) :
    ∀ s : ℕ, 1 ≤ s → s ≤ Y → HasRationalDivisorSum K (s : ℚ) 16 := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum

theorem OAI.Problem337.rational_divisor_supply_of_triples line 100

Source documentation

Package the three-prime combinatorial step without hiding it as an axiom: any supplied three-summand representations of sufficiently large odd integers extend, using the factorial fallback, to the complete interval.

theorem rational_divisor_supply_of_triples {K N Y : ℕ} (hN : 1 ≤ N)
    (hNK : N.factorial ∣ K)
    (htriples : ∀ u : ℕ, N ≤ u → u ≤ Y → Odd u →
      ∃ p q r : ℕ, p + q + r = u ∧
        HasRationalDivisorSum K (p : ℚ) 5 ∧
        HasRationalDivisorSum K (q : ℚ) 5 ∧
        HasRationalDivisorSum K (r : ℚ) 5) :
    ∀ s : ℕ, 1 ≤ s → s ≤ Y → HasRationalDivisorSum K (s : ℚ) 16 := by
…

Mentions: OAI.Problem337.HasRationalDivisorSum