CleanupApplications.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.egyptian_expansion_length_numerator line 10
Source documentation
Existence follows from cleaning up the representation with a copies of 1/b.
```
theorem egyptian_expansion_length_numerator (a b : ℕ) (ha : 1 ≤ a) (hab : a < b) :
    ∃ n : Fin a → ℕ, IsEgyptianExpansion ((a : ℚ) / b) n := by
…
```
Mentions: OAI.Problem337.IsEgyptianExpansion
theorem OAI.Problem337.egyptianLengths_nonempty_cleanup line 18
Source documentation
The set whose infimum defines the Egyptian length is nonempty.
```
theorem egyptianLengths_nonempty_cleanup (a b : ℕ) (ha : 1 ≤ a) (hab : a < b) :
    (egyptianLengths a b).Nonempty :=
…
```
Mentions: OAI.Problem337.egyptianLengths

theorem OAI.Problem337.egyptian_expansion_of_list line 23

Source documentation

List-form interface for the dense-family and quantitative-tail constructions.

theorem egyptian_expansion_of_list (x : ℚ) (hx : x < 1) (l : List ℕ)
    (hpos : ∀ d ∈ l, 1 ≤ d)
    (hsum : (l.map (fun d : ℕ => (1 : ℚ) / (d : ℚ))).sum = x) :
    ∃ n : Fin l.length → ℕ, IsEgyptianExpansion x n := by
…

Mentions: OAI.Problem337.IsEgyptianExpansion