OAI/NumberTheory/EgyptianFractions/BinaryExpansion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.binary_unit_fraction_list line 10

   Source documentation

   Binary digits give a short expansion whenever a large power of two is available as a divisor of the denominator.

   theorem binary_unit_fraction_list (u M a : ℕ) (huM : u < M)
       (hu : u < 2 ^ (a + 1)) (hdiv : 2 ^ a ∣ M) :
       ∃ l : List ℕ, (∀ d ∈ l, 2 ≤ d) ∧ l.length ≤ a + 1 ∧
         (l.map (fun d : ℕ => (1 : ℚ) / (d : ℚ))).sum = (u : ℚ) / M := by
   …