OAI/NumberTheory/EgyptianFractions/GoodNumeratorSets.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem337.goodNumeratorAux line 10

   Source documentation

   Finite backwards construction, indexed first by the number of remaining steps so that its recursion is structurally terminating.

   private def goodNumeratorAux
       (X : ℕ → ℝ) (I : ℕ → Finset ℕ) (res : ℕ → ℕ → ℕ → ℕ) :
       ℕ → ℕ → Finset ℕ
     | 0, j => Finset.Icc 1 ⌊X j⌋₊
     | n + 1, j => by
         classical
         exact (Finset.Icc 1 ⌊X j⌋₊).filter (fun u =>
           u ∈ goodNumeratorAux X I res n (j + 1) ∨
           ∃ i ∈ I j, res j i u = 0 ∨ res j i u ∈ goodNumeratorAux X I res n (j + 1))

2. theorem OAI.Problem337.goodNumeratorAux_subset line 20
3. theorem OAI.Problem337.exists_good_numerator_sets line 29

   Source documentation

   The good numerator sets exist for arbitrary finite indexed residue maps. No arithmetic distribution or analytic estimate is required for this recursion.

   theorem exists_good_numerator_sets
       (d : ℕ) (X : ℕ → ℝ) (I : ℕ → Finset ℕ) (res : ℕ → ℕ → ℕ → ℕ) :
       ∃ G : ℕ → Finset ℕ,
         (∀ j ≤ d, G j ⊆ Finset.Icc 1 ⌊X j⌋₊) ∧
         G d = Finset.Icc 1 ⌊X d⌋₊ ∧
         (∀ j < d, ∀ u : ℕ, u ∈ G j ↔
           u ∈ Finset.Icc 1 ⌊X j⌋₊ ∧
           (u ∈ G (j + 1) ∨ ∃ i ∈ I j, res j i u = 0 ∨ res j i u ∈ G (j + 1))) := by
   …