GoodSetRecursion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.backwardFiniteSequence line 9
Source documentation
A finite backwards recursion, extended constantly beyond its terminal index.
```
def backwardFiniteSequence {α : Type*} (d : ℕ) (terminal : α)
    (step : ℕ → α → α) (j : ℕ) : α :=
…
```
theorem OAI.Problem337.backwardFiniteSequence_terminal line 13
theorem OAI.Problem337.backwardFiniteSequence_step line 17

theorem OAI.Problem337.exists_backward_good_sets line 30

Source documentation

The exact finite good-set recurrence used in the residue descent always has a solution. Bounds may be arbitrary; monotonicity is not needed here.

theorem exists_backward_good_sets (d : ℕ) (bound : ℕ → ℕ)
    (indices : ℕ → Finset ℕ) (residue : ℕ → ℕ → ℕ → ℕ) :
    ∃ G : ℕ → Finset ℕ,
      (∀ j ≤ d, G j ⊆ Finset.Icc 1 (bound j)) ∧
      G d = Finset.Icc 1 (bound d) ∧
      (∀ j < d, ∀ u : ℕ, u ∈ G j ↔
        u ∈ Finset.Icc 1 (bound j) ∧
          (u ∈ G (j + 1) ∨ ∃ i ∈ indices j,
            residue j i u = 0 ∨ residue j i u ∈ G (j + 1))) := by
…