OAI/NumberTheory/EgyptianFractions/FiniteExpansion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.finset_increasing_enumeration line 9

   Source documentation

   A finite collection of denominators has a canonical increasing enumeration.

   theorem finset_increasing_enumeration (s : Finset ℕ) :
       ∃ n : Fin s.card → ℕ, StrictMono n ∧
         (∀ m, (∃ i, n i = m) ↔ m ∈ s) ∧
         (∀ f : ℕ → ℚ, (∑ i, f (n i)) = ∑ m ∈ s, f m) := by
   …

2. theorem OAI.Problem337.finset_unit_fraction_representation line 26

   Source documentation

   Enumeration preserves a lower bound and the sum of unit fractions.

   theorem finset_unit_fraction_representation (s : Finset ℕ) (a : ℕ) (x : ℚ)
       (hpos : ∀ m ∈ s, a ≤ m) (hsum : (∑ m ∈ s, (1 : ℚ) / m) = x) :
       ∃ n : Fin s.card → ℕ, (∀ i, a ≤ n i) ∧ StrictMono n ∧
         (∑ i, (1 : ℚ) / n i) = x ∧
         (∀ m, (∃ i, n i = m) ↔ m ∈ s) := by
   …

3. theorem OAI.Problem337.finset_replace_unit_fraction line 39

   Source documentation

   Replacing one denominator by two fresh distinct denominators preserves the unit-fraction total and all other markers, while increasing cardinality by one.

   theorem finset_replace_unit_fraction (s : Finset ℕ) (d a b L : ℕ)
       (hd : d ∈ s) (ha : a ∉ s) (hb : b ∉ s) (hab : a ≠ b)
       (hpos : ∀ m ∈ s, L ≤ m) (haL : L ≤ a) (hbL : L ≤ b)
       (hsplit : (1 : ℚ) / a + 1 / b = 1 / d) :
       ∃ t : Finset ℕ, t.card = s.card + 1 ∧
         (∀ m ∈ t, L ≤ m) ∧
         (∑ m ∈ t, (1 : ℚ) / m) = ∑ m ∈ s, (1 : ℚ) / m ∧
         (∀ m ∈ s, m ≠ d → m ∈ t) := by
   …

4. theorem OAI.Problem337.increasing_unit_fraction_split line 72

   Source documentation

   Sequence form of the collision-free splitting construction.

   theorem increasing_unit_fraction_split {k : ℕ} (n : Fin k → ℕ)
       (hn : StrictMono n) (L : ℕ) (hpos : ∀ i, L ≤ n i)
       (d : Fin k) (a b : ℕ) (ha : ∀ i, n i ≠ a) (hb : ∀ i, n i ≠ b)
       (hab : a ≠ b) (haL : L ≤ a) (hbL : L ≤ b)
       (hsplit : (1 : ℚ) / a + 1 / b = 1 / n d) :
       ∃ n' : Fin (k + 1) → ℕ, (∀ i, L ≤ n' i) ∧ StrictMono n' ∧
         (∑ i, (1 : ℚ) / n' i) = ∑ i, (1 : ℚ) / n i ∧
         ∀ m, (∃ i, n i = m) → m ≠ n d → ∃ i, n' i = m := by
   …