MarkerCoverage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.marker_length_ge_three line 10
Source documentation
An expansion containing a proper unit fraction needs at least three terms.
```
theorem marker_length_ge_three {k m : ℕ} (hm : m ∈ D k) : 3 ≤ k := by
…
```
Mentions: OAI.Problem337.D

theorem OAI.Problem337.D_mono_of_padding line 44

Source documentation

Exact marker padding implies monotonicity even at the empty small lengths.

theorem D_mono_of_padding
    (padding : ∀ r : ℕ, 3 ≤ r → ∀ n : Fin r → ℕ, IsOneExpansion n →
      ∀ m : ℕ, (∃ i : Fin r, n i = m) →
        ∃ n' : Fin (r + 1) → ℕ,
          IsOneExpansion n' ∧ ∃ i : Fin (r + 1), n' i = m) :
    Monotone D := by
…

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

theorem OAI.Problem337.bounded_markers_eventually line 60

Source documentation

Finitely many markers all occur at every sufficiently large exact length.

theorem bounded_markers_eventually
    (hmono : Monotone D)
    (occurs : ∀ m : ℕ, 2 ≤ m → ∃ k : ℕ, m ∈ D k)
    (B : ℕ) :
    ∃ K : ℕ, ∀ k : ℕ, K ≤ k → ∀ m : ℕ, 2 ≤ m → m ≤ B → m ∈ D k := by
…

Mentions: OAI.Problem337.D