OAI/NumberTheory/EgyptianFractions/MissingSemantics.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.denominator_mem_D_le_of_bound line 9

   Source documentation

   The coordinate bound also bounds every denominator occurring in an exact-length expansion.

   theorem denominator_mem_D_le_of_bound
       (hbound : ∀ k : ℕ, ∀ n : Fin k → ℕ, IsOneExpansion n →
         ∀ i : Fin k, n i ≤ k ^ (2 ^ i.val))
       {k m : ℕ} (hm : m ∈ D k) : m ≤ k ^ (2 ^ (k - 1)) := by
   …

   Mentions: OAI.Problem337.IsOneExpansion, OAI.Problem337.D

2. theorem OAI.Problem337.missing_denominator_semantics_of_bound line 19

   Source documentation

   All first-missing-denominator semantics follow from the coordinate bound.

   theorem missing_denominator_semantics_of_bound
       (hbound : ∀ k : ℕ, ∀ n : Fin k → ℕ, IsOneExpansion n →
         ∀ i : Fin k, n i ≤ k ^ (2 ^ i.val)) :
       ∀ k : ℕ,
     Set.Finite (D k) ∧
     (∃ m : ℕ, m ∈ missingDenominators k) ∧
     2 ≤ v k ∧ v k ∉ D k ∧
     (∀ m : ℕ, 2 ≤ m → m < v k → m ∈ D k) ∧
     (1 ≤ k → v k ≤ 1 + k ^ (2 ^ (k - 1))) := by
   …

   Mentions: OAI.Problem337.IsOneExpansion, OAI.Problem337.D, OAI.Problem337.missingDenominators, OAI.Problem337.v