Odd greedy algorithm for Egyptian fractions

DefinitionOdd greedy choice#✓fully proved

For a rational number \(r\) and a natural number \(d\), \(d\) is the odd greedy choice at \(r\) when \(r > 0\), \(d\) is positive and odd, \(1/d \le r\), and \(d \le e\) for every positive odd natural number \(e\) with \(1/e \le r\). Equivalently, \(1/d\) is the largest unit fraction with odd denominator that does not exceed \(r\).

def IsOddGreedyChoice (r : ℚ) (d : ℕ) : Prop :=
  0 < r ∧ 0 < d ∧ Odd d ∧ (1 : ℚ) / (d : ℚ) ≤ r ∧
    ∀ e : ℕ, 0 < e → Odd e → (1 : ℚ) / (e : ℚ) ≤ r → d ≤ e

Used by 8

Used byThe odd greedy unit fraction does not exceed the remainder · Characterization of the odd greedy choice · Odd greedy choice at a fraction · The odd greedy choice is minimal · The odd greedy choice is odd · The odd greedy choice is positive · The odd greedy choice needs a positive remainder · Uniqueness of the odd greedy choice

TheoremThe odd greedy choice needs a positive remainder#✓fully proved

If \(d\) is the odd greedy choice at a rational number \(r\), then \(r > 0\).

theorem IsOddGreedyChoice.pos_r {r : ℚ} {d : ℕ}
    (h : IsOddGreedyChoice r d) : 0 < r

Uses 1 · Used by 1

Statement usesOdd greedy choice

Used byCharacterization of the odd greedy choice

TheoremThe odd greedy choice is positive#✓fully proved

If \(d\) is the odd greedy choice at a rational number \(r\), then \(d > 0\).

theorem IsOddGreedyChoice.pos_d {r : ℚ} {d : ℕ}
    (h : IsOddGreedyChoice r d) : 0 < d

Uses 1 · Used by 2

Statement usesOdd greedy choice

Used byCharacterization of the odd greedy choice · Uniqueness of the odd greedy choice

TheoremThe odd greedy choice is odd#✓fully proved

If \(d\) is the odd greedy choice at a rational number \(r\), then \(d\) is odd.

theorem IsOddGreedyChoice.odd {r : ℚ} {d : ℕ}
    (h : IsOddGreedyChoice r d) : Odd d

Uses 1 · Used by 2

Statement usesOdd greedy choice

Used byCharacterization of the odd greedy choice · Uniqueness of the odd greedy choice

TheoremThe odd greedy unit fraction does not exceed the remainder#✓fully proved

If \(d\) is the odd greedy choice at a rational number \(r\), then \(1/d \le r\).

theorem IsOddGreedyChoice.inv_le {r : ℚ} {d : ℕ}
    (h : IsOddGreedyChoice r d) : (1 : ℚ) / (d : ℚ) ≤ r

Uses 1 · Used by 2

Statement usesOdd greedy choice

Used byCharacterization of the odd greedy choice · Uniqueness of the odd greedy choice

TheoremThe odd greedy choice is minimal#✓fully proved

If \(d\) is the odd greedy choice at a rational number \(r\), then \(d \le e\) for every positive odd natural number \(e\) with \(1/e \le r\).

theorem IsOddGreedyChoice.min {r : ℚ} {d e : ℕ}
    (h : IsOddGreedyChoice r d) (he : 0 < e) (hodd : Odd e)
    (hle : (1 : ℚ) / (e : ℚ) ≤ r) : d ≤ e

Uses 1 · Used by 2

Statement usesOdd greedy choice

Used byCharacterization of the odd greedy choice · Uniqueness of the odd greedy choice

TheoremUniqueness of the odd greedy choice#✓fully proved

If \(d\) and \(d'\) are both odd greedy choices at the same rational number \(r\), then \(d = d'\).

theorem IsOddGreedyChoice.unique {r : ℚ} {d d' : ℕ}
    (h : IsOddGreedyChoice r d) (h' : IsOddGreedyChoice r d') :
    d = d'

Uses 5

Statement usesOdd greedy choice

Proof usesThe odd greedy unit fraction does not exceed the remainder · The odd greedy choice is minimal · The odd greedy choice is odd · The odd greedy choice is positive

TheoremCharacterization of the odd greedy choice#✓fully proved

A natural number \(d\) is the odd greedy choice at a rational number \(r\) if and only if \(r > 0\) and \(d\) is the least element of the set of positive odd natural numbers \(e\) with \(1/e \le r\).

theorem isOddGreedyChoice_iff {r : ℚ} {d : ℕ} :
    IsOddGreedyChoice r d ↔
      0 < r ∧ IsLeast {e : ℕ | 0 < e ∧ Odd e ∧ (1 : ℚ) / (e : ℚ) ≤ r} d

Uses 6

Statement usesOdd greedy choice

Proof usesThe odd greedy unit fraction does not exceed the remainder · The odd greedy choice is minimal · The odd greedy choice is odd · The odd greedy choice is positive · The odd greedy choice needs a positive remainder

TheoremEven sums of odd unit fractions have even numerator#●ready to prove

Let \(m\) be an even natural number and let \(d_1, \dots, d_m\) be odd natural numbers. If integers \(a\) and \(b\) with \(b \ne 0\) satisfy \(a/b = \sum_{i=1}^{m} 1/d_i\), then \(a\) is even.

theorem_wanted even_num_of_even_sum_unit_fractions
    (m : ℕ) (hm : Even m) (d : Fin m → ℕ)
    (hd : ∀ i, Odd (d i)) (a b : ℤ) (hb : b ≠ 0)
    (h : (a : ℚ) / (b : ℚ) = ∑ i, (1 : ℚ) / (d i : ℚ)) :
    Even a

Sources

• Joel Louwsma and Joseph Martino, "Rational Numbers with Two-Term Odd Greedy Expansion", Proposition 1.

TheoremOdd greedy choice at a fraction#●ready to prove

Let \(n\) and \(d\) be positive natural numbers and let \(x_1\) be an odd natural number. Then \(x_1\) is the odd greedy choice at \(n/d\) (the first denominator of the odd greedy expansion of \(n/d\)) if and only if \(d \le n x_1\) and \(n x_1 < d + 2n\), that is, \(0 \le n x_1 - d < 2n\) in the integers.

theorem_wanted isOddGreedyChoice_iff (n d x1 : ℕ)
    (hn : 0 < n) (hd : 0 < d) (hx : Odd x1) :
    MetaMathlibExt.IsOddGreedyChoice ((n : ℚ) / (d : ℚ)) x1 ↔
      d ≤ n * x1 ∧ n * x1 < d + 2 * n

Sources

• Joel Louwsma and Joseph Martino, "Rational Numbers with Two-Term Odd Greedy Expansion", Lemma 2.

Uses 1

Statement usesOdd greedy choice

8 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.