MarkerTelescope.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.reciprocal_telescope line 10

Source documentation

The telescoping unit-fraction expansion of the complement of 1/m.

theorem reciprocal_telescope (j : ℕ) :
    (∑ i ∈ Finset.range j, (1 : ℚ) / (((i + 1) * (i + 2) : ℕ) : ℚ)) =
      1 - 1 / ((j + 1 : ℕ) : ℚ) := by
…

theorem OAI.Problem337.consecutive_product_gap line 24
Source documentation
Consecutive products grow strictly and have gaps larger than one.
```
theorem consecutive_product_gap {a b : ℕ} (ha : 1 ≤ a) (hab : a < b) :
    a * (a + 1) + 1 < b * (b + 1) := by
…
```
theorem OAI.Problem337.consecutive_product_succ_ne line 32
Source documentation
If the reserved marker collides with a telescoping denominator, its successor does not.
```
theorem consecutive_product_succ_ne {a b : ℕ} (ha : 1 ≤ a) (hb : 1 ≤ b) :
    a * (a + 1) + 1 ≠ b * (b + 1) := by
…
```