OAI/NumberTheory/EgyptianFractions/FixedSumFinite.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem337.OrderedUnitSums line 11

   Source documentation

   Ordered positive denominator tuples with a prescribed rational sum. Repetitions are allowed.

   def OrderedUnitSums (k : ℕ) (x : ℚ) : Set (Fin k → ℕ) :=
   …

2. lemma OAI.Problem337.ordered_unit_sum_pos line 14
3. lemma OAI.Problem337.ordered_unit_first_bound line 22
4. theorem OAI.Problem337.ordered_unit_sums_finite line 45

   Source documentation

   For every fixed length and fixed rational total, there are only finitely many nondecreasing tuples of positive unit-fraction denominators.

   theorem ordered_unit_sums_finite (k : ℕ) (x : ℚ) :
       Set.Finite (OrderedUnitSums k x) := by
   …

   Mentions: OAI.Problem337.OrderedUnitSums