OAI/NumberTheory/EgyptianFractions/DenominatorBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.ordered_unit_tail_bound line 11
2. theorem OAI.Problem337.denominator_le_prefix_product line 49
3. theorem OAI.Problem337.ordered_unit_denominator_bound line 65

   Source documentation

   The coordinate estimate only needs weak ordering, so it also applies to expansions with repeated denominators.

   theorem ordered_unit_denominator_bound {k : ℕ} (n : Fin k → ℕ)
       (hn : ∀ i, 0 < n i) (hmono : Monotone n)
       (hsum : (∑ j : Fin k, (1 : ℚ) / n j) = 1) :
       ∀ i : Fin k, n i ≤ k ^ (2 ^ i.val) := by
   …

4. theorem OAI.Problem337.one_expansion_denominator_bound line 109