PrefixGrowth.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.prefix_growth_bound line 7

Source documentation

The elementary growth estimate for successive products of denominators.

theorem prefix_growth_bound (k t : ℕ) (P : ℕ → ℕ)
    (hzero : P 0 = 1)
    (hstep : ∀ i < t, P (i + 1) ≤ k * (P i) ^ 2) :
    ∀ i ≤ t, P i ≤ k ^ (2 ^ i - 1) := by
…

theorem OAI.Problem337.denominator_growth_bound line 30
Source documentation
The bound for the next denominator follows from the prefix-product bound.
```
theorem denominator_growth_bound (k i P n : ℕ)
    (hP : P ≤ k ^ (2 ^ i - 1)) (hn : n ≤ k * P) :
    n ≤ k ^ (2 ^ i) := by
…
```