OAI/NumberTheory/EgyptianFractions/Distinctize.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.Distinctize.duplicate_split line 10

   Source documentation

   Takenouchi's two-term replacement increases the denominator sum.

   theorem duplicate_split (d : ℕ) (hd : 3 ≤ d) :
       ∃ u v : ℕ, 2 ≤ u ∧ 2 ≤ v ∧
         (2 : ℚ) / d = 1 / (u : ℚ) + 1 / (v : ℚ) ∧ 2 * d < u + v := by
   …

   Mentions: OAI.Problem337.v

2. theorem OAI.Problem337.Distinctize.sum_update_balance line 39

   Source documentation

   Updating one coordinate changes a sum by the corresponding summand.

   theorem sum_update_balance {k : ℕ} (n : Fin k → ℕ) (g : ℕ → ℚ)
       (i : Fin k) (u : ℕ) :
       (∑ j, g (Function.update n i u j)) + g (n i) =
         (∑ j, g (n j)) + g u := by
   …

3. theorem OAI.Problem337.Distinctize.two_updates line 52

   Source documentation

   Replace equal coordinates by a two-term replacement.

   theorem two_updates {k : ℕ} (n : Fin k → ℕ) (g : ℕ → ℚ)
       (i j : Fin k) (hij : i ≠ j) (u v : ℕ) :
       (∑ a, g (Function.update (Function.update n i u) j v a)) +
           g (n i) + g (n j) =
         (∑ a, g (n a)) + g u + g v := by
   …

   Mentions: OAI.Problem337.v

4. theorem OAI.Problem337.Distinctize.distinctize_of_finite line 63

   Source documentation

   Takenouchi's finite maximization argument removes all repetitions.

   theorem distinctize_of_finite {k : ℕ} {x : ℚ} (_hx : 0 < x) (hxone : x < 1)
       (hfinite : Set.Finite {n : Fin k → ℕ | (∀ i, 0 < n i) ∧ Monotone n ∧
         (∑ i, (1 : ℚ) / (n i : ℚ)) = x})
       (n : Fin k → ℕ) (hn : ∀ i, 0 < n i)
       (hsum : (∑ i, (1 : ℚ) / (n i : ℚ)) = x) :
       ∃ d : Fin k → ℕ, (∀ i, 2 ≤ d i) ∧ StrictMono d ∧
         (∑ i, (1 : ℚ) / (d i : ℚ)) = x := by
   …

5. theorem OAI.Problem337.Distinctize.distinctize line 143

   Source documentation

   Every positive rational unit-fraction list of total less than one has a strictly increasing representation with exactly the same number of terms.

   theorem distinctize {k : ℕ} {x : ℚ} (hx : 0 < x) (hxone : x < 1)
       (n : Fin k → ℕ) (hn : ∀ i, 0 < n i)
       (hsum : (∑ i, (1 : ℚ) / (n i : ℚ)) = x) :
       ∃ d : Fin k → ℕ, (∀ i, 2 ≤ d i) ∧ StrictMono d ∧
         (∑ i, (1 : ℚ) / (d i : ℚ)) = x :=
   …