PrefixGap.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.sum_den_dvd_prod line 10
Source documentation
The reduced denominator of a finite rational sum divides the product of its summands' reduced denominators.
```
theorem sum_den_dvd_prod {α : Type*} [DecidableEq α]
    (s : Finset α) (q : α → ℚ) :
    (∑ j ∈ s, q j).den ∣ ∏ j ∈ s, (q j).den := by
…
```

theorem OAI.Problem337.one_div_le_of_den_dvd line 20

Source documentation

A positive rational with denominator dividing P is at least 1/P.

theorem one_div_le_of_den_dvd {q : ℚ} {P : ℕ}
    (hq : 0 < q) (hP : 0 < P) (hd : q.den ∣ P) :
    (1 : ℚ) / P ≤ q := by
…

theorem OAI.Problem337.prefix_remainder_gap line 35

Source documentation

The remainder after subtracting finitely many positive unit fractions from one has a gap of at least the reciprocal of the denominator product.

theorem prefix_remainder_gap {α : Type*} [DecidableEq α]
    (s : Finset α) (n : α → ℕ)
    (hn : ∀ j ∈ s, 0 < n j)
    (hrem : 0 < 1 - ∑ j ∈ s, (1 : ℚ) / (n j : ℚ)) :
    (1 : ℚ) / (∏ j ∈ s, n j : ℕ) ≤
      1 - ∑ j ∈ s, (1 : ℚ) / (n j : ℚ) := by
…