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.

[7324136828]

Hi @teorth,

Thanks for the clarification, and sorry about the misunderstanding.

I don’t currently have a copy of the book, so I was working from the Lean code and the surrounding context. I’ll plan to get a copy in the near future so I can check the original text more carefully when contributing.

I’ve also been out of academia for about six years, so I’m still getting back into the habit of reading and working with this kind of material. Please excuse the occasional clumsiness on my part.

Your explanation about the indexing makes perfect sense. I’m happy to update the PR so that the example uses 2 ^ n and remains faithful to the book.

Thanks again for the helpful explanation and for taking the time to review the PR.

Best,

Yuzhe Ni