From ba44bcb0ffc322e1be531f1dae2de5c6e85f90c9 Mon Sep 17 00:00:00 2001 From: Ada Alakbarova Date: Sun, 8 Mar 2026 19:30:12 +0100 Subject: [PATCH] fix(L9L5): fix typo `TermLtSum` -> `TermLeSum` --- Game/Levels/L9Levels/L05_BddOfConv.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Game/Levels/L9Levels/L05_BddOfConv.lean b/Game/Levels/L9Levels/L05_BddOfConv.lean index 6b8bd9f..31747d5 100644 --- a/Game/Levels/L9Levels/L05_BddOfConv.lean +++ b/Game/Levels/L9Levels/L05_BddOfConv.lean @@ -106,13 +106,13 @@ This tells us something profound: **convergent sequences can't escape to infinit 1. **Two-region strategy** - You split the natural numbers into two parts: - Eventually (n ≥ N): where convergence gives you control - - Initially (n < N): where you used your TermLtSum theorem + - Initially (n < N): where you used your TermLeSum theorem 2. **Constructing clever bounds** - You built `M = 2*|L| + ∑ k ∈ range N, |a k|`, which elegantly captures both regions in a single expression 3. **Case analysis** - You used `by_cases` to handle the two regions separately, applying the appropriate bound for each -4. **Connecting theorems** - You saw how `TermLtSum` from Level 1 became an essential tool for handling finitely many terms +4. **Connecting theorems** - You saw how `TermLeSum` from Level 1 became an essential tool for handling finitely many terms ## Why This Matters @@ -127,7 +127,7 @@ The boundedness of convergent sequences is fundamental throughout mathematics: Notice we assumed `L ≠ 0` in this proof. The case where `L = 0` is left as an exercise, but the idea is similar: - Use convergence with `ε = 1` to bound terms eventually by `1` -- Handle the finitely many initial terms with TermLtSum +- Handle the finitely many initial terms with TermLeSum - The bound becomes `M = 1 + ∑ k ∈ range N, |a k|` ## Looking Ahead