LengthBasic.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.egyptianLength_le_of_expansion line 9
Source documentation
The least length is bounded by every witnessed length.
```
theorem egyptianLength_le_of_expansion {a b k : ℕ}
    (h : ∃ n : Fin k → ℕ, IsEgyptianExpansion ((a : ℚ) / (b : ℚ)) n) :
    egyptianLength a b ≤ k := by
…
```
Mentions: OAI.Problem337.IsEgyptianExpansion, OAI.Problem337.egyptianLength

theorem OAI.Problem337.egyptianLength_attained_of_exists line 15

Source documentation

Existence is the only input needed to obtain a least expansion.

theorem egyptianLength_attained_of_exists {a b : ℕ}
    (h : ∃ k : ℕ, ∃ n : Fin k → ℕ,
      IsEgyptianExpansion ((a : ℚ) / (b : ℚ)) n) :
    ∃ n : Fin (egyptianLength a b) → ℕ,
      IsEgyptianExpansion ((a : ℚ) / (b : ℚ)) n := by
…

Mentions: OAI.Problem337.IsEgyptianExpansion, OAI.Problem337.egyptianLength

theorem OAI.Problem337.egyptianLength_le_max line 23
Source documentation
A pointwise length is bounded by the maximum over proper numerators.
```
theorem egyptianLength_le_max {a b : ℕ} (ha : 1 ≤ a) (hab : a < b) :
    egyptianLength a b ≤ maxEgyptianLength b := by
…
```
Mentions: OAI.Problem337.egyptianLength, OAI.Problem337.maxEgyptianLength
theorem OAI.Problem337.maxEgyptianLength_le_of_bound line 31
Source documentation
Uniform bounds on actual expansions descend to the maximum least length.
```
theorem maxEgyptianLength_le_of_bound {b K : ℕ}
    (h : ∀ a : ℕ, 1 ≤ a → a < b → egyptianLength a b ≤ K) :
    maxEgyptianLength b ≤ K := by
…
```
Mentions: OAI.Problem337.egyptianLength, OAI.Problem337.maxEgyptianLength