BackwardExpansions.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.Descent.UnitListAtMost line 10
Source documentation
Length-bounded positive unit-fraction lists; repetitions are allowed at this stage of the density construction.
```
def UnitListAtMost (x : ℚ) (B : ℕ) : Prop :=
…
```
theorem OAI.Problem337.Descent.UnitListAtMost.mono line 14
theorem OAI.Problem337.Descent.unitListAtMost_zero line 19
theorem OAI.Problem337.Descent.UnitListAtMost.change_factor line 24
theorem OAI.Problem337.Descent.UnitListAtMost.residue_step line 33

theorem OAI.Problem337.Descent.backward_good_set_expansions line 47

Source documentation

Backward propagation of bounded expansions through good numerator sets. The hypotheses encode exactly the inherited-membership and successful-residue alternatives in the dense-family construction.

theorem backward_good_set_expansions
    (M d B : ℕ) (Q : ℕ → ℕ) (G : ℕ → Set ℕ)
    (hM : 0 < M) (hQ : ∀ j, j ≤ d → 0 < Q j)
    (hdiv : ∀ j, j < d → Q (j + 1) ∣ Q j)
    (hterminal : ∀ u ∈ G d,
      UnitListAtMost ((u : ℚ) / (M * Q d : ℕ)) B)
    (hstep : ∀ j, j < d → ∀ u ∈ G j,
      u ∈ G (j + 1) ∨ ∃ t z h : ℕ,
        0 < t ∧ t ∣ M ∧ 0 < z ∧ Q j * t + h = u * z ∧
          (h = 0 ∨ h ∈ G (j + 1))) :
    ∀ j, j ≤ d → ∀ u ∈ G j,
      UnitListAtMost ((u : ℚ) / (M * Q j : ℕ)) (B + (d - j)) := by
…

Mentions: OAI.Problem337.Descent.UnitListAtMost

theorem OAI.Problem337.Descent.UnitListAtMost.denominators_two line 79
Source documentation
If a propagated fraction is below one, its positive denominators are all at least two, as required by the dense-family interface.
```
theorem UnitListAtMost.denominators_two {x : ℚ} {B : ℕ}
    (H : UnitListAtMost x B) (hx : x < 1) :
    ∃ k : ℕ, k ≤ B ∧ ∃ n : Fin k → ℕ,
      (∀ i, 2 ≤ n i) ∧ (∑ i : Fin k, (1 : ℚ) / (n i : ℚ)) = x := by
…
```
Mentions: OAI.Problem337.Descent.UnitListAtMost