GreedyStep.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.greedy_step_data line 8

Source documentation

Arithmetic data for one step of the greedy Egyptian fraction algorithm.

theorem greedy_step_data (a b : ℕ) (ha : 0 < a) (hab : a < b)
    (hr : b % a ≠ 0) :
    ∃ z c : ℕ, 2 ≤ z ∧ 0 < c ∧ c < a ∧ c < b * z ∧
      (a : ℚ) / b = 1 / (z : ℚ) + (c : ℚ) / (b * z : ℕ) ∧
      (c : ℚ) / (b * z : ℕ) < 1 / (z : ℚ) := by
…

theorem OAI.Problem337.greedy_terminal_data line 40

Source documentation

The terminal, divisible case of the greedy algorithm.

theorem greedy_terminal_data (a b : ℕ) (ha : 0 < a) (hab : a < b)
    (hr : b % a = 0) :
    2 ≤ b / a ∧ (a : ℚ) / b = 1 / (b / a : ℕ) := by
…

theorem OAI.Problem337.denominators_gt_of_sum_lt line 59

Source documentation

If a reciprocal sum is below 1/z, every denominator exceeds z.

theorem denominators_gt_of_sum_lt {k z : ℕ} (n : Fin k → ℕ)
    (hn : ∀ i, 0 < n i) (hz : 0 < z)
    (hs : (∑ i : Fin k, (1 : ℚ) / (n i : ℚ)) < 1 / (z : ℚ)) :
    ∀ i, z < n i := by
…