MarkerExplicitBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.marker_occurs_at_length_of_lt line 13
Source documentation
A marker smaller than the prescribed length always occurs at that exact length.
```
theorem marker_occurs_at_length_of_lt {m k : ℕ} (hm : 2 ≤ m) (hmk : m < k) :
    m ∈ D k := by
…
```
Mentions: OAI.Problem337.D
theorem OAI.Problem337.bounded_markers_at_explicit_length line 19
Source documentation
The qualitative finite-exception cutoff can be chosen explicitly.
```
theorem bounded_markers_at_explicit_length {B k : ℕ} (hBk : B < k) :
    ∀ m : ℕ, 2 ≤ m → m ≤ B → m ∈ D k := by
…
```
Mentions: OAI.Problem337.D
theorem OAI.Problem337.length_le_first_missing line 25
Source documentation
A basic unconditional lower bound for the first missing denominator.
```
theorem length_le_first_missing (k : ℕ) : k ≤ v k := by
…
```
Mentions: OAI.Problem337.v
theorem OAI.Problem337.first_missing_tendsto_atTop line 32