Update examples in Section 5.1 for clarity

[7324136828]

No description provided.

[teorth]

Thanks for the PR, and welcome!

You've spotted a genuine mismatch — the docstring and the Lean really don't agree. But I think the fix should go the other way round: the docstring is right and the Lean term is wrong.

The text in §5.1 reads:

The sequence $1$, $2$, $4$, $8$, $16, \dots$ is not $\eps$-steady for any $\eps$.

The house convention in this repo is that the Lean statement is the thing that should be made faithful to the book, and docstrings record what the book says. So rather than changing the docstring to 2, 4, 8, ..., the example should become:

example (ε:ℚ) : ¬ ε.Steady ((fun n:ℕ ↦ (2 ^ n:ℚ) ):Sequence) := by sorry

The neighbouring example is a good check that the indexing works out: (10:ℚ) ^ (-(n:ℤ)-1) gives 0.1 at n = 0, matching the book's first term, so 2 ^ n likewise gives 1 at n = 0.

If you'd like to update the PR along those lines that'd be great — otherwise I'm happy to take it from here. Either way, thanks for reading closely enough to catch it.