Skip to content

Egyptian fraction underapproximations

17 fully proved

Egyptian Fraction

DefinitionNondecreasing Egyptian denominator tuples#✓fully proved

A tuple \((a_1, \dots, a_n)\) of natural numbers lies in \(\mathcal{E}_n^{\le}\) when \(2 \le a_1 \le a_2 \le \dots \le a_n\), that is, every \(a_i\) is at least \(2\) and the tuple is nondecreasing.

def IsNondecreasingEgyptian {n : ℕ} (a : Fin n → ℕ) : Prop :=
  (∀ i, 2 ≤ a i) ∧ Monotone a
Sources
  • Kovač–Tang, arXiv:2607.28387v2, lines 103–107.
Used by 6
Used byNondecreasing underapproximations have Egyptian denominator tuples · Egyptian underapproximations with nondecreasing denominators · Nondecreasing underapproximations have at least one term · A nondecreasing underapproximation stays below its target · The target of a nondecreasing underapproximation is positive · Strict underapproximations are nondecreasing underapproximations

DefinitionStrictly increasing Egyptian denominator tuples#✓fully proved

A tuple \((a_1, \dots, a_n)\) of natural numbers lies in \(\mathcal{E}_n^{<}\) when \(2 \le a_1 < a_2 < \dots < a_n\), that is, every \(a_i\) is at least \(2\) and the tuple is strictly increasing.

def IsStrictEgyptian {n : ℕ} (a : Fin n → ℕ) : Prop :=
  (∀ i, 2 ≤ a i) ∧ StrictMono a
Sources
  • Kovač–Tang, arXiv:2607.28387v2, lines 108–110.
Used by 6
Used byStrict underapproximations have strictly increasing Egyptian denominators · Egyptian underapproximations with strictly increasing denominators · Strict underapproximations have at least one term · A strict underapproximation stays below its target · The target of a strict underapproximation is positive · Strict underapproximations are nondecreasing underapproximations

DefinitionEgyptian underapproximations with nondecreasing denominators#✓fully proved

Let \(\lambda\) be a real number and \(a = (a_1, \dots, a_n)\) a tuple of natural numbers. Then \(a\) is a nondecreasing underapproximation of \(\lambda\) when \(n \ge 1\), \(\lambda > 0\), \(a\) lies in \(\mathcal{E}_n^{\le}\) (that is, \(2 \le a_1 \le \dots \le a_n\)), and \(\sum_{i=1}^{n} 1/a_i < \lambda\), the sum taken in the real numbers.

def IsNondecreasingUnderapproximation {n : ℕ} (target : ℝ) (a : Fin n → ℕ) : Prop :=
  0 < n ∧
    0 < target ∧
    IsNondecreasingEgyptian a ∧
    ∑ i, ((a i : ℝ)⁻¹) < target
Sources
  • Kovač–Tang, arXiv:2607.28387v2, lines 113–120; \(n \ge 1\) and \(\lambda > 0\) follow the paper's conventions.
Uses 1 · Used by 7
Statement usesNondecreasing Egyptian denominator tuples
Used byDenominators of a nondecreasing underapproximation are at least two · Nondecreasing underapproximations have Egyptian denominator tuples · Denominators of a nondecreasing underapproximation are nondecreasing · Nondecreasing underapproximations have at least one term · A nondecreasing underapproximation stays below its target · The target of a nondecreasing underapproximation is positive · Strict underapproximations are nondecreasing underapproximations

DefinitionEgyptian underapproximations with strictly increasing denominators#✓fully proved

Let \(\lambda\) be a real number and \(a = (a_1, \dots, a_n)\) a tuple of natural numbers. Then \(a\) is a strict underapproximation of \(\lambda\) when \(n \ge 1\), \(\lambda > 0\), \(a\) lies in \(\mathcal{E}_n^{<}\) (that is, \(2 \le a_1 < \dots < a_n\), so the unit fractions are distinct), and \(\sum_{i=1}^{n} 1/a_i < \lambda\), the sum taken in the real numbers.

def IsStrictUnderapproximation {n : ℕ} (target : ℝ) (a : Fin n → ℕ) : Prop :=
  0 < n ∧
    0 < target ∧
    IsStrictEgyptian a ∧
    ∑ i, ((a i : ℝ)⁻¹) < target
Sources
  • Kovač–Tang, arXiv:2607.28387v2, lines 113–120.
Uses 1 · Used by 7
Statement usesStrictly increasing Egyptian denominator tuples
Used byDenominators of a strict underapproximation are at least two · Strict underapproximations have strictly increasing Egyptian denominators · Strict underapproximations have at least one term · Denominators of a strict underapproximation increase strictly · A strict underapproximation stays below its target · The target of a strict underapproximation is positive · Strict underapproximations are nondecreasing underapproximations

Is Nondecreasing Underapproximation

TheoremNondecreasing underapproximations have at least one term#✓fully proved

Let \(n\) be a natural number, \(\lambda\) a real number and \(a_1, \dots, a_n\) natural numbers. If \((a_1, \dots, a_n)\) is a nondecreasing underapproximation of \(\lambda\), then \(n \ge 1\).

theorem nonempty {n : ℕ} {target : ℝ} {a : Fin n → ℕ}
    (h : IsNondecreasingUnderapproximation target a) : 0 < n
Uses 2
Statement usesEgyptian underapproximations with nondecreasing denominators
Proof usesNondecreasing Egyptian denominator tuples

TheoremThe target of a nondecreasing underapproximation is positive#✓fully proved

Let \(n\) be a natural number, \(\lambda\) a real number and \(a_1, \dots, a_n\) natural numbers. If \((a_1, \dots, a_n)\) is a nondecreasing underapproximation of \(\lambda\), then \(\lambda > 0\).

theorem target_pos {n : ℕ} {target : ℝ} {a : Fin n → ℕ}
    (h : IsNondecreasingUnderapproximation target a) : 0 < target
Uses 2
Statement usesEgyptian underapproximations with nondecreasing denominators
Proof usesNondecreasing Egyptian denominator tuples

TheoremNondecreasing underapproximations have Egyptian denominator tuples#✓fully proved

If \(a = (a_1, \dots, a_n)\) is a nondecreasing underapproximation of a real number \(\lambda\), then \(a\) lies in \(\mathcal{E}_n^{\le}\), that is, \(2 \le a_1 \le \dots \le a_n\).

theorem isNondecreasingEgyptian {n : ℕ} {target : ℝ} {a : Fin n → ℕ}
    (h : IsNondecreasingUnderapproximation target a) : IsNondecreasingEgyptian a
Uses 2 · Used by 2
Statement usesNondecreasing Egyptian denominator tuples · Egyptian underapproximations with nondecreasing denominators
Used byDenominators of a nondecreasing underapproximation are at least two · Denominators of a nondecreasing underapproximation are nondecreasing

TheoremDenominators of a nondecreasing underapproximation are at least two#✓fully proved

Let \(n\) be a natural number, \(\lambda\) a real number and \(a_1, \dots, a_n\) natural numbers. If \((a_1, \dots, a_n)\) is a nondecreasing underapproximation of \(\lambda\), then \(a_i \ge 2\) for every \(1 \le i \le n\).

theorem denominator_ge_two {n : ℕ} {target : ℝ} {a : Fin n → ℕ}
    (h : IsNondecreasingUnderapproximation target a) (i : Fin n) : 2 ≤ a i
Uses 2
Statement usesEgyptian underapproximations with nondecreasing denominators
Proof usesNondecreasing underapproximations have Egyptian denominator tuples

TheoremDenominators of a nondecreasing underapproximation are nondecreasing#✓fully proved

Let \(n\) be a natural number, \(\lambda\) a real number and \(a_1, \dots, a_n\) natural numbers. If \((a_1, \dots, a_n)\) is a nondecreasing underapproximation of \(\lambda\), then \(a_i \le a_j\) whenever \(1 \le i \le j \le n\).

theorem monotone {n : ℕ} {target : ℝ} {a : Fin n → ℕ}
    (h : IsNondecreasingUnderapproximation target a) : Monotone a
Uses 2
Statement usesEgyptian underapproximations with nondecreasing denominators
Proof usesNondecreasing underapproximations have Egyptian denominator tuples

TheoremA nondecreasing underapproximation stays below its target#✓fully proved

Let \(n\) be a natural number, \(\lambda\) a real number and \(a_1, \dots, a_n\) natural numbers. If \((a_1, \dots, a_n)\) is a nondecreasing underapproximation of \(\lambda\), then \(\sum_{i=1}^{n} 1/a_i < \lambda\).

theorem sum_lt {n : ℕ} {target : ℝ} {a : Fin n → ℕ}
    (h : IsNondecreasingUnderapproximation target a) :
    ∑ i, ((a i : ℝ)⁻¹) < target
Uses 2
Statement usesEgyptian underapproximations with nondecreasing denominators
Proof usesNondecreasing Egyptian denominator tuples

Is Strict Underapproximation

TheoremStrict underapproximations have at least one term#✓fully proved

Let \(n\) be a natural number, \(\lambda\) a real number and \(a_1, \dots, a_n\) natural numbers. If \((a_1, \dots, a_n)\) is a strict underapproximation of \(\lambda\), then \(n \ge 1\).

theorem nonempty {n : ℕ} {target : ℝ} {a : Fin n → ℕ}
    (h : IsStrictUnderapproximation target a) : 0 < n
Uses 2 · Used by 1
Statement usesEgyptian underapproximations with strictly increasing denominators
Proof usesStrictly increasing Egyptian denominator tuples
Used byStrict underapproximations are nondecreasing underapproximations

TheoremThe target of a strict underapproximation is positive#✓fully proved

Let \(n\) be a natural number, \(\lambda\) a real number and \(a_1, \dots, a_n\) natural numbers. If \((a_1, \dots, a_n)\) is a strict underapproximation of \(\lambda\), then \(\lambda > 0\).

theorem target_pos {n : ℕ} {target : ℝ} {a : Fin n → ℕ}
    (h : IsStrictUnderapproximation target a) : 0 < target
Uses 2 · Used by 1
Statement usesEgyptian underapproximations with strictly increasing denominators
Proof usesStrictly increasing Egyptian denominator tuples
Used byStrict underapproximations are nondecreasing underapproximations

TheoremStrict underapproximations have strictly increasing Egyptian denominators#✓fully proved

If \(a = (a_1, \dots, a_n)\) is a strict underapproximation of a real number \(\lambda\), then \(a\) lies in \(\mathcal{E}_n^{<}\), that is, \(2 \le a_1 < \dots < a_n\).

theorem isStrictEgyptian {n : ℕ} {target : ℝ} {a : Fin n → ℕ}
    (h : IsStrictUnderapproximation target a) : IsStrictEgyptian a
Uses 2 · Used by 3
Statement usesStrictly increasing Egyptian denominator tuples · Egyptian underapproximations with strictly increasing denominators
Used byDenominators of a strict underapproximation are at least two · Denominators of a strict underapproximation increase strictly · Strict underapproximations are nondecreasing underapproximations

TheoremDenominators of a strict underapproximation are at least two#✓fully proved

Let \(n\) be a natural number, \(\lambda\) a real number and \(a_1, \dots, a_n\) natural numbers. If \((a_1, \dots, a_n)\) is a strict underapproximation of \(\lambda\), then \(a_i \ge 2\) for every \(1 \le i \le n\).

theorem denominator_ge_two {n : ℕ} {target : ℝ} {a : Fin n → ℕ}
    (h : IsStrictUnderapproximation target a) (i : Fin n) : 2 ≤ a i
Uses 2
Statement usesEgyptian underapproximations with strictly increasing denominators
Proof usesStrict underapproximations have strictly increasing Egyptian denominators

TheoremDenominators of a strict underapproximation increase strictly#✓fully proved

Let \(n\) be a natural number, \(\lambda\) a real number and \(a_1, \dots, a_n\) natural numbers. If \((a_1, \dots, a_n)\) is a strict underapproximation of \(\lambda\), then \(a_i < a_j\) whenever \(1 \le i < j \le n\).

theorem strictMono {n : ℕ} {target : ℝ} {a : Fin n → ℕ}
    (h : IsStrictUnderapproximation target a) : StrictMono a
Uses 2
Statement usesEgyptian underapproximations with strictly increasing denominators
Proof usesStrict underapproximations have strictly increasing Egyptian denominators

TheoremA strict underapproximation stays below its target#✓fully proved

Let \(n\) be a natural number, \(\lambda\) a real number and \(a_1, \dots, a_n\) natural numbers. If \((a_1, \dots, a_n)\) is a strict underapproximation of \(\lambda\), then \(\sum_{i=1}^{n} 1/a_i < \lambda\), the sum taken in the real numbers.

theorem sum_lt {n : ℕ} {target : ℝ} {a : Fin n → ℕ}
    (h : IsStrictUnderapproximation target a) :
    ∑ i, ((a i : ℝ)⁻¹) < target
Uses 2 · Used by 1
Statement usesEgyptian underapproximations with strictly increasing denominators
Proof usesStrictly increasing Egyptian denominator tuples
Used byStrict underapproximations are nondecreasing underapproximations

TheoremStrict underapproximations are nondecreasing underapproximations#✓fully proved

Let \(n\) be a natural number, \(\lambda\) a real number and \(a_1, \dots, a_n\) natural numbers. If \((a_1, \dots, a_n)\) is a strict underapproximation of \(\lambda\), then it is also a nondecreasing underapproximation of \(\lambda\).

This is the inclusion of strictly increasing denominator tuples among nondecreasing ones, together with the same bound on the sum of reciprocals.

theorem toIsNondecreasingUnderapproximation {n : ℕ} {target : ℝ} {a : Fin n → ℕ}
    (h : IsStrictUnderapproximation target a) :
    IsNondecreasingUnderapproximation target a
Uses 8
Statement usesEgyptian underapproximations with nondecreasing denominators · Egyptian underapproximations with strictly increasing denominators
Proof usesNondecreasing Egyptian denominator tuples · Strictly increasing Egyptian denominator tuples · Strict underapproximations have strictly increasing Egyptian denominators · Strict underapproximations have at least one term · A strict underapproximation stays below its target · The target of a strict underapproximation is positive

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.