From 4c2ae43962f58c3a50ed4e2e24c8f6e7c5d31712 Mon Sep 17 00:00:00 2001 From: ovo-Tim Date: Tue, 10 Feb 2026 23:26:05 +0800 Subject: [PATCH 1/3] feat: port to leanprover/lean4:v4.26.0 --- .claude/settings.local.json | 12 + .i18n/en/Game.pot | 19223 ++++++++++------ Game/CustomTactic/Linarith.lean | 3 +- Game/Levels/L10Levels/L06_Prod.lean | 2 +- Game/Levels/L11Levels/L01_IsCauchyOfLim.lean | 2 +- Game/Levels/L11Levels/L02_IsCauchyOfSum.lean | 2 +- Game/Levels/L11Levels/L03_IsBddOfCauchy.lean | 2 +- Game/Levels/L15Levels/L01_check.lean | 6 +- .../Levels/L15Levels/L01_completenessAlt.lean | 8 +- Game/Levels/L18Pset/L02.lean | 2 +- Game/Levels/L18Pset/L04.lean | 5 +- Game/Levels/L19Levels/L03.lean | 2 +- Game/Levels/L20Levels/L03.lean | 2 +- Game/Levels/L21Levels/L08.lean | 2 +- Game/Levels/L22Levels/L02.lean | 4 +- Game/Levels/L23Levels/L02.lean | 2 +- Game/Levels/L23Levels/L03.lean | 4 +- Game/Levels/L24Levels/L02.lean | 2 +- Game/Levels/L4Levels/L01_NonConverge.lean | 16 +- Game/Levels/L4Pset/L4Pset1.lean | 16 +- Game/Levels/L6Levels/L00_SumOfSeqs.lean | 2 +- Game/Levels/L6Pset/L6Pset4.lean | 2 +- Game/Levels/L7Levels/L00_Uniqueness.lean | 2 +- Game/Levels/L7Levels/L01_Eventually.lean | 2 +- Game/Levels/L7Pset/L7Pset1.lean | 2 +- Game/Levels/L7Pset/L7Pset3.lean | 4 +- Game/Metadata.lean | 2 +- lake-manifest.json | 34 +- lakefile.lean | 5 +- lean-toolchain | 2 +- 30 files changed, 12300 insertions(+), 7074 deletions(-) create mode 100644 .claude/settings.local.json diff --git a/.claude/settings.local.json b/.claude/settings.local.json new file mode 100644 index 0000000..233bdb0 --- /dev/null +++ b/.claude/settings.local.json @@ -0,0 +1,12 @@ +{ + "permissions": { + "allow": [ + "Bash(lake build:*)", + "Bash(wait:*)", + "Bash(git ls-remote:*)", + "Bash(lake update:*)", + "Bash(find:*)", + "Bash(grep:*)" + ] + } +} diff --git a/.i18n/en/Game.pot b/.i18n/en/Game.pot index 7b94a3b..80c505d 100644 --- a/.i18n/en/Game.pot +++ b/.i18n/en/Game.pot @@ -1,689 +1,870 @@ msgid "" -msgstr "Project-Id-Version: Game v4.23.0-rc2\n" +msgstr "Project-Id-Version: Game v4.26.0\n" "Report-Msgid-Bugs-To: \n" -"POT-Creation-Date: 2025-12-11\n" +"POT-Creation-Date: 2026-02-10\n" "Last-Translator: \n" "Language-Team: none\n" "Language: en\n" "Content-Type: text/plain; charset=UTF-8\n" "Content-Transfer-Encoding: 8bit" -#: Game.Levels.L6Pset.L6Pset3 -msgid "# Problem 3\n" -"\n" -"You are given that a sequence `a : ℕ → ℝ` converges to 5.\n" -"Prove that it is eventually positive." -msgstr "" - -#: Game.Levels.L3Levels.L01_ArchProp -msgid "Prove the \\\"Archimedean Property\\\"\n" -"that no matter how small `ε > 0` may be,\n" -"there is always a natural number `N` with `1 / ε < N`." -msgstr "" - #: Game.Levels.L23Levels.L03 msgid "A continuous function on a compact set is uniformly continuous on that set." msgstr "" -#: Game.Levels.L10Pset.L10Pset6 -msgid "# Problem 5:\n" +#. §0: `h : x = 2 ∧ y = 3 ∧ z = 4` +#. §1: `z = 4` +#: Game.Levels.L6Pset.L6Pset2 +msgid "# Problem 2\n" "\n" -"Show that the sequence `a n = n` is unbounded." +"You know that §0.\n" +"Your goal is to show that: §1." msgstr "" -#: Game.Levels.L16Levels.L01_check -msgid "`(a : ℕ → ℝ) : Prop := SeqConv (Series a)`\n" +#. §0: `rewrite [Bob]` +#. §1: `x` +#. §2: `2` +#: Game.Levels.L1RealAnalysisStory.L03_rw +msgid "Type §0 to replace §1 with §2 in the goal. Then what?" +msgstr "" + +#. §0: `ε > 0` +#. §1: `N` +#. §2: `1 / N` +#. §3: `ε` +#. §4: `ε` +#. §5: `N` +#. §6: `1 / ε < N` +#. §7: `ε : ℝ` +#. §8: `0 < ε` +#. §9: `N : ℕ` +#. §10: `1 / ε < N` +#. §11: `N` +#. §12: `x ↦ ⌈x⌉` +#. §13: `ℤ` +#. §14: `ℕ` +#. §15: `x ↦ ⌈x⌉₊` +#. §16: `\\lceil` +#. §17: `\\rceil` +#. §18: `\\_+` +#. §19: `0` +#. §20: `⌈-3.14⌉₊ = 0` +#. §21: `⌈3.14⌉₊ = 4` +#. §22: `N = ⌈1 / ε⌉₊ + 1` +#. §23: `1 / ε ≤ ⌈1 / ε⌉₊` +#. §24: `1 / ε < ⌈1 / ε⌉₊ + 1` +#. §25: `ℕ` +#. §26: `ℤ` +#. §27: `ℚ` +#. §28: `ℝ` +#. §29: `have` +#. §30: `have fact : 1 / ε ≤ ⌈1 / ε⌉₊ := by WhateverTheProofIs` +#. §31: `fact : 1 / ε ≤ ↑⌈1 / ε⌉₊` +#. §32: `↑` +#. §33: `ℕ` +#. §34: `ℤ` +#. §35: `ℚ` +#. §36: `ℝ` +#. §37: `3 : ℕ` +#. §38: `3 / 1 : ℚ` +#. §39: `3.000 : ℝ` +#. §40: `push_cast` +#. §41: `ring_nf` +#. §42: `⌈ ⬝ ⌉₊` +#. §43: `push_cast` +#. §44: `bound` +#. §45: `bound` +#: Game.Levels.L3Levels.L01_ArchProp +msgid "# Level 1: The Archimedean Property\n" "\n" -"The Series of a sequence `a : N → ℝ` converges if the sequence of its partial sums converges." -msgstr "" - -#: Game.Levels.L20Pset.L03 -msgid "If `f → L` as `x → c`, then `k · f → k · L`." -msgstr "" - -#: Game.Levels.L7Levels.L02_SeqOfAbs -msgid "The absolute value function is Lipschitz with constant 1." -msgstr "" - -#: Game.Levels.L10Pset.L10Pset5 -msgid "# Problem 4:\n" +"The so-called Archimedean Property (which I think is originally due to Eudoxus, and appears already in Euclid's Elements Book V) is a fundamental property of the real numbers that captures the intuitive notion that there are no \"infinitely large\" or \"infinitesimally small\" positive real numbers.\n" "\n" -"Exhibit (by starting with `let a : ℕ → ℝ := fun n ↦ ???`)\n" -"a sequence so that\n" +"More precisely, it states that no matter how small §0 is, there is always a natural number §1 so that §2 is even smaller than §3 (and of course positive). Equivalently, we can state it as: for any positive real number §4, there exists a natural number §5 such that §6.\n" "\n" -"- the terms are all strictly positive: `∀ n, 0 < a n`,\n" -"- and yet the sequence converges to zero (and not something strictly positive!).\n" +"*Why does this matter?* The Archimedean Property is one of the most fundamental properties distinguishing the real numbers from other number systems. Without it, we could have \"infinitely large\" or \"infinitesimally small\" positive numbers, which would break most of calculus and analysis.\n" "\n" -"When you define a new sequence using `let`, you might find it\n" -"convenient to immediately prove a trivial theorem restating the definition:\n" +"Our goal will be to prove the following:\n" +"\n" +"**Theorem (ArchProp)**: For any §7 with §8, there exists §9 such that §10.\n" +"\n" +"This is mathematically \"obvious\" to most people—if you have a positive number ε, no matter how small, you can always find a natural number large enough that 1 / ε is smaller than it. (At least it seems obvious, and perhaps becomes less so once you remember that we don't yet know what the real numbers actually *are*... We'll continue postponing the construction for some time.) But how do you actually formalize this in Lean?\n" +"\n" +"## The Natural Language Proof Strategy\n" +"\n" +"First, let's think about this in natural language. The key insight is that we need to provide a specific natural number §11 that works.\n" +"\n" +"A natural choice would be to use something related to the ceiling function. The ceiling function §12 rounds any real number up to the nearest integer. However, there's a subtle issue here: the standard ceiling function takes values in integers §13, but we need values in §14 (the natural numbers). These are *not* the same thing!!\n" +"\n" +"Fortunately, Lean provides the \"natural number ceiling function\" written §15, which takes any real number and returns a natural number.\n" +"(You can write these symbols using §16, §17, and §18. Or if you're lazy like me, just copy and paste them from elsewhere.)\n" +" For negative inputs, this function returns §19. For example, §20 and §21.\n" +"\n" +"Now our strategy becomes clear:\n" +"- **Choice of N**: Use §22\n" +"- **Why this works**: We have the \"key inequality\": §23, which holds by the definition of the ceiling function\n" +"- **Getting strict inequality**: Adding 1 gives us §24\n" +"\n" +"## The Lean Implementation Challenges\n" +"\n" +"In Lean, the first two steps of our natural language proof work fine, but then we encounter the issue of **type coercion** (\"casting\" between different number types). We'll discuss this in more detail later, but again it has to do with the fact that §25, §26, §27, and §28 are all different kinds of things, and we need to be able to move numbers up the \"sophistication\" heirarchy, with natural numbers being the simplest objects and the reals being the most complicated (so much so that we keep postponing their construction).\n" +"\n" +"For example, notice that when we'll write our §29 statement to establish the key inequality:\n" "\n" -"`have ha : ∀ n, a n = ??? := by intro n; rfl`\n" +"§30\n" "\n" -"This may become useful should you want to `rewrite` by `ha` (you can't rewrite by `a`, since it's a definition, not a theorem!)...\n" +"Lean will record it as:\n" +"\n" +"§31\n" +"\n" +"Notice the mysterious up arrow §32. This represents a coercion function from natural numbers to real numbers:\n" +"\n" +"↑ : ℕ → ℝ\n" +"\n" +"This is because §33, §34, §35, and §36 are all **different** types in Lean's type system (and really, in mathematics, as we'll see when we construct the real numbers)! Even though we think of natural numbers as being \"contained\" in the real numbers, formally they are distinct types of things, and Lean needs explicit coercion functions to convert between them.\n" +"\n" +"*Think of it this way*: the natural number §37 and the fraction §38 and the real number §39 are different objects that just happen to represent the same mathematical value.\n" +"\n" +"The §40 tactic helps manage these coercions, kind of like §41 but for casting instead of ring operations.\n" "\n" -"**Extra challenge:** See if you can do it by using theorems we already proved, not by going into the `ε-N` definition..." +"## New Tools You'll Need\n" +"\n" +"- §42: The natural number ceiling function\n" +"- §43: Tactic that handles coercions between number types\n" +"- §44: Solves many routine inequalities\n" +"\n" +"The §45 tactic can solve many \"trivial\" inequalities once the types are properly aligned.\n" +"\n" +"## Hint:\n" +"\n" +"If you get stuck and don't see a Hint, try backtracking until you do." msgstr "" -#: Game.Levels.L1RealAnalysisStory.L05_use -msgid "The `use` tactic provides a specific value to prove an existence statement." +#: Game.Levels.L7Levels.L02_SeqOfAbs +msgid "The absolute value function is Lipschitz with constant 1." msgstr "" +#. §0: `change ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |b n - 2 * L| < ε` #: Game.Levels.L5Levels.L01_DoubleSeqConv -msgid "You can't use `abs_mul` just yet, because you don't have a product of things inside the absolute values! So first factor out the 2: `have factor : 2 * a n - 2 * L = 2 * (a n - L) := by ring_nf`" -msgstr "" - -#: Game -msgid "Learn real analysis through the historical crises that forced mathematicians to rebuild calculus from the ground up in the 19th century." -msgstr "" - -#: Game.Levels.L7Levels.L04_ByCases -msgid "ByCases" +msgid "Start by unfolding the definition: §0" msgstr "" -#: Game.Levels.L14Lecture -msgid "# Lecture 14: Bolzano-Weierstrass" +#. §0: `N` +#. §1: `N` +#. §2: `1 / ε < N` +#. §3: `have f1 : ∃ (N : ℕ), 1 / ε < N := by apply ArchProp hε` +#: Game.Levels.L3Levels.L02_OneOverN +msgid "We need to find §0. Use the Archimedean Property: there exists §1 such that §2. Try: §3" msgstr "" -#: Game.Levels.L23Levels.L03 -msgid "`IsCompact (S : Set ℝ) : Prop :=\n" -" ∀ (ι : Type) (xs : ι → ℝ) (δs : ι → ℝ), (∀ i, 0 < δs i) → (S ⊆ ⋃ i, Ball (xs i) (δs i)) →\n" -" ∃ (V : Finset ι), S ⊆ ⋃ i ∈ V, Ball (xs i) (δs i)`\n" -"\n" -"A set `S` is compact if for every cover of `S` by balls, there exists a finite subcover." +#: Game +msgid "Learn real analysis through the historical crises that forced mathematicians to rebuild calculus from the ground up in the 19th century." msgstr "" -#: Game.Levels.L11Levels.L01_IsCauchyOfLim -msgid "# Congratulations! You've proven that convergence implies Cauchy!\n" +#. §0: $|a_n| \\leq b_n$ +#. §1: $\\sum b_n$ +#. §2: $\\sum a_n$ +#: Game.Levels.L18Levels.L01 +msgid "# Congratulations!\n" "\n" -"This is one of the most fundamental results in analysis. You've just shown that the \"self-referential\" Cauchy property is a *necessary condition* for convergence.\n" +"You've just proven one of the most important theorems in the theory of infinite series!\n" "\n" -"## What you've learned\n" +"## What We've Learned\n" "\n" -"- How to work with the Cauchy definition using multiple indices `m` and `n`\n" -"- The power of the `ε/2` trick to make inequalities work out\n" -"- How to use `abs_sub_comm` to flip differences inside absolute values\n" -"- How to connect a sequence to itself rather than to an external limit\n" +"The theorem **absolute convergence implies convergence** gives us a powerful tool: to show a series converges, it often suffices to show it converges absolutely. This is frequently easier because we can ignore the signs of the terms.\n" "\n" -"## The Big Question\n" +"## Key Technique\n" "\n" -"You've proven: **convergence ⟹ Cauchy**\n" +"The proof relied on the **Cauchy criterion**: a series converges if and only if its partial sums form a Cauchy sequence. We showed that if the series of absolute values is Cauchy, then the original series must be Cauchy too, using the triangle inequality to bound the partial sums.\n" "\n" -"But what about the converse? Is every Cauchy sequence convergent?\n" +"## Why This Matters\n" "\n" -"- **For rational sequences**: NO! The sequence `1, 1.4, 1.41, 1.414, ...` is Cauchy in ℚ but doesn't converge to a rational number.\n" -"- **For real sequences**: This is the *Cauchy Completeness Theorem*, and it's **YES**! But we'll need to carefully construct the real numbers first to prove it.\n" +"This theorem is the foundation for:\n" +"- **Comparison tests**: If §0 and §1 converges, then §2 converges absolutely (hence converges)\n" +"- **Rearrangement theorems**: Absolutely convergent series can be rearranged without changing their sum\n" +"- **Function series**: Power series and Fourier series often converge absolutely in their domains\n" "\n" -"This is why Cauchy sequences are so important—they give us a way to *define* the real numbers as the completion of the rationals!\n" +"## The Converse is False!\n" "\n" -"Onward to the next level!" -msgstr "" - -#: Game.Levels.L4Levels.L01_NonConverge -msgid "`(a : ℕ → ℝ) := ∃ L, SeqLim a L`\n" +"Remember: The converse is *not* true. There exist series that converge but do not converge absolutely. These are called **conditionally convergent** series, and they behave very differently from absolutely convergent series (as we'll see in the next level with the Alternating Series Test)!\n" "\n" -"A sequence `a : N → ℝ` converges (`SeqConv a` holds) if there exists some\n" -"`L : ℝ` so that `a → L`, that is, `SeqLim a L` holds." +"The distinction between absolute and conditional convergence is one of the most important concepts in real analysis." msgstr "" -#: Game.Levels.L6Levels.L04_Cases' -msgid "When have a hypothesis `h : P ∨ Q`, you can say `cases' h with h1 h2`; this will make two new Game Boards, one with an extra hypothesis `h1 : P`, and the other with the hypothesis `h2 : Q`. You'll have to solve both to solve the original Goal!" +#: Game.Levels.L7Levels.L04_ByCases +msgid "ByCases" msgstr "" -#: Game.Levels.L17Levels.L04 -msgid "Magnificent! You've proven that the Basel series converges—a major milestone in the history of mathematics!\n" +#. §0: `xₙ` +#. §1: `n` +#. §2: `y` +#. §3: `k` +#. §4: `N(k)` +#. §5: `1/(k+1)` +#. §6: `y` +#. §7: `y` +#. §8: `∑ aₙ` +#. §9: `x₀, f(x₀), f(f(x₀)), ...` +#. §10: `eˣ` +#. §11: `sin(x)` +#. §12: `cos(x)` +#: Game.Levels.L15Levels.L01_check +msgid "# Conclusion: The Reals Are Complete\n" "\n" -"## What You've Accomplished\n" +"Congratulations! You've just proved one of the most fundamental theorems in real analysis: **the real numbers are complete**.\n" "\n" -"**Theorem:** The series `∑ k, 1/(k+2)² = 1/4 + 1/9 + 1/16 + ...` converges.\n" +"## What We Accomplished\n" "\n" -"You proved this using the **Monotone Bounded Convergence Theorem**, which you first established by connecting two powerful results:\n" -"- `IsCauchy_of_MonotoneBdd`: monotone bounded sequences are Cauchy\n" -"- `Conv_of_IsCauchy`: by completeness of ℝ, Cauchy sequences converge\n" +"We showed that any Cauchy sequence of real numbers converges to a real number. This means:\n" +"- We don't need to construct yet another number system beyond ℝ\n" +"- The completion process terminates: ℚ → ℝ → ... → ℝ (we're done!)\n" +"- Every \"should converge\" sequence in ℝ actually does converge in ℝ\n" "\n" -"## The Proof Strategy\n" +"## The Beauty of the Construction\n" "\n" -"Your proof had three elegant components:\n" +"The proof relied on a clever diagonal-inspired construction:\n" +"- Each real §0 is secretly a Cauchy sequence of rationals (row §1 of our array)\n" +"- We extracted a **single** sequence §2 by sampling one rational from each row\n" +"- The key: we sampled row §3 at index §4 where it had already converged to within §5 of its limit\n" +"- This ensured §6 itself was Cauchy, and that §7 captured the limit of the sequence of reals\n" "\n" -"1. **Comparison with Leibniz:** You showed `1/(k+2)² ≤ 1/((k+1)(k+2))`, so by `SeriesOrderThm`, the Basel partial sums are bounded by the Leibniz partial sums, which equal `1 - 1/(n+1) < 1`.\n" +"The technique—choosing convergence points rather than blindly taking the diagonal—is fundamental in analysis. You'll see variations of this argument in:\n" +"- Arzela-Ascoli theorem (equicontinuous families)\n" +"- Weak compactness arguments (functional analysis)\n" +"- Diagonal extraction arguments throughout measure theory\n" "\n" -"2. **Boundedness:** The Basel series has partial sums bounded above by 1.\n" +"## Why Completeness Matters\n" "\n" -"3. **Monotonicity:** Since each term `1/(k+2)² > 0`, the partial sums form a monotone increasing sequence.\n" +"Completeness is what makes analysis possible. Here's what we can now guarantee:\n" "\n" -"Monotone + Bounded = Convergent! This is one of the fundamental patterns in real analysis.\n" +"**Closure under limits:** Take limits freely within ℝ without worrying about \"escaping\" the space.\n" "\n" -"## What We Haven't Shown\n" +"**Convergence of series:** Infinite sums §8 converge whenever their partial sums are Cauchy.\n" "\n" -"Notice that we've proven convergence but **not** computed the exact value! We know the series converges to *some* real number less than 1, but we don't know what it is.\n" +"**Fixed point theorems:** Contractions have fixed points, found by iterating §9\n" "\n" -"Computing the exact value is much harder. Euler's brilliant solution in 1734 showed:\n" -"$\\sum_{k=1}^\\infty 1/k^2 = \\pi^2/6 \\approx 1.6449...$\n" +"**Function construction:** Define §10, §11, §12 as limits of sequences/series with confidence they converge.\n" "\n" -"See the homework problems for more details!\n" +"**Completeness + Archimedean + Ordered Field = ℝ:** Any mathematical structure with these properties is isomorphic to the real numbers. We've fully characterized ℝ!\n" "\n" -"## The Broader Story: Riemann Zeta Function\n" +"## The Completion Journey\n" "\n" -"Euler went on to evaluate `∑ 1/k^(2n)` for all positive integers `n`, showing each equals a rational multiple of `π^(2n)`. These are now known as special values of the **Riemann zeta function**:\n" -"`ζ(s) = ∑_{k=1}^∞ 1/k^s`\n" +"Let's recap how we got here:\n" "\n" -"So `ζ(2) = π²/6`, `ζ(4) = π⁴/90`, `ζ(6) = π⁶/945`, etc.\n" +"1. **Started with ℚ** - algebraically nice but full of holes\n" +"2. **Defined Cauchy sequences** - identified \"should converge\" sequences\n" +"3. **Took equivalence classes** - two sequences are the same if their difference → 0\n" +"4. **Created ℝ** - the set of these equivalence classes\n" +"5. **Proved completeness** - Cauchy sequences in ℝ converge in ℝ\n" "\n" -"But what about odd values? Is `ζ(3) = ∑ 1/k³` related to `π`, or any other known constant? This question is still open today! Only in 1978, did Roger Apéry manage to prove that `ζ(3)` is **irrational**! We do not have a **right** to mathematical knowledge; any time our ignorance is momentarily lifted, it is a cause for celebration.\n" +"This is the **completion** of a metric space, and it's a universal construction in mathematics.\n" "\n" -"## The Power of Comparison\n" +"## Beyond the Reals\n" "\n" -"Your proof demonstrated the **comparison test** in action: to prove a series converges, find a known convergent series that dominates it term-by-term. This is one of the most practical convergence tests in analysis.\n" +"The completeness property isn't unique to ℝ:\n" "\n" -"## Historical Significance\n" +"**Other complete spaces:**\n" +"- ℂ (complex numbers) - complete in the same sense\n" +"- ℝⁿ (Euclidean space) - complete under the Euclidean metric\n" +"- Lᵖ spaces - complete normed vector spaces of functions\n" +"- C[a,b] - continuous functions with sup norm\n" "\n" -"The Basel Problem launched Euler's career and revolutionized the study of infinite series. It showed that series could encode deep connections between discrete sums and continuous quantities like `π`.\n" +"**Incomplete spaces that need completion:**\n" +"- ℚ needs completion → ℝ\n" +"- ℚₚ (p-adics) from ℚ with p-adic absolute value\n" +"- Continuous functions with L² norm need completion → L² space\n" "\n" -"---\n" +"The pattern is always the same: Cauchy sequences → equivalence classes → completed space.\n" "\n" -"**Congratulations!** You've completed Lecture 17 and proven some of the most beautiful classical results about infinite series. You've mastered telescoping sums, the comparison test, and the monotone bounded convergence theorem—powerful tools you'll use throughout analysis.\n" +"## Looking Ahead\n" "\n" -"**Next lecture:** We'll explore more sophisticated convergence tests and dive deeper into the theory of series!" -msgstr "" - -#: Game.Levels.L16Pset.L16Pset2 -msgid "The partial sums of the series `∑ k, c * a k` is equal to that of `c * ∑ k, a k`." -msgstr "" - -#: Game.Levels.L1RealAnalysisStory.L02_rfl -msgid "The `rfl` tactic proves goals of the form `A = A` where both sides are *identical*." -msgstr "" - -#: Game.Levels.L11Levels.L01_IsCauchyOfLim -msgid "Big Boss : Limits are Cauchy" -msgstr "" - -#: Game.Levels.L9Pset.L9Pset1 -msgid "# Problem 1\n" +"With completeness established, we've finished building the real number system. We now have:\n" +"- ✓ An ordered field (arithmetic that respects order)\n" +"- ✓ Archimedean property (no infinitesimals)\n" +"- ✓ Monotone Convergence Theorem (bounded monotone sequences converge)\n" +"- ✓ Bolzano-Weierstrass Theorem (bounded sequences have convergent subsequences)\n" +"- ✓ Completeness (Cauchy sequences converge)\n" "\n" -"Prove the same theorem as `Bdd_of_ConvNonzero`, but without the assumption that `L ≠ 0`. (Hint: break\n" -"the proof into cases, and the case `L ≠ 0` should just be an appeal to `Bdd_of_ConvNonzero`. What\n" -"do you do in the other case?)" +"These properties collectively **characterize** ℝ up to isomorphism.\n" +"\n" +"Now we can move beyond the construction of ℝ to actually **doing analysis**:\n" +"- Continuous functions and the Intermediate Value Theorem\n" +"- Differentiability and the Mean Value Theorem\n" +"- Integration and the Fundamental Theorem of Calculus\n" +"- Uniform convergence and series of functions\n" +"- Power series and analytic functions\n" +"\n" +"The foundation is solid. The real mathematics begins now!\n" +"\n" +"## A Final Thought\n" +"\n" +"There's something philosophically profound about completeness. To achieve it, we had to:\n" +"- Accept infinite processes as completed objects\n" +"- Embrace numbers that can't be written as finite expressions\n" +"- Work with equivalence classes rather than concrete representations\n" +"\n" +"But in return, we gained a number system where:\n" +"- Every bounded monotone sequence converges\n" +"- Every continuous function on [a,b] attains its maximum\n" +"- The Intermediate Value Theorem holds\n" +"- Calculus works!\n" +"\n" +"We traded the simplicity of ℚ (every number is p/q) for the completeness of ℝ (every Cauchy sequence converges). This trade-off—giving up finite describability to gain analytic power—is at the heart of modern mathematics.\n" +"\n" +"**Welcome to the real numbers. They're complete, they're beautiful, and they're ready for analysis.**" msgstr "" -#: Game.Levels.L6Levels.L00_SumOfSeqs -msgid "Prove that the sum of two convergent sequences converges to the sum of their limits.\n" -"This is the mathematician's version of 'if two factories each meet their quality standards, their combined output will too!'" +#: Game.Levels.L14Lecture +msgid "# Lecture 14: Bolzano-Weierstrass" msgstr "" -#: Game.Levels.L10Levels.L08_Mono -msgid "Beautiful! That was remarkably simple for such a powerful theorem.\n" +#. §0: `(f : ℕ → ℝ → ℝ) (F : ℝ → ℝ) := +#. ∀ ε > 0, ∃ N, ∀ n ≥ N, ∀ x, |f n x - F x| < ε` +#. §1: `f : ℕ → ℝ → ℝ` +#. §2: `F : ℝ → ℝ` +#: Game.Levels.L22Levels.L02 +msgid "§0\n" +"\n" +"The sequence §1 of functions converges uniformly to §2." +msgstr "" + +#. §0: `f` +#. §1: `g` +#. §2: `c` +#. §3: `f + g` +#. §4: `c` +#. §5: `f(x)` +#. §6: `f(c)` +#. §7: `g(x)` +#. §8: `g(c)` +#. §9: `x` +#. §10: `c` +#. §11: `f(c) + g(c)` +#. §12: `ε/2` +#. §13: `ε > 0` +#. §14: `|(f + g)(x) - (f + g)(c)| < ε` +#. §15: `|(f + g)(x) - (f + g)(c)| = |f(x) + g(x) - f(c) - g(c)|` +#. §16: ` = |[f(x) - f(c)] + [g(x) - g(c)]|` +#. §17: ` ≤ |f(x) - f(c)| + |g(x) - g(c)|` +#. §18: `ε/2` +#. §19: `ε` +#. §20: `f` +#. §21: `c` +#. §22: `δ₁ > 0` +#. §23: `|x - c| < δ₁` +#. §24: `|f(x) - f(c)| < ε/2` +#. §25: `g` +#. §26: `c` +#. §27: `δ₂ > 0` +#. §28: `|x - c| < δ₂` +#. §29: `|g(x) - g(c)| < ε/2` +#. §30: `δ = min δ₁ δ₂` +#. §31: `f` +#. §32: `g` +#. §33: `c` +#. §34: `c` +#. §35: `FunContAt f c → FunContAt g c → FunContAt (fun x ↦ f x + g x) c` +#. §36: `ε` +#. §37: `hε` +#. §38: `hf` +#. §39: `hg` +#. §40: `ε/2` +#. §41: `δ₁` +#. §42: `δ₂` +#. §43: `use min δ₁ δ₂` +#. §44: `bound` +#: Game.Levels.L20Levels.L03 +msgid "# Level 3: Sum of Continuous Functions\n" "\n" -"**Why This Proof Works:**\n" +"One of the most powerful aspects of continuity is that it behaves well with respect to algebraic operations. Let's prove our first **continuity theorem**: the sum of continuous functions is continuous!\n" "\n" -"The key insight is that subsequences can only \"spread out\" indices, never compress them. Since `σ(n) ≥ n` always, if `a` is eventually within `ε` of `L` (for all indices ≥ N), then `a ∘ σ` is too—because `σ` maps `n ≥ N` to even larger indices where `a` is still close to `L`.\n" +"## The Theorem\n" "\n" -"The same `N` works for all subsequences!\n" +"**Theorem:** If §0 and §1 are both continuous at §2, then §3 is continuous at §4.\n" "\n" -"**The Contrapositive: A Divergence Test**\n" +"This seems intuitive: if §5 stays close to §6 and §7 stays close to §8 when §9 is near §10, then their sum should stay close to §11.\n" "\n" -"The Subsequence Theorem says: *If `a n → L`, then every subsequence converges to `L`.*\n" +"## The Strategy: The §12 Trick\n" "\n" -"By contrapositive: *If there exist two subsequences converging to different limits, then `a` does not converge.*\n" +"Given §13, we want to make §14.\n" "\n" -"This is a powerful tool for proving divergence!\n" +"Notice that:\n" "\n" -"**Example Application:**\n" +"§15\n" "\n" -"Consider `a n = (-1)^n`, which oscillates between -1 and 1:\n" -"- The even-indexed subsequence: `a(0), a(2), a(4), ... = 1, 1, 1, ...` converges to 1\n" -"- The odd-indexed subsequence: `a(1), a(3), a(5), ... = -1, -1, -1, ...` converges to -1\n" +"§16\n" "\n" -"Since we have subsequences converging to different limits (1 and -1), the sequence `a n = (-1)^n` does not converge. We'll see this in the next level!\n" +"§17\n" "\n" -"**Looking Ahead:**\n" +"So if we can make each term less than §18, their sum will be less than §19!\n" "\n" -"Subsequences are fundamental in analysis:\n" -"- **Bolzano-Weierstrass Theorem:** Every bounded sequence has a convergent subsequence\n" -"- **Compactness:** Sequential compactness is defined using subsequences\n" -"- **Cauchy sequences:** Can be understood through subsequences\n" -"- **limsup and liminf:** Defined as limits of monotone subsequences\n" +"Since §20 is continuous at §21, there exists §22 such that §23 implies §24.\n" "\n" -"The concept generalizes to metric spaces and topological spaces, where it's crucial for understanding convergence and compactness.\n" +"Since §25 is continuous at §26, there exists §27 such that §28 implies §29.\n" "\n" -"**Exercise:** Prove that if a sequence has two subsequences converging to different limits, then the sequence diverges. (Hint: use proof by contradiction—assume the sequence converges and derive that the two limits must be equal.)" +"Taking §30 ensures both conditions hold simultaneously!\n" +"\n" +"## Your Challenge\n" +"\n" +"Prove that if §31 and §32 are continuous at §33, then their sum is continuous at §34:\n" +"\n" +"§35\n" +"\n" +"**Hint:** After introducing §36 and §37, use the hypotheses §38 and §39 with §40 to choose §41 and §42. Then §43. You'll need to show this is positive and that it works. The triangle inequality and §44 will be your friends!" msgstr "" -#: Game.Levels.L10Pset.L10Pset7 -msgid "Problem 6" +#. §0: `ring_nf` +#. §1: `apply hypothesis_name` +#. §2: `rfl` +#. §3: `rewrite [hypothesis_name]` +#. §4: `ring_nf` +#. §5: `ring_nf` +#: Game.Levels.L1RealAnalysisStory.L04_ring_nf +msgid "Excellent! You've learned the §0 tactic.\n" +"\n" +"This tactic is incredibly powerful for algebraic manipulations. It automatically handles all the tedious algebra that would take many steps to do by hand.\n" +"\n" +"Your toolkit now includes:\n" +"- §1 for when a hypothesis matches your goal\n" +"- §2 for proving something equals itself\n" +"- §3 for rewriting using equalities\n" +"- §4 for algebraic simplifications and expansions\n" +"\n" +"As we move into real analysis proper, you'll find that §5 is invaluable for dealing with polynomial expressions, which appear everywhere in calculus!" msgstr "" -#: Game.Levels.L13Levels.L03_MonotoneSubseq -msgid "Monotone Subsequence" +#. §0: `intro ε` +#. §1: `intro hε` +#. §2: `ε > 0` +#: Game.Levels.L1RealAnalysisStory.L06_intro +msgid "Use §0 to introduce the variable, then §1 to introduce the hypothesis §2. Then how do you solve the goal?" msgstr "" -#: Game.Levels.L3Levels.L02_OneOverN -msgid "Now we need `1 / n < ε`. First establish that everything is positive. Start with: `have f3 : 0 < 1 / ε := by bound`" +#. §0: `Series (fun n ↦ |a n|)` +#. §1: `Series a` +#: Game.Levels.L18Levels.L01 +msgid "If §0 converges, then §1 converges." msgstr "" -#: Game.Levels.L11Levels.L01_IsCauchyOfLim -msgid "If a sequence `a : ℕ → ℝ` converges, then it is Cauchy." +#. §0: $x = 5$ +#. §1: $x = 5$ +#: Game.Levels.L1RealAnalysisStory.L00_the_problem +#: Game.Levels.L1RealAnalysisStory.L03_rw +msgid "If we know that §0, then we can prove that §1." msgstr "" -#: Game.Levels.L22Levels.L03 -msgid "Summation distributes: `∑ i ∈ s, (f i + g i) = ∑ i ∈ s, f i + ∑ i ∈ s, g i`" +#. §0: `∑ k, 1 / ((k + 1) * (k + 2))` +#: Game.Levels.L17Levels.L01 +#: Game.Levels.L17Levels.L02 +msgid "The series §0 converges." msgstr "" -#: Game.Levels.L20Pset.L01 -msgid "ContinuousIff I" +#: Game.Levels.L11Levels.L01_IsCauchyOfLim +msgid "Big Boss : Limits are Cauchy" msgstr "" -#: Game.Levels.L20Lecture -msgid "Lecture 20: Function Limits" +#. §0: `a` +#. §1: `b` +#: Game.Levels.L11Levels.L02_IsCauchyOfSum +msgid "If sequences §0 and §1 are Cauchy, then so is their sum." msgstr "" -#: Game.Levels.L19Levels.L02 -msgid "# Congratulations!\n" +#. §0: `1 / n ^ 2` +#: Game.Levels.L3Pset.L3Pset3 +msgid "Determine what the limit of the sequence §0 is, and prove it." +msgstr "" + +#. §0: `α ⊕ β` +#. §1: `α` +#. §2: `β` +#. §3: `α` +#. §4: `β` +#. §5: `α ⊕ β = {Sum.inl a : a ∈ α} ∪ {Sum.inr b : b ∈ β}` +#. §6: `Sum.inl a` +#. §7: `a : α` +#. §8: `Sum.inr b` +#. §9: `b : β` +#. §10: `match` +#. §11: `match` +#. §12: `let f : α ⊕ β → γ := fun x ↦ +#. match x with +#. | Sum.inl a => ... -- handle the α case +#. | Sum.inr b => ... -- handle the β case` +#. §13: `cases` +#. §14: `cases` +#. §15: `cases x with +#. | inl a => ... -- when x came from α +#. | inr b => ... -- when x came from β` +#. §16: `s : Finset (α ⊕ β)` +#. §17: `s.lefts : Finset α` +#. §18: `a ∈ s.lefts ↔ Sum.inl a ∈ s` +#. §19: `ι` +#. §20: `S` +#. §21: `Sᶜ` +#. §22: `S` +#. §23: `ι ⊕ Sᶜ` +#. §24: `S ⊆ T` +#. §25: `T` +#. §26: `S` +#. §27: `Sᶜ` +#. §28: `Sᶜ` +#. §29: `Sᶜ` +#. §30: `T` +#. §31: `ℝ` +#. §32: `T` +#. §33: `S` +#. §34: `S` +#: Game.Levels.L24Levels.L05 +msgid "# Level 5: Heine-Borel Theorem: Part 2b\n" "\n" -"You've just proven the **Eventually Covers Property** for rearrangements—a beautiful result about bijections of the natural numbers!\n" +"**The Grand Finale**: We'll complete Heine-Borel by proving that any closed, bounded set is compact. The strategy is elegant: show that closed subsets of compact sets are compact, then use Level 4.\n" "\n" -"## What We've Accomplished\n" +"**New Lean Technology - Sum Types** 📦\n" "\n" -"This theorem tells us that no matter how wildly a rearrangement `σ` scrambles the natural numbers, it can't \"hide\" any element forever. Given any target set `{0, 1, ..., M-1}`, there's a point `N` beyond which we're guaranteed to have seen all of these elements as outputs.\n" +"Before diving into the proof, you need to master Lean's **disjoint union** (sum type):\n" "\n" -"## The Proof Technique\n" +"**What is §0?**: It's the \"either §1 or §2\" type - every element is either from type §3 or from type §4, but not both. Think of it as two boxes labeled \"Left\" and \"Right\":\n" "\n" -"The proof uses a clever construction:\n" -"1. Since `σ` is surjective, each element `j < M` appears as `σ(k_j)` for some `k_j`\n" -"2. We use the axiom of choice (via `choose`) to select all these preimages simultaneously\n" -"3. We set `N` larger than all the `k_j` values\n" -"4. Then for any `n ≥ N`, all the required preimages are in `range n`, so all their images are covered\n" +"§5\n" "\n" -"The key insight is that finite sets have maximum elements, so we can always find a threshold that works.\n" +"**Note**:\n" +"- §6 puts element §7 into the \"left\" side\n" +"- §8 puts element §9 into the \"right\" side\n" "\n" -"## A Concrete Example\n" +"**Pattern Matching with §10**: To make a function on a sum type, use §11:\n" "\n" -"Consider the rearrangement that sends:\n" -"- `0 → 1, 1 → 2, 2 → 3, ...` (shift everything right)\n" -"- except `1000000 → 0` (one element goes way back)\n" +"§12\n" "\n" -"To cover `range 1` (just `{0}`), we need `N ≥ 1000001`, because `0` doesn't appear as `σ(k)` until `k = 1000000`.\n" +"**Case Analysis with §13**: When arguing about where an element of a sum type came from, use §14:\n" "\n" -"But the theorem guarantees such an `N` exists! No matter how we rearrange, we eventually catch everything.\n" +"§15\n" "\n" -"## Why This Matters for Series\n" +"**Extracting Components**: If §16, then:\n" +"- §17 extracts all the \"left\" elements\n" +"- §18\n" "\n" -"When we rearrange a series `∑ a_n` to get `∑ a_(σ(n))`, the partial sums are:\n" -"- Original: `a_0 + a_1 + ... + a_(n-1)`\n" -"- Rearranged: `a_(σ(0)) + a_(σ(1)) + ... + a_(σ(n-1))`\n" +"**Why Sum Types for This Proof?**\n" "\n" -"This theorem tells us that for large enough `n`, the rearranged partial sum includes all the terms `a_0, a_1, ..., a_M` from the original series. Combined with the strong Cauchy property from Level 1, this will let us prove that the rearranged series converges to the same limit!\n" +"We need to handle TWO kinds of balls simultaneously:\n" +"1. **Original balls** (type §19) that cover our closed set §20\n" +"2. **Avoidance balls** (type §21) that cover points outside §22\n" "\n" -"## Next Steps\n" +"The sum type §23 lets us create a unified covering system!\n" "\n" -"In Level 3, we'll combine this result with the strong Cauchy property to prove the magnificent **Rearrangement Theorem**: absolutely convergent series can be rearranged without changing their sum!" +"**The Strategy**:\n" +"1. Start with any covering of closed set §24 where §25 is compact\n" +"2. Since §26 is closed, §27 is open - so each point in §28 has a ball staying in §29\n" +"3. Use sum types to combine: original balls + avoidance balls = covering of all §30 (in fact, all of §31)\n" +"4. Apply compactness of §32 to get finite subcover\n" +"5. Extract just the \"left\" (original) balls to cover §33, since avoidance balls don't touch §34\n" +"\n" +"**Your Mission**: Master sum types and use them to extend any covering of a closed subset to a covering of the whole compact set. This completes the Heine-Borel theorem!" msgstr "" -#: Game.Levels.L3Levels.L01_ArchProp -msgid "And now the `bound` tactic will do the trick." +#: Game.Levels.L6Levels.L00_SumOfSeqs +msgid "Prove that the sum of two convergent sequences converges to the sum of their limits.\n" +"This is the mathematician's version of 'if two factories each meet their quality standards, their combined output will too!'" msgstr "" -#: Game.Levels.L24PsetIntro -msgid "# Problem Set 24\n" -"\n" -"Prove Problems 1 - 6 formally (in natural language); the rest can be proved using sketches of the main ideas.\n" -"\n" -"$\\# 1)$ Prove that an arbitrary union of open sets is open.\n" -"\n" -"$\\# 2)$ Prove that a finite intersection of open sets is open. Give a counterexample to show that an infinite intersection of open sets need not be open.\n" -"\n" -"$\\# 3)$ Prove that an arbitrary intersection of closed sets is closed.\n" -"\n" -"$\\# 4)$ Prove that a finite union of closed sets is closed. Give a counterexample to show that an infinite union of closed sets need not be closed.\n" -"\n" -"$\\# 5)$ Prove that if a set `S : Set ℝ` is closed, then it contains all its limit points; that is, if a sequence `(x_n)` in `S` converges to `x`, then `x ∈ S`. (This is in fact what closed sets are \"closed\" under -- taking limits!)\n" -"\n" -"$\\# 6)$ Prove that if a set `S : Set ℝ` contains all its limit points (`∀ (x : ℕ → ℝ) (L : ℝ), (∀ n, x n ∈ S) → (SeqLim x L) → (L ∈ S)`), then it is closed.\n" -"\n" -"$\\# 7)$ Give a different proof that a closed interval `[a, b]` is Closed. Suppose `xₙ` is a sequence in `[a, b]` converging to `L`. Show that `L ∈ [a, b]`. [Hint: Try the Order Limit Theorem from Lecture 10, Level 2...]\n" -"\n" -"$\\# 8)$ Let `S` be a set of reals, and let `T` be the set of its limit points (that is, the set of all `L : ℝ` such that there exists a sequence `(x_n)` in `S` converging to `L`). Show that if `L` is a limit point of `S ⋃ T`, then `L` is a limit point of `S`. That is, no new limit points are created when we pass from `S` to its \"closure\" `S ⋃ T`. [Hint: Remember how we proved that the real numbers are complete?...]\n" -"\n" -"$\\# 9)$ Prove that if `S` is compact, then any sequence `(x_n)` in `S` has a subsequence that converges to a limit in `S`. The latter property is called *sequential compactness*.\n" -"\n" -"$\\# 10)$ Conversely, prove that if `S` is sequentially compact (that is, every sequence in `S` has a subsequence converging to a limit in `S`), then it is compact.\n" -"\n" -"$\\# 11)$⋆ (Optional!) Let `C` denote the \"Cantor set\". This is constructed as follows. Start with the closed interval `[0, 1]`. Remove the open middle third `(1/3, 2/3)`, leaving the two closed intervals `[0, 1/3]` and `[2/3, 1]`. Now remove the open middle thirds of these two intervals, leaving four closed intervals: `[0, 1/9]`, `[2/9, 1/3]`, `[2/3, 7/9]`, and `[8/9, 1]`. Continue this process indefinitely. The Cantor set `C` is defined as the intersection of all these sets obtained at each step. Show that the Cantor set `C` is closed and hence compact. A point `p` in a set `S` is said to be an *isolated point* of `S` if there exists a ball `Ball p r` that contains no other points of `S` except for `p` itself; that is, there is no nontrivial sequence in `S` converging to `p`. A set `S` is called *perfect* if it has no isolated points, that is, its every point is a nontrivial limit point.\n" -"Show that the Cantor set is perfect." +#. §0: `have abs_factor : |2 * (a n - L)| = |2| * |a n - L| := by apply abs_mul` +#: Game.Levels.L5Levels.L01_DoubleSeqConv +msgid "Apply the absolute value of products: §0" msgstr "" -#: Game.Levels.L9Pset.L9Pset3 -msgid "# Problem 3\n" -"\n" -"Prove that `2 * (1 + 2 + ... + N) = N * (N + 1)`." +#: Game.Levels.L10Pset.L10Pset7 +msgid "Problem 6" msgstr "" -#: Game.Levels.L1RealAnalysisStory.L06_intro -msgid "The `intro` tactic introduces variables and hypotheses from ∀ statements or implications." +#: Game.Levels.L13Levels.L03_MonotoneSubseq +msgid "Monotone Subsequence" msgstr "" -#: Game.Levels.L10Pset.L10Pset2 -msgid "If sequence `a : ℕ → ℝ` converges to `0` and sequence `b : ℕ → ℝ` is bounded, then `a n * b n` converges to `0`." +#. §0: `f : X → Y` +#. §1: `Surjective` +#. §2: `y : Y` +#. §3: `∃ x : X` +#. §4: `f x = y` +#: Game.Levels.L19Levels.L02 +msgid "A function §0 called §1 if: for all §2, §3 so that §4." msgstr "" -#: Game.Levels.L7Pset.L7Pset2 -msgid "# Problem 2\n" -"\n" -"Suppose that sequences `a b : ℕ → ℝ` converge to `L` and `M`, resp, with `L < M`. Show that\n" -"eventually, `a n < b n`." +#: Game.Levels.L20Pset.L01 +msgid "ContinuousIff I" msgstr "" -#: Game.Levels.L25Levels.L02 -msgid "# Level 2 **BIG BOSS**: Intermediate Value Theorem\n" -"\n" -"Welcome to the grand finale! We end our journey through formal real analysis with mathematics' most \"obvious\" theorem—one so intuitive that it was used without proof for over **2000 years**.\n" -"\n" -"**The Intermediate Value Theorem**: If a function `f` is continuous on a closed interval `[a, b]`, with `f(a) < 0` and `f(b) > 0`, then there exists some `c ∈ (a, b)` such that `f(c) = 0`.\n" -"\n" -"*Translation*: A continuous function that changes sign must cross zero somewhere.\n" -"\n" -"**Why is this the \"greatest\" theorem?** Because it captures something profound about the real numbers that we take for granted: there are **no gaps**. Unlike the rationals ℚ (where `f(x) = x² - 2` changes sign but never equals zero), the reals ℝ are **complete**.\n" -"\n" -"**Historical irony**: Ancient Greeks used this theorem in geometric constructions. Euler applied it freely. Even Bolzano and Cauchy assumed it initially. Yet the first rigorous proof wasn't given until 1817—after calculus had been developed for 150 years!\n" -"\n" -"**Why so hard to prove?** Because it requires the **Least Upper Bound Principle**—the very completeness of ℝ that distinguishes it from ℚ. This \"obvious\" theorem actually encapsulates the deepest property of real numbers.\n" -"\n" -"Your proof will use *every major tool* we've built: suprema, continuity, proof by contradiction, and the intricate dance between topology and analysis. Ready for the ultimate challenge?" +#: Game.Levels.L20Lecture +msgid "Lecture 20: Function Limits" msgstr "" -#: Game.Levels.L18Pset.L07 -msgid "# Level 7: `AntitoneSeriesOdd`\n" -"\n" -"Prove `AntitoneSeriesOdd`:" +#. §0: `choose N hN using f1` +#. §1: `hN` +#. §2: `choose N eps_inv_lt_N using f1` +#: Game.Levels.L3Levels.L02_OneOverN +msgid "Presumably you know that you\n" +"should §0 at this stage. But maybe you'd like to give §1 a more descriptive name (so that I can keep giving you hints). Try §2." msgstr "" -#: Game.Levels.L11Lecture -msgid "# Lecture 11: The Real Numbers I\n" -"\n" -"**SOCRATES:** So far we've learned that *if* a sequence converges, then it's bounded, and moreover that any subsequence of it also converges to the same limit.\n" -"\n" -"**SIMPLICIO:** Yeah, so what?\n" -"\n" -"**SOCRATES:** And we saw that there can be sequences which do not themselves converge -- for example, $(-1)^n$ -- but which are bounded and have subsequences that do converge. The even-indexed terms, in this example, are all equal 1.\n" -"\n" -"**SIMPLICIO:** What are you getting at?\n" -"\n" -"**SOCRATES:** Well, what's a question that a mathematician might naturally ask given that information?\n" -"\n" -"**SIMPLICIO:** You mean whether that always happens?\n" -"\n" -"**SOCRATES:** Yes, something like that. Can you elaborate?\n" -"\n" -"**SIMPLICIO:** Okay, I'll play along. You're trying to get me to formulate some kind of converse. If a sequence is bounded, then... it converges? No, that can't be right -- a bounded sequence can bounce around without converging, like $(-1)^n$ itself.\n" -"\n" -"Ah, but maybe there's always *some* subsequence that converges? Hmm, but that can't be right either, since the sequence `aₙ = n` has no convergent subsequence -- it just escapes to infinity.\n" -"\n" -"Oh! But wait, that sequence isn't bounded. Are you saying that if all I know about a sequence is that it's bounded, then there's always *some* subsequence that converges?\n" -"\n" -"**SOCRATES:** Yes, precisely! This important fact is called the \"Bolzano-Weierstrauss theorem\". But here's where it gets **really** subtle. Think about the sequence of fractions: `a (0) = 1 / 1`, `a (1) = 14 / 10`, `a (2) = 141 / 100`, `a (3) = 1414 / 1000`, ... getting closer and closer to $1.4142\\dots = \\sqrt 2$. The sequence is bounded (by $2$, to be crude), and even increasing, but its limit is not a rational number! So the Bolzno-Weierstrauss theorem is not true for the rationals. As I warned you long ago, we'll have to eventually face the fact that we don't even know what the real numbers *are*. I think that time is now.\n" +#. §0: `a` +#: Game.Levels.L11Levels.L03_IsBddOfCauchy +msgid "If a sequence §0 is Cauchy, then it is eventually bounded." +msgstr "" + +#. §0: `split_ands` +#. §1: `left` +#. §2: `right` +#. §3: `h` +#. §4: `h.2` +#. §5: `h : P ∧ Q` +#. §6: `h.1` +#. §7: `P` +#. §8: `h.2` +#. §9: `Q` +#. §10: `P ∧ Q ∧ R` +#. §11: `h.1` +#. §12: `P` +#. §13: `h.2` +#. §14: `Q ∧ R` +#. §15: `P ∧ Q ∧ R = P ∧ (Q ∧ R)` +#. §16: `Q` +#. §17: `h.2.1` +#. §18: `Q` +#. §19: `h.2.2` +#. §20: `R` +#: Game.Levels.L6Levels.L03_DotNotation +msgid "# Level 4: Dot Notation - Accessing Parts of Complex Information\n" "\n" -"**SIMPLICIO:** Fine, I'm ready; tell me what they are.\n" +"Now that you've learned to construct \"and\" statements with §0 and make strategic choices with \"or\" statements using §1 and §2, it's time to learn how to efficiently extract information from complex hypotheses you already have.\n" "\n" -"**SOCRATES:** Unfortunately, it's rather complicated, and it'll take us some time to arrive at the answer, and to see why it *is* the answer. Let's take a step back. What would you *like* to be able to say about the real numbers?\n" +"Often in mathematics, you'll be given a hypothesis that contains multiple pieces of information bundled together. For instance, you might know that \"x = 2 AND y = 3\" but only need the fact that \"y = 3\" for your current goal. Rather than using lengthy tactics to unpack this information, Lean provides an elegant shorthand: dot notation.\n" "\n" -"**SIMPLICIO:** Well, I guess I'd like to say something like: they're the limits of their decimal expansions. So they're limits of rational sequences. Like, $\\sqrt{2}$ is the limit of that sequence you just mentioned: $1, 1.4, 1.41, 1.414, \\dots$\n" +"Think of dot notation like accessing specific files in a well-organized filing cabinet. If you have a folder labeled §3 that contains multiple documents, you can quickly grab the second document with §4 instead of having to open the folder, sort through all the papers, and extract what you need manually.\n" "\n" -"**SOCRATES:** Good! So you want to define a real number as \"the limit of a sequence of rationals.\" But remind me, what does it mean for a sequence to have a limit?\n" +"This notation becomes especially powerful when dealing with complex mathematical objects. In real analysis, we often work with properties that have multiple components—a sequence might be both bounded AND monotonic, or a function might be both continuous AND differentiable. Dot notation lets us access exactly the property we need, when we need it.\n" "\n" -"**SIMPLICIO:** It means that for all `ε > 0`, there exists an `N`, yadda yadda. The terms get arbitrarily close to some number $L$.\n" +"## New Tools You'll Need\n" "\n" -"**SOCRATES:** And what is this mysterious number $L$? What *type* of number it?\n" +"**Dot notation**: When you have a hypothesis §5, you can access the first part with §6 (which gives you §7) and the second part with §8 (which gives you §9).\n" "\n" -"**SIMPLICIO:** It's... a real number. Oh no.\n" +"Note that for longer conjunctions like §10, §11 gives §12 as expected, but\n" +"§13 gives §14. That's because there are hidden parentheses: §15. So how do you get to §16 alone? Easy: dot notation! Writing §17 gives §18, and §19 gives §20." +msgstr "" + +#: Game.Levels.L17PsetIntro +msgid "Pset 17" +msgstr "" + +#. §0: `Series_abs_add` +#. §1: `Series_abs_add` +#: Game.Levels.L18Pset.L02 +msgid "# Level 2: §0\n" "\n" -"**SOCRATES:** Exactly! We have a circular definition. We're trying to define the real numbers as limits of rational sequences, but the very notion of \"limit\" that we've been using presupposes that we already know what the real numbers are!\n" +"Prove §1:" +msgstr "" + +#. §0: `a : ℕ → ℚ` +#. §1: `SeqLim` +#. §2: `Real_of_CauSeq` +#: Game.Levels.L15Levels.L01_check +msgid "If a sequence §0 is Cauchy, then it converges (that is, §1 holds)\n" +"to the real number defined in §2." +msgstr "" + +#. §0: `n` +#. §1: $$\\sum_{i=0}^{n-1} (i+1)^2 = \\frac{n(n+1)(2n+1)}{6}.$$ +#: Game.Levels.L22Pset.L04 +msgid "The sum of the squares of the first §0 natural numbers is given by the formula:\n" +"§1" +msgstr "" + +#. §0: `f(x) = x² - 1` +#. §1: `x = 2` +#. §2: `FunDerivAt f L c` +#. §3: `f` +#. §4: `L` +#. §5: `c` +#. §6: `FunDeriv` +#. §7: `g` +#. §8: `f` +#. §9: `∀ x, FunDerivAt f (g x) x` +#. §10: `FunDeriv f g` +#. §11: `x` +#. §12: `f` +#. §13: `x` +#. §14: `g(x)` +#. §15: `f(x) = x² - 1` +#. §16: `f'(x) = 2x` +#. §17: `x` +#. §18: `d/dx[xⁿ] = n·xⁿ⁻¹` +#. §19: `x` +#. §20: `lim[h→0] (f(x + h) - f(x)) / h` +#. §21: ` = lim[h→0] ((x + h)² - 1 - (x² - 1)) / h` +#. §22: ` = lim[h→0] (x² + 2xh + h² - x²) / h` +#. §23: ` = lim[h→0] (2xh + h²) / h` +#. §24: ` = lim[h→0] h(2x + h) / h` +#. §25: ` = lim[h→0] (2x + h)` +#. §26: ` = 2x` +#. §27: `f(x) = x² - 1` +#. §28: `g(x) = 2x` +#. §29: `FunDeriv (fun x ↦ x^2 - 1) (fun x ↦ 2 * x)` +#. §30: `∀ x, FunDerivAt (fun x ↦ x^2 - 1) (2 * x) x` +#. §31: `x` +#. §32: `x` +#. §33: `2` +#. §34: `ε > 0` +#. §35: `δ = ε` +#. §36: `h ≠ 0` +#. §37: `|h| < ε` +#. §38: `(x + h)² - 1 - (x² - 1) = 2xh + h²` +#. §39: `(2xh + h²) / h = 2x + h` +#. §40: `h ≠ 0` +#. §41: `|(2x + h) - 2x| = |h| < ε` +#: Game.Levels.L21Levels.L07 +msgid "# Level 3: Derivatives Everywhere\n" "\n" -"**SIMPLICIO:** So we're stuck? We can't define the real numbers?\n" +"In the previous level, we computed the derivative of §0 at a single point §1. Now we'll prove something much more powerful: we'll find the derivative at **every** point!\n" "\n" -"**SOCRATES:** Sure seems like it! But this is where Cauchy had a **brilliant** insight. He realized the same thing you did: he can't use real numbers to define limits. He wants to say: \"$a_n$ gets closer and closer to $L$\" but without reference to $L$ itself. He needs to find *something else* that he can say $a_n$ gets close to.\n" +"## From Point Derivatives to Derivative Functions\n" "\n" -"**SIMPLICIO:** But he *has* nothing else.\n" +"So far, §2 tells us that §3 has derivative §4 at the specific point §5.\n" "\n" -"**SOCRATES:** Exactly!! So...?\n" +"But for most functions, we can compute derivatives at *every* point, giving us a **derivative function**.\n" "\n" -"**SIMPLICIO:** So if all he has is the sequence $a_n$, and he has to compare it to something, and he has nothing else... Oh!!! He has to compare it to **itself**!?! But how?\n" +"## The New Definition\n" "\n" -"**SOCRATES:** Wow, you got it! Yes, exactly, How?\n" +"**Definition (§6):** We say that §7 is the derivative of §8 (everywhere) if:\n" "\n" -"**SIMPLICIO:** Well of course it's pointless to ask if `|aₙ - aₙ| < ε`. But... you could ask for `|aₙ - aₘ| < ε`, once `n` and `m` are *both* large enough?\n" +"§9\n" "\n" -"**SOCRATES:** Ha, you did it! Yes, exactly, if $a_n$ and $a_m$ are both within $\\varepsilon$ of **each other**, that should be a substitute for convergence.\n" +"This is written §10.\n" "\n" -"**SIMPLICIO:** That's so clever! So instead of saying \"the sequence converges to $L$,\" we say \"the terms of the sequence get arbitrarily close to each other\"?\n" +"In other words: for each point §11, the derivative of §12 at §13 equals §14.\n" "\n" -"**SOCRATES:** Precisely. Can you make this formal, using `ε`'s and `N`'s?\n" +"## The Power Rule\n" "\n" -"**SIMPLICIO:** I think so. I guess we should say that a sequence $a_n$ has a limit if: for every $\\varepsilon > 0$, there exists an $N$ such that for all $m, n \\geq N$, we have $|a_m - a_n| < \\varepsilon$.\n" +"For §15, we'll prove that §16 for all §17.\n" "\n" -"**SOCRATES:** Beautiful! But since we already have a different meaning for the notion of \"has a limit\", we'll call this property \"Cauchy\". So we say that **a sequence is Cauchy** if, as you said:\n" +"This is an instance of the **power rule**: §18.\n" "\n" -"`∀ ε > 0, ∃ N, ∀ n ≥ N, ∀ m ≥ n, |a m - a n| < ε`\n" +"## Computing the General Derivative\n" "\n" -"(It will be very convenient later to know which of `m` and `n` is bigger, instead of needing to break into cases;\n" -" so we can just say `m ≥ n`.)\n" +"For arbitrary §19, we need:\n" "\n" -"This is one of the most important definitions in **all of mathematics**.\n" -"It appears not only here in real analysis, but also in higher arithmetic when building the p-adic numbers, in functional analysis when studying Banach spaces and Hilbert spaces, and in topology and geometry when \"completing\" metric spaces. Anywhere mathematicians want to talk about \"convergence\" but without knowing *a priori* where things converge *to*, they reach for a version of Cauchy's definition.\n" +"§20\n" "\n" -"But before we return to the real numbers, let's first get more familiar\n" -"with this definition and what it can do.\n" +"§21\n" "\n" -"**SIMPLICIO:** I like it; let's go!" -msgstr "" - -#: Game.Levels.L17PsetIntro -msgid "Pset 17" -msgstr "" - -#: Game.Levels.L3Pset.L3Pset2 -msgid "Prove that the sequence `(n + 1) / n` has a limit `L` and determine what it is." -msgstr "" - -#: Game.Levels.L18Pset.L08 -msgid "Prove `BddSeriesEven`" -msgstr "" - -#: Game.Levels.L7Levels.L01_Eventually -msgid "## What You've Proven\n" +"§22\n" "\n" -"Excellent work! You've proven that convergent sequences with nonzero limits are\n" -"**eventually bounded away from zero**. This is more than just a technical lemma—it's\n" -"a deep insight about the behavior of convergent sequences.\n" +"§23\n" "\n" -"## The Reverse Triangle Inequality in Action\n" +"§24\n" "\n" -"This proof showcased a powerful technique: using the triangle inequality \"in reverse\"\n" -"to establish lower bounds rather than upper bounds. The key manipulation was:\n" +"§25\n" "\n" -"$$|L| = |a (n) + (L - a (n))| \\leq |a (n)| + |L - a (n)|$$\n" +"§26\n" "\n" -"This allowed us to isolate `|a (n)|` and bound it from below.\n" +"## Your Challenge\n" "\n" -"## Looking Ahead\n" +"Prove that the derivative of §27 is §28 everywhere:\n" "\n" -"This result is the crucial prerequisite for proving that reciprocals preserve convergence.\n" -"When we want to show that `1/a (n) → 1/L`, we need to ensure that the denominators `a (n)`\n" -"don't get too small. This theorem guarantees exactly that: eventually, `|a (n)| ≥ |L|/2 > 0`,\n" -"so the reciprocals `1/a (n)` are well-defined and bounded.\n" +"§29\n" "\n" -"You now have the key tool needed for the next major theorem!" -msgstr "" - -#: Game.Levels.L8Pset.L8Pset4 -msgid "# Problem 4\n" +"**Hint:** You need to prove §30.\n" "\n" -"Suppose a sequence `σ : ℕ → ℕ` takes values in the\n" -"*natural numbers* (not reals), and is strictly increasing, that is,\n" -"if `i < j`, then `σ (i) < σ (j)`. Prove that\n" -"`σ (n)` grows at least as fast as `n` itself." -msgstr "" - -#: Game.Levels.L3Levels.L02_OneOverN -msgid "The `linarith` tactic, with syntax `linarith [h₁, h₂]`, can solve goals that are linear arithmetic combinations of hypotheses `h₁, h₂` involving `≤`, `<`, `=` with addition and multiplication by constants.\n" -"- ✅ **Linear:** `2*x + y - 3`, `z / 5`\n" -"- ❌ **Not Linear:** `x*y`, `x^2`, `|x|`, `1/x`\n" +"After introducing §31, the proof is very similar to Level 2, but with §32 instead of §33.\n" "\n" -"Example Usage:\n" -"h1 : x < y\n" -"h2 : y ≤ z\n" -"Goal: x < z + 1\n" -"linarith [h1, h2]" -msgstr "" - -#: Game.Levels.L18Pset.L01 -msgid "Prove `DiffOfSeries`" +"Given §34, use §35. For §36 with §37, simplify:\n" +"- §38\n" +"- §39 (for §40)\n" +"- §41" msgstr "" #: Game.Levels.L22PsetIntro msgid "Pset 22" msgstr "" -#: Game.Levels.L9Levels.L05_BddOfConv -msgid "If `a : ℕ → ℝ` is a sequence which converges to a non-zero limit, then it is bounded.\n" -"See also `Bdd_of_Conv` which assumes nothing about the limit." -msgstr "" - -#: Game.Levels.L1RealAnalysisStory.L04_ring_nf -msgid "Write `ring_nf` to expand and simplify both sides algebraically." +#. §0: `a` +#. §1: `b` +#. §2: `x ∈ Ico a b ↔ a ≤ x ∧ x < b` +#: Game.Levels.L19Levels.L01 +msgid "For §0 and §1, §2." msgstr "" #: Game.Levels.L10Levels.L09_Subseq msgid "Subsequence Example" msgstr "" -#: Game.Levels.L14Levels.L01_BolzanoWeierstrass -msgid "If a sequence `a : ℕ → X` (where `X` can be `ℚ` or `ℝ`) is antitone and bounded, then it is Cauchy." -msgstr "" - #: Game.Levels.L24Levels.L05 msgid "Any closed subset of a compact set is compact." msgstr "" +#. §0: `x=c` +#. §1: `x=c` +#. §2: `f c` +#: Game.Levels.L20Pset.L01 +msgid "# Level 1: ContinuousIff I\n" +"\n" +"Prove the forward direction: If a function is continuous at §0,\n" +"then its limit at §1 exists and is equal to §2." +msgstr "" + #: Game.Levels.L6PsetIntro msgid "# Problem Set 6\n" "\n" "Good luck!" msgstr "" -#: Game.Levels.L23Levels.L02 -msgid "If a function `f` is uniformly continuous on `[a,b]`, then the Riemann sums of `f` converge to a limit as `N → ∞`." +#. §0: `bound` +#: Game.Levels.L3Levels.L01_ArchProp +msgid "And now the §0 tactic will do the trick." msgstr "" -#: Game.Levels.L17Levels.L04 -msgid "# Level 4: The Basel Problem\n" -"\n" -"Near the turn of the 18th century, the Bernoulli brothers Johann and Jakob became obsessed with evaluating the series:\n" -"\n" -"`∑ k, 1 / ((k + 2)²) = 1/4 + 1/9 + 1/16 + 1/25 + ...`\n" -"\n" -"This became known as the **Basel Problem** (after Basel, Switzerland, where the Bernoullis lived). Despite their considerable mathematical prowess, they could not find its exact value.\n" -"\n" -"It would take several more decades, and their most brilliant student—the legendary Leonhard Euler—to solve it in 1734. Euler showed that:\n" -"$∑_{k=1}^\\infty 1/k^2 = \\pi^2/6$.\n" -"\n" -"(Our series starts at k=2, so it equals `π²/6 - 1`, but that's a minor detail.)\n" -"\n" -"## Our More Modest Goal\n" -"\n" -"In this level, we won't compute the exact value—that requires Euler's revolutionary techniques connecting series to trigonometric functions. Instead, we'll prove something more fundamental: **the series converges at all**.\n" +#. §0: `ε` +#. §1: `ε / 2` +#: Game.Levels.L11Levels.L02_IsCauchyOfSum +msgid "# Excellent work! Cauchy sequences are closed under addition!\n" "\n" -"## The Strategy: Comparison\n" +"You've just proven that the set of Cauchy sequences forms a well-behaved algebraic structure—they can be added together and the result is still Cauchy.\n" "\n" -"The key insight is to **compare** the Basel series with the Leibniz series from Levels 1-2. Observe that:\n" -"`1/(k+2)² = 1/((k+2)(k+2)) ≤ 1/((k+1)(k+2))`\n" +"## What this means\n" "\n" -"Why? Because `(k+2)² ≥ (k+1)(k+2)` for all `k ≥ 0`.\n" +"This theorem shows that the Cauchy property is **preserved by addition**. This is crucial because:\n" "\n" -"By the Series Order Theorem (Level 3), this means:\n" -"`∑_{k m`, set `[aₙ₊₁, bₙ₊₁] = [s, bₙ]`\n" -"\n" -"**Dependent Types Magic**: The type system *guarantees* that our construction maintains all necessary properties at each step. We're not just building sequences - we're building sequences *with proofs* that they satisfy our constraints!\n" -"\n" -"**Your Mission**: Implement this bisection algorithm and prove that the limit sequences converge to the least upper bound of `S`." +"Prove §0:\n" +"If §1, then §2 is Monotone." msgstr "" -#: Game.Levels.L22Levels.L02 -msgid "`(f : ℕ → ℝ → ℝ) (F : ℝ → ℝ) :=\n" -"∀ ε > 0, ∃ N, ∀ n ≥ N, ∀ x, |f n x - F x| < ε`\n" -"\n" -"The sequence `f : ℕ → ℝ → ℝ` of functions converges uniformly to `F : ℝ → ℝ`." +#. §0: `x ≠ 0` +#. §1: `0 < |x|` +#: Game.Levels.L7Levels.L00_Uniqueness +#: Game.Levels.L7Levels.L03_SeqInvLim +#: Game.Levels.L13Levels.L03_MonotoneSubseq +#: Game.Levels.L17Levels.L03 +#: Game.Levels.L18Levels.L01 +#: Game.Levels.L18Levels.L01 +#: Game.Levels.L19Levels.L03 +msgid "If §0, then §1." msgstr "" #: Game.Levels.L1RealAnalysisStory.L09_big_boss @@ -694,71 +875,19 @@ msgstr "" msgid "Lecture 2: Newton's Computation of π" msgstr "" -#: Game.Levels.L8Pset.L8Pset1 -msgid "For all `n : ℕ`, `2 * n + 9 ≤ 2 ^ (n + 4)`." -msgstr "" - -#: Game.Levels.L21Levels.L07 -msgid "# Level 3: Derivatives Everywhere\n" -"\n" -"In the previous level, we computed the derivative of `f(x) = x² - 1` at a single point `x = 2`. Now we'll prove something much more powerful: we'll find the derivative at **every** point!\n" -"\n" -"## From Point Derivatives to Derivative Functions\n" -"\n" -"So far, `FunDerivAt f L c` tells us that `f` has derivative `L` at the specific point `c`.\n" -"\n" -"But for most functions, we can compute derivatives at *every* point, giving us a **derivative function**.\n" -"\n" -"## The New Definition\n" -"\n" -"**Definition (`FunDeriv`):** We say that `g` is the derivative of `f` (everywhere) if:\n" -"\n" -"`∀ x, FunDerivAt f (g x) x`\n" -"\n" -"This is written `FunDeriv f g`.\n" -"\n" -"In other words: for each point `x`, the derivative of `f` at `x` equals `g(x)`.\n" -"\n" -"## The Power Rule\n" -"\n" -"For `f(x) = x² - 1`, we'll prove that `f'(x) = 2x` for all `x`.\n" -"\n" -"This is an instance of the **power rule**: `d/dx[xⁿ] = n·xⁿ⁻¹`.\n" -"\n" -"## Computing the General Derivative\n" -"\n" -"For arbitrary `x`, we need:\n" -"\n" -"`lim[h→0] (f(x + h) - f(x)) / h`\n" -"\n" -"` = lim[h→0] ((x + h)² - 1 - (x² - 1)) / h`\n" -"\n" -"` = lim[h→0] (x² + 2xh + h² - x²) / h`\n" -"\n" -"` = lim[h→0] (2xh + h²) / h`\n" -"\n" -"` = lim[h→0] h(2x + h) / h`\n" -"\n" -"` = lim[h→0] (2x + h)`\n" -"\n" -"` = 2x`\n" -"\n" -"## Your Challenge\n" -"\n" -"Prove that the derivative of `f(x) = x² - 1` is `g(x) = 2x` everywhere:\n" -"\n" -"`FunDeriv (fun x ↦ x^2 - 1) (fun x ↦ 2 * x)`\n" -"\n" -"**Hint:** You need to prove `∀ x, FunDerivAt (fun x ↦ x^2 - 1) (2 * x) x`.\n" -"\n" -"After introducing `x`, the proof is very similar to Level 2, but with `x` instead of `2`.\n" -"\n" -"Given `ε > 0`, use `δ = ε`. For `h ≠ 0` with `|h| < ε`, simplify:\n" -"- `(x + h)² - 1 - (x² - 1) = 2xh + h²`\n" -"- `(2xh + h²) / h = 2x + h` (for `h ≠ 0`)\n" -"- `|(2x + h) - 2x| = |h| < ε`" +#. §0: `a : ℕ → ℝ` +#. §1: `Monotone` +#. §2: `L` +#. §3: `n` +#. §4: `a n ≤ L` +#: Game.Levels.L17Pset.L05' +msgid "If §0 is §1 and has limit §2, then for all §3, §4." msgstr "" +#. §0: `lim_{n→∞} a(n) = L` +#. §1: `by_contra` +#. §2: `d` +#. §3: `d/2` #: Game.Levels.L7Levels.L00_Uniqueness msgid "## What You've Proven\n" "\n" @@ -774,102 +903,191 @@ msgid "## What You've Proven\n" "The uniqueness of limits is fundamental to the entire edifice of analysis. It ensures that:\n" "\n" "- When we define continuous functions using limits, the definitions are unambiguous\n" -"- Limit notation like `lim_{n→∞} a(n) = L` is well-defined\n" +"- Limit notation like §0 is well-defined\n" "- We can safely use limits in computations without worrying about multiple possible values\n" "- Many standard theorems that rely on \"the limit\" make sense\n" "\n" "## The Power of Contradiction\n" "\n" -"This proof also showcased the power of **proof by contradiction** (`by_contra`). When\n" +"This proof also showcased the power of **proof by contradiction** (§1). When\n" "direct proof seems difficult, assuming the opposite and deriving an impossibility can be\n" "an elegant and effective strategy. You'll use this technique many times throughout\n" "analysis.\n" "\n" -"The key insight was geometric: if two points are separated by distance `d`, then no third\n" -"point can be within distance `d/2` of both. This simple observation, made rigorous through\n" +"The key insight was geometric: if two points are separated by distance §2, then no third\n" +"point can be within distance §3 of both. This simple observation, made rigorous through\n" "epsilon-N arguments, gave us our contradiction." msgstr "" -#: Game.Levels.L10Pset.L10Pset7 -msgid "If a sequence `a : ℕ → ℝ` has two convergent subsequences, `a ∘ σ` converges to `L` and `a ∘ τ` converges to `M ≠ L`, then `a` is not convergent." -msgstr "" - -#: Game.Levels.L18Levels.L02 -msgid "If `a` decreases to `0`, then the alternating series `Series (fun n ↦ (-1)^n * a n)` converges." +#. §0: `a b c d e : ℕ → ℝ` +#. §1: `a` +#. §2: `c` +#. §3: `e` +#. §4: `L` +#. §5: `n` +#. §6: `a n ≤ b n ≤ c n ≤ d n ≤ e n` +#. §7: `b` +#. §8: `d` +#. §9: `L` +#: Game.Levels.L6Pset.L6Pset5 +msgid "# Problem 5\n" +"\n" +"You are given five sequences §0, and you know that\n" +"§1, §2, and §3 converge to §4, and that, for all §5, §6.\n" +"Prove that both §7 and §8 also converge to §9." msgstr "" #: Game.Levels.L17Pset.L05 msgid "Monotonicity of Series" msgstr "" -#: Game.Levels.L12Levels.L01_Choose -msgid "## What You've Accomplished\n" -"\n" -"You've mastered a crucial technique for extracting structured objects from existence statements. By using `choose` to convert the Twin Prime Conjecture into concrete functions, then applying orbit construction to make those functions monotonic, you've built a subsequence that is both strictly increasing and preserves the desired property.\n" -"\n" -"## The Power of `choose`\n" -"\n" -"This level revealed how existence statements like `∀ N, ∃ n > N, p n` are actually encoding:\n" -"- A **function** `τ : ℕ → ℕ` that produces witnesses\n" -"- **Proofs** that these witnesses satisfy the required properties\n" -"- The ability to **extract** these hidden structures for further use\n" -"\n" -"The `choose` tactic transforms abstract existence into concrete tools you can manipulate.\n" +#. §0: `intro` +#. §1: `∃` +#. §2: `use` +#. §3: `∀` +#. §4: `intro` +#. §5: `∀` +#. §6: `t` +#. §7: `t` +#. §8: `t_pos` +#. §9: `t > 0` +#. §10: `f : ℝ → ℝ` +#. §11: `hf : ∀ x > 0, f (x) = x^2` +#. §12: `f` +#. §13: `(x)` +#. §14: `f x` +#. §15: `f (x)` +#. §16: `f(x)` +#. §17: `f (t) = t^2` +#. §18: `apply hf` +#. §19: `hf` +#. §20: `f (t) = t²` +#. §21: `specialize` +#. §22: `specialize hf t` +#. §23: `hf` +#. §24: `t` +#. §25: `hf` +#. §26: `intro` +#. §27: `specialize hf t_pos` +#. §28: `specialize hf t t_pos` +#: Game.Levels.L1RealAnalysisStory.L07_specialize +msgid "# Using universal statements\n" "\n" -"## Bridging Existence and Structure\n" +"Now let's learn the flip side of §0. You have already learned that:\n" +"- if you have §1 in the goal, you write §2 to provide a specific value. And\n" +"- if you have §3 in the goal, you write §4 to introduce an arbitrary variable\n" "\n" -"The key insight is the two-step process:\n" -"1. **Extract witnesses** using `choose` to get a function `τ` satisfying the property\n" -"2. **Add structure** using orbit construction to get a subsequence `σ` that's both monotonic and property-preserving\n" +"But what if you have §5 in a *hypothesis* and you want to use it for a particular value?\n" "\n" -"This pattern - *existence → extraction → structuring* - appears throughout advanced mathematics.\n" +"For a concrete example, suppose you have:\n" +"- A positive real number §6; that is, a real number §7, together with a hypothesis, say, §8 that §9\n" +"- A function §10\n" +"- A hypothesis §11, meaning \"for all x positive, f (x) equals x²\". (Note that you *have* to put a space after §12 before §13 or else Lean will be very angry with you! In fact, Lean will often drop unnecessary parentheses, so you'll see §14 instead of §15 -- and again, definitely *not* §16.)\n" +"- And you want to prove the goal §17.\n" "\n" -"## Looking Ahead\n" +"Can you use §18? No! The hypothesis §19 says \"for all positive x, f (x) = x²\" but the goal asks specifically about §20. They're not the same.\n" "\n" -"You now have all the tools needed for the main theorem of this lecture. In the next level, you'll see this exact `choose` technique applied to extract subsequences from the negation of the Cauchy property. The orbit construction you've mastered will then be used to accumulate gaps and create the contradiction with boundedness.\n" +"This is where the §21 command comes in. You can write §22 to specialize the statement §23 to the particular value §24. This transforms §25 from \"∀ x > 0, f (x) = x²\" into \"t > 0 → f (t) = t²\". Just like we had to §26 multiple times (once for the dummy variable name, and again to name the hypothesis), we can specialize multiple times; so you can now write §27. Or you can kill two birds with one stone via: §28.\n" "\n" -"The ability to extract functions from complex quantified statements, then transform them to have the structure you need, is a fundamental skill in formal mathematics. You've seen how abstract number theory (Twin Prime Conjecture) and concrete analysis (orbit construction) can work together seamlessly." -msgstr "" - -#: Game.Levels.L3Levels.L02_OneOverN -msgid "Clear denominators in the goal: `field_simp`" +"I'm sure you can solve the goal from there yourself!" msgstr "" -#: Game.Levels.L18Levels.L02 -msgid "# Congratulations!\n" -"\n" -"You've just proven the **Alternating Series Test**—one of the most beautiful and practical convergence tests in real analysis!\n" +#. §0: `L` +#. §1: `M` +#. §2: `L` +#. §3: `M` +#. §4: `by_contra` +#. §5: `by_contra` +#. §6: `by_contra h` +#. §7: `h` +#. §8: `False` +#. §9: `abs_pos_of_nonzero` +#. §10: `x ≠ 0` +#. §11: `0 < |x|` +#. §12: `L ≠ M` +#. §13: `|L - M| > 0` +#. §14: `ε := |L - M| / 2` +#. §15: `N₁` +#. §16: `N₂` +#. §17: `L` +#. §18: `M` +#. §19: `N = N₁ + N₂` +#. §20: `n = N` +#. §21: `|L - M| ≤ |a N - L| + |a N - M| < ε + ε = |L - M|` +#. §22: `|L - M| < |L - M|` +#. §23: `L - M = (L - a(N)) + (a(N) - M)` +#: Game.Levels.L7Levels.L00_Uniqueness +msgid "# Level 1: Uniqueness of Limits\n" "\n" -"## What We've Accomplished\n" +"One of the fundamental properties of convergent sequences is that they converge to a\n" +"**unique** limit. This might seem obvious at first glance—after all, how could a sequence\n" +"be getting arbitrarily close to two different numbers? But as with many intuitive facts\n" +"in analysis, the rigorous proof requires careful reasoning with our epsilon-N definitions.\n" "\n" -"This theorem tells us that an alternating series $\\sum_{n=0}^{\\infty} (-1)^n \\cdot a_n$ converges whenever:\n" -"1. The terms $a_n$ are decreasing (antitone)\n" -"2. The terms approach zero: $a_n \\to 0$\n" +"The key to proving uniqueness is **proof by contradiction**. We'll assume a sequence\n" +"converges to two different limits §0 and §1, and show this leads to an impossibility.\n" +"The strategy involves choosing epsilon to be half the distance between §2 and §3, then\n" +"showing the sequence can't simultaneously stay that close to both limits.\n" "\n" -"These conditions are remarkably easy to check in practice!\n" +"## New Tools You'll Need\n" "\n" -"## The Power of the Proof Technique\n" +"### Proof by Contradiction: §4\n" "\n" -"The proof strategy—analyzing even and odd partial sums separately—is a powerful technique that appears throughout analysis:\n" -"- The even partial sums squeeze upward toward the limit\n" -"- The odd partial sums squeeze downward toward the limit\n" -"- They meet in the middle as $a_n \\to 0$\n" +"The §5 tactic allows us to prove a statement by assuming its negation and deriving\n" +"a contradiction. The syntax is §6, which adds a hypothesis §7 containing the\n" +"negation of the current goal and changes the goal to §8.\n" "\n" -"This \"pinching\" or \"squeezing\" argument is elegant and intuitive.\n" +"### §9\n" "\n" -"## A Crucial Observation: Conditional Convergence\n" +"If §10, then §11. This theorem is essential for working with distances between\n" +"distinct points.\n" "\n" -"Notice that the alternating harmonic series $\\sum_{k=1}^{\\infty} \\frac{(-1)^{k+1}}{k}$ converges by this test, but its absolute value series $\\sum_{k=1}^{\\infty} \\frac{1}{k}$ (the harmonic series) diverges!\n" +"## The Strategy\n" "\n" -"This makes it **conditionally convergent**—it converges, but not absolutely. As we discussed in the introduction to this lecture, such series have remarkable properties: their sums can be rearranged to converge to *any* real number, or even to diverge! This is **Riemann's Rearrangement Theorem**, which we'll explore in future levels.\n" +"Here's how the proof works:\n" "\n" -"## Historical Note\n" +"1. Assume for contradiction that §12\n" +"2. Then §13, so we can use §14 as our tolerance\n" +"3. Apply the convergence condition to get §15 and §16 for sequences converging to §17 and §18\n" +"4. Take §19 and evaluate at §20\n" +"5. Use the triangle inequality to show §21\n" +"6. This gives the contradiction: §22\n" "\n" -"Leibniz discovered this test in the 1670s while studying his famous series for $\\pi/4$ (also known centuries before to the Indian Madhava). It was one of the first convergence tests ever discovered, and it remains one of the most useful and elegant results in all of analysis.\n" +"The algebra in step 5 is the key: we write §23 and apply\n" +"the triangle inequality to get the impossible conclusion." +msgstr "" + +#. §0: `(f : ℝ → ℝ) (a b : ℝ) (N : ℕ) := +#. (b - a) / N * ∑ i ∈ range N, f (a + (i + 1) * (b - a) / N)` +#. §1: `f` +#. §2: `a` +#. §3: `b` +#. §4: `N` +#: Game.Levels.L22Levels.L03 +msgid "§0\n" "\n" -"## What's Next?\n" "\n" -"With absolute convergence (Level 1) and the alternating series test (Level 2) under our belt, we're now ready to explore the deep and sometimes counterintuitive theory of **rearrangements of series**—where the distinction between absolute and conditional convergence becomes truly dramatic!" +"The Riemann sum of §1 from §2 to §3 with §4 subintervals." +msgstr "" + +#. §0: `L` +#. §1: `a (n) = (3n + 8) / (2n + 5)` +#. §2: `a` +#. §3: `L` +#: Game.Levels.L3Pset.L3Pset4 +msgid "Determine the limit §0 of the sequence §1, and prove that §2 indeed converges to §3." +msgstr "" + +#. §0: `fₙ` +#. §1: `F` +#. §2: `fₙ` +#. §3: `[a, b]` +#. §4: `F` +#. §5: `[a, b]` +#. §6: `F` +#. §7: `fₙ` +#: Game.Levels.L25Levels.L01 +msgid "If §0 converges uniformly to §1, and each §2 is integrable on §3, then §4 is integrable on §5, and the integral of §6 equals the limit of the integrals of §7." msgstr "" #: Game.Levels.L19Levels.L03 @@ -918,468 +1136,706 @@ msgid "# Congratulations!\n" "In Level 4, we'll see the shocking flip side: Riemann's Rearrangement Theorem. For conditionally convergent series, rearrangements can make the sum equal to *any* real number. The contrast couldn't be more dramatic!" msgstr "" -#: Game.Levels.L20PsetIntro -msgid "Pset 20" -msgstr "" - +#. §0: `x` +#. §1: `s i` +#. §2: `i` +#. §3: `x` +#. §4: `s i` #: Game.Levels.L23Levels.L03 -msgid "A `Type` is an arbitrary mathematical object." +msgid "An element §0 is in the union of sets §1 if and only if there exists an index §2 such that §3 is in §4." msgstr "" -#: Game.Levels.L1RealAnalysisStory.L07_specialize -msgid "Now write `specialize hf t_pos` feed in the proof that `t > 0`; then you should be able to finish it yourself." +#: Game.Levels.L20PsetIntro +msgid "Pset 20" msgstr "" #: Game.Levels.L11Levels.L02_IsCauchyOfSum msgid "Level 2 : Sums of Cauchy sequences" msgstr "" -#: Game.Levels.L1RealAnalysisStory.L08_choose -msgid "Excellent! You've learned the `choose` tactic for working with existence in hypotheses.\n" -"\n" -"Notice the complete pattern:\n" -"1. `choose c hc using h` unpacked the hypothesis into a specific value `c` and proof `hc : f c = 2`\n" -"2. `use c` provided this same value as our witness for the goal\n" -"3. `rewrite [hc]` rewrote `f c` as `2` in the goal, changing it to `2^2 = 4`\n" -"4. `ring_nf` verified that `2 ^ 2 = 4`\n" -"\n" -"The symmetry is beautiful:\n" -"- `use` when you have `∃` in the goal (\"here's my specific example\")\n" -"- `choose` when you have `∃` in a hypothesis (\"let me unpack this existence claim\")\n" -"\n" -"This completes your basic logical toolkit! In real analysis, you'll use `choose` constantly when working with:\n" -"- Limit definitions (\"given ε > 0, there exists δ > 0...\")\n" -"- Intermediate Value Theorem (\"there exists c such that f(c) = 0\")\n" -"- Existence theorems throughout analysis\n" -"\n" -"You're now ready to tackle real mathematical proofs!" -msgstr "" - #: Game.Levels.L12Lecture msgid "# Lecture 12: Cauchy Sequences II" msgstr "" -#: Game.Levels.L3Pset.L3Pset3 -msgid "Determine what the limit of the sequence `1 / n ^ 2` is, and prove it." -msgstr "" - -#: Game.Levels.L1RealAnalysisStory.L00_the_problem -msgid "Perfect! You've completed your first Lean proof involving real numbers.\n" +#. §0: `a : ℕ → ℝ` +#. §1: `Antitone` +#. §2: `∀ n, 0 ≤ a n` +#. §3: `n ↦ ∑ k ∈ range (2n+1), (-1)^k * a k` +#. §4: `Antitone` +#: Game.Levels.L18Levels.L02 +msgid "If §0 is §1 and §2, then the odd alternating series §3 is §4." +msgstr "" + +#. §0: `ε/2` +#. §1: `|(f + g)(x) - (f + g)(c)| < ε` +#. §2: `|(f + g)(x) - (f + g)(c)| ≤ |f(x) - f(c)| + |g(x) - g(c)|` +#. §3: `ε/2` +#. §4: `ε` +#. §5: `min(δ₁, δ₂)` +#. §6: `δ₁` +#. §7: `f` +#. §8: `|f(x) - f(c)| < ε/2` +#. §9: `|x - c| < δ₁` +#. §10: `δ₂` +#. §11: `g` +#. §12: `|g(x) - g(c)| < ε/2` +#. §13: `|x - c| < δ₂` +#. §14: `min(δ₁, δ₂)` +#: Game.Levels.L20Levels.L03 +msgid "## What We've Learned\n" "\n" -"Remember: the `apply` tactic is used when you have what you need to prove the goal. Look at the top right: your list of tactics now includes `apply`, and if you forget how it works or what it does, just click on it for a reminder." -msgstr "" - -#: Game.Levels.L17Levels.L02 -msgid "# Level 2: Leibniz Series — Convergence\n" +"This theorem marks a major milestone: we've proven that continuity is **preserved under addition**!\n" "\n" -"In the previous level, you proved that the partial sums have an explicit formula:\n" -"`∑ k ∈ range n, a k = 1 - 1 / (n + 1)`\n" +"### The §0 Trick\n" "\n" -"Now it's time to prove rigorously that the infinite series **converges**.\n" +"This is one of the most elegant techniques in analysis:\n" "\n" -"## What We Need to Show\n" +"- We need to make §1\n" +"- By the triangle inequality: §2\n" +"- If each piece is less than §3, the sum is less than §4!\n" "\n" -"To prove `SeriesConv a`, we need to show that the sequence of partial sums converges to some limit `L`.\n" +"The beauty: we **split the budget**. Each function gets half the tolerance.\n" "\n" -"From the formula, it's clear that the limit should be `L = 1`, since:\n" -"`lim (n → ∞) [1 - 1/(n+1)] = 1 - 0 = 1`\n" +"### The §5 Strategy\n" "\n" -"But we need to prove this using the **ε-N definition** of convergence!\n" +"Why take the minimum of two deltas?\n" "\n" -"## The ε-N Challenge\n" +"- §6 works for §7: guarantees §8 when §9\n" +"- §10 works for §11: guarantees §12 when §13\n" +"- §14 works for **both**: it's the \"most restrictive\" requirement\n" "\n" -"We must show: for every `ε > 0`, there exists `N` such that for all `n ≥ N`:\n" -"`|∑ k ∈ range n, a k - 1| < ε`\n" +"**Key insight:** When combining guarantees, take the stronger (smaller) constraint!\n" "\n" -"Using the partial sum formula, this becomes:\n" -"`|(1 - 1/(n+1)) - 1| < ε`\n" +"### Building Up From Simple Pieces\n" +"\n" +"This is the beginning of a powerful story. We can now prove:\n" +"- Sums of continuous functions are continuous ✓\n" +"- Products of continuous functions are continuous (similar proof!)\n" +"- Compositions of continuous functions are continuous (chain rule!)\n" +"- Therefore: all polynomials, rational functions, trig functions, etc. are continuous!\n" "\n" -"Simplifying: `|−1/(n+1)| = 1/(n+1) < ε`\n" +"We've just laid the foundation for understanding continuity of essentially every function in calculus." +msgstr "" + +#. §0: `1 / n < ε` +#. §1: `have f3 : 0 < 1 / ε := by bound` +#: Game.Levels.L3Levels.L02_OneOverN +msgid "Now we need §0. First establish that everything is positive. Start with: §1" +msgstr "" + +#. §0: `σ(n) ≥ n` +#. §1: `a` +#. §2: `ε` +#. §3: `L` +#. §4: `a ∘ σ` +#. §5: `σ` +#. §6: `n ≥ N` +#. §7: `a` +#. §8: `L` +#. §9: `N` +#. §10: `a n → L` +#. §11: `L` +#. §12: `a` +#. §13: `a n = (-1)^n` +#. §14: `a(0), a(2), a(4), ... = 1, 1, 1, ...` +#. §15: `a(1), a(3), a(5), ... = -1, -1, -1, ...` +#. §16: `a n = (-1)^n` +#: Game.Levels.L10Levels.L08_Mono +msgid "Beautiful! That was remarkably simple for such a powerful theorem.\n" "\n" -"So we need: **given ε > 0, find N such that for all n ≥ N, we have 1/(n+1) < ε**.\n" +"**Why This Proof Works:**\n" "\n" -"## The Key Tool: Archimedean Property\n" +"The key insight is that subsequences can only \"spread out\" indices, never compress them. Since §0 always, if §1 is eventually within §2 of §3 (for all indices ≥ N), then §4 is too—because §5 maps §6 to even larger indices where §7 is still close to §8.\n" "\n" -"This is exactly what the **Archimedean Property** gives us! It says that for any `ε > 0`, there exists `N` such that `1/N < ε`.\n" +"The same §9 works for all subsequences!\n" "\n" -"Then for all `n ≥ N`, we have:\n" -"`1/(n+1) ≤ 1/n ≤ 1/N < ε`\n" +"**The Contrapositive: A Divergence Test**\n" "\n" -"## Your Task\n" +"The Subsequence Theorem says: *If §10, then every subsequence converges to §11.*\n" "\n" -"Prove that `SeriesConv a` using:\n" -"- The explicit formula from Level 1 (`LeibnizSeriesFinite`)\n" -"- The Archimedean Property (`ArchProp`)\n" -"- Careful inequality reasoning to show `1/(n+1) < ε`\n" +"By contrapositive: *If there exist two subsequences converging to different limits, then §12 does not converge.*\n" "\n" -"**Hint:** After using `ArchProp` to get your `N`, you'll need to do some work showing that `1/(n+1) ≤ 1/n ≤ 1/N < ε`. The tactics `field_simp` and `bound` will be your friends!" -msgstr "" - -#: Game.Levels.L22Levels.L03 -msgid "Integration" -msgstr "" - -#: Game.Levels.L1RealAnalysisStory.L05_use -msgid "There exists a real number that makes this binomial expansion work." -msgstr "" - -#: Game.Levels.L10PsetIntro -msgid "Pset 10" -msgstr "" - -#: Game.Levels.L20Levels.L01 -msgid "# Level 1: Introduction to Function Limits\n" +"This is a powerful tool for proving divergence!\n" "\n" -"Welcome to Lecture 20! We now shift our focus from sequences to **functions**. Just as we studied limits of sequences, we can study limits of functions as the input approaches a particular point.\n" +"**Example Application:**\n" "\n" -"## The Definition\n" +"Consider §13, which oscillates between -1 and 1:\n" +"- The even-indexed subsequence: §14 converges to 1\n" +"- The odd-indexed subsequence: §15 converges to -1\n" "\n" -"**Definition (`FunLimAt`):** We say that `f` has limit `L` at `x = c` if:\n" -"```\n" -"∀ ε > 0, ∃ δ > 0, ∀ x ≠ c, |x - c| < δ → |f x - L| < ε\n" -"```\n" +"Since we have subsequences converging to different limits (1 and -1), the sequence §16 does not converge. We'll see this in the next level!\n" "\n" -"This is written `FunLimAt f L c`. (First the function, then the limit, then \"at\" `x = c`.)\n" +"**Looking Ahead:**\n" "\n" -"**Reading the definition:** For *every* tolerance `ε` around the output value `L`, there exists a distance `δ` around the input value `c` such that whenever `x` is within `δ` of `c` (but not equal to `c`), the function value `f(x)` is within `ε` of `L`.\n" +"Subsequences are fundamental in analysis:\n" +"- **Bolzano-Weierstrass Theorem:** Every bounded sequence has a convergent subsequence\n" +"- **Compactness:** Sequential compactness is defined using subsequences\n" +"- **Cauchy sequences:** Can be understood through subsequences\n" +"- **limsup and liminf:** Defined as limits of monotone subsequences\n" "\n" -"## The Intuition\n" +"The concept generalizes to metric spaces and topological spaces, where it's crucial for understanding convergence and compactness.\n" "\n" -"The key difference from sequence limits is the condition `x ≠ c`. We care about what happens *near* c, but not at all about what happens *at* c. The function might not even be defined at `c`!\n" +"**Exercise:** Prove that if a sequence has two subsequences converging to different limits, then the sequence diverges. (Hint: use proof by contradiction—assume the sequence converges and derive that the two limits must be equal.)" +msgstr "" + +#. §0: `a : ℕ → ℝ` +#. §1: `L ≠ 0` +#. §2: `|a n|` +#. §3: `2|L|` +#: Game.Levels.L7Pset.L7Pset1 +msgid "# Problem 1\n" "\n" -"This is exactly what happens with the classic example:\n" +"Suppose that a sequence §0 converges to §1. Show that eventually §2 is at most\n" +"§3." +msgstr "" + +#: Game.Levels.L22Levels.L03 +msgid "Integration" +msgstr "" + +#. §0: `a : ℕ → ℝ` +#. §1: `Antitone` +#. §2: `∀ n, 0 ≤ a n` +#. §3: `n ↦ ∑ k ∈ range (2n), (-1)^k * a k` +#. §4: `Monotone` +#: Game.Levels.L18Levels.L02 +msgid "If §0 is §1 and §2, then the even alternating series §3 is §4." +msgstr "" + +#. §0: `use` +#. §1: `∃` +#. §2: `use` +#. §3: `c` +#. §4: `f (c) = 2` +#. §5: `h : ∃ (c : ℝ), f c = 2` +#. §6: `c` +#. §7: `(f c)^2 = 4` +#. §8: `apply h` +#. §9: `h` +#. §10: `c` +#. §11: `choose` +#. §12: `choose` +#. §13: `choose c hc using h` +#. §14: `c` +#. §15: `c` +#. §16: `hc` +#. §17: `c` +#: Game.Levels.L1RealAnalysisStory.L08_choose +msgid "# Extracting information from existential quantifiers\n" "\n" -"`f(x) = (x² - 1)/(x - 1)`\n" +"Now let's learn the counterpart to §0. You know that if you have §1 in the goal, you write §2 to provide a specific value.\n" "\n" -"At `x = 1`, the function is \"undefined\" (because it's `0/0`; in Lean, this is equal to `0`). But for `x ≠ 1`, we can factor:\n" +"But suppose you have a *hypothesis* that says \"there exists a real number §3 such that §4\". In Lean, this looks like:\n" +"§5\n" "\n" -"`f(x) = (x² - 1)/(x - 1) = (x - 1)(x + 1)/(x - 1) = x + 1`\n" +"And say you want to prove that \"there exists a real number §6 such that §7\".\n" "\n" -"So as x approaches 1, `f(x)` approaches some constant `L`. Your job: figure out `L`, and prove that it's the limit!\n" +"Again, you can't just say §8 because these are different statements.\n" +"If you know from §9 that at least one such §10 exists, how do you *choose* one?\n" +" The name of this command is... §11.\n" "\n" -"## Your Challenge\n" +"The syntax for §12 is as follows:\n" "\n" -"Prove that there exists a limit `L` such that:\n" +"§13.\n" "\n" -"`FunLimAt (fun x ↦ (x^2 - 1)/(x - 1)) L 1`\n" +"You need to give a name to both the value of §14, and to the hypothesis with which §15 is bundled. Here we named it §16 (a hypothesis about §17).\n" "\n" -"In other words, prove that the function `f(x) = (x² - 1)/(x - 1)` has *some* limit as `x` approaches `1`." +"You should be able to figure out how to solve the goal from here." msgstr "" -#: Game.Levels.L21Levels.L07 -msgid "The Derivative Function" +#: Game.Levels.L1RealAnalysisStory.L05_use +msgid "There exists a real number that makes this binomial expansion work." msgstr "" -#: Game.Levels.L17Pset.L05' -msgid "# Level 2: Monotone Limit Bound\n" +#. §0: `specialize` +#. §1: `hf : ∀ x > 0, f (x) = x^2` +#. §2: `specialize hf t` +#. §3: `hf : t > 0 → f (t) = t ^ 2` +#. §4: `specialize` +#. §5: `specialize hf t_pos` +#. §6: `hf` +#. §7: `hf : f (t) = t ^ 2` +#. §8: `apply hf` +#. §9: `intro` +#. §10: `∀` +#. §11: `specialize` +#. §12: `∀` +#: Game.Levels.L1RealAnalysisStory.L07_specialize +msgid "Great! You've learned the §0 tactic.\n" +"\n" +"Notice what happened:\n" +"1. Initially, §1 was a universal statement\n" +"2. §2 transformed it into §3\n" +"3. Another §4 command, namely §5 turned the\n" +"hypothesis §6 into §7\n" +"4. And finally, §8 worked because the hypothesis matched the goal.\n" +"\n" +"The pattern is:\n" +"- §9 when you have §10 in the goal (\"introduce an arbitrary term...\")\n" +"- §11 when you have §12 in a hypothesis (\"apply the hypothesis to specific value...\")\n" +"\n" +"This is fundamental in real analysis when working with:\n" +"- Function properties that hold \"for all x\"\n" +"- Limit definitions involving \"for all ε > 0\"\n" +"- Continuity statements\n" "\n" -"Prove the theorem `MonotoneLimitBound`:\n" -"Suppose that a sequence `a : ℕ → ℝ` is `Monotone` and has limit `L`. Then\n" -"for every `n`, `a n ≤ L`." +"Last lesson in Lecture 1 coming up." msgstr "" -#: Game.Levels.L1RealAnalysisStory.L03_rw -msgid "The `rewrite` tactic replaces the left-hand side of an equality with the right-hand side in the goal. The syntax is `rewrite [hypothesis_name1, hypothesis_name2, etc]`." +#. §0: `abs_Lipschitz` +#. §1: `0 ≤ x` +#. §2: `abs_of_nonneg` +#. §3: `abs_neg` +#: Game.Levels.L7Pset.L7Pset3 +msgid "# Problem 3\n" +"\n" +"Prove §0, obviously without referring to that theorem!\n" +"(Hint: you'll want to break things into cases according to whether §1 or not,\n" +"then systematically use §2 and §3...)" msgstr "" -#: Game.Levels.L2NewtonsCalculationOfPi.L01_SeqConvDef -msgid "The `norm_num` tactic can normalize numerical constants and functions of them." +#: Game.Levels.L10PsetIntro +msgid "Pset 10" msgstr "" -#: Game.Levels.L19Levels.L04 -msgid "# Congratulations!\n" -"\n" -"You've reached the pinnacle of our journey through series and rearrangements—Riemann's Rearrangement Theorem!\n" -"\n" -"## The Complete Picture\n" -"\n" -"We now have the full story about infinite summation and commutativity:\n" -"\n" -"**Level 3 (Rearrangement Theorem)**: Absolute convergence → rearrangement invariance\n" -"- The sum never changes, no matter how we reorder\n" -"- Infinite series behave like finite sums\n" -"\n" -"**Level 4 (Riemann's Theorem)**: Conditional convergence → complete chaos\n" -"- The sum can be *anything* we want by choosing the right rearrangement\n" -"- Order is everything; the series has no \"true\" sum independent of ordering\n" -"\n" -"There is no middle ground. Every convergent series falls into exactly one of these two categories.\n" -"\n" -"## Why Both Subseries Must Diverge\n" -"\n" -"A key insight: if `∑ a_n` converges but `∑ |a_n|` diverges, then both the series of positive terms and the series of negative terms must diverge to infinity. If either converged, we could show absolute convergence, a contradiction. This dual divergence is what gives us the freedom to hit any target—we never run out of positive or negative terms to adjust the sum.\n" -"\n" -"## The Greedy Algorithm\n" +#. §0: `n` +#. §1: `Even` +#. §2: `∃ k, n = 2 * k` +#. §3: `Odd` +#. §4: `∃ k, n = 2 * k + 1` +#: Game.Levels.L18Pset.L05 +msgid "A natural number §0 is either §1 (that is, §2), or §3 (that is, §4)" +msgstr "" + +#: Game.Levels.L21Levels.L07 +msgid "The Derivative Function" +msgstr "" + +#. §0: `Type` +#: Game.Levels.L23Levels.L03 +msgid "A §0 is an arbitrary mathematical object." +msgstr "" + +#. §0: `ε` +#. §1: `b (n)` +#. §2: `ε` +#. §3: `L` +#. §4: `a (n)` +#. §5: `c (n)` +#. §6: `ε` +#. §7: `L` +#. §8: `b (n)` +#. §9: `b (n)` +#. §10: `ε` +#. §11: `L` +#: Game.Levels.L6Levels.L06_Squeeze +msgid "# Level 7 Big Boss: Squeeze Theorem\n" "\n" -"The construction is elegant: alternately add positive terms (to push the sum up) and negative terms (to pull it back down), always staying close to our target `L`. Since `a_n → 0`, we need fewer and fewer terms for each adjustment, the oscillations shrink, and we converge exactly to `L`. Every term appears exactly once, making this a genuine rearrangement.\n" +"Welcome to another Big Boss level! You're about to prove one of the most elegant and powerful theorems in real analysis: the Squeeze Theorem (also known as the Sandwich Theorem or Pinching Theorem). This theorem beautifully captures the intuitive idea that if you trap a sequence between two other sequences that both converge to the same limit, then the trapped sequence must also converge to that limit.\n" "\n" -"## Philosophical Implications\n" +"The Squeeze Theorem is a perfect showcase for how the logical tools you've been developing—working with conjunctions, absolute values, and inequalities—come together to prove deep mathematical results. You'll need to orchestrate all your skills: extracting information from convergence conditions, managing multiple epsilon-N arguments simultaneously, and combining inequalities with absolute value manipulations.\n" "\n" -"This theorem reveals a profound truth about infinity: our finite intuitions can fail dramatically. In finite arithmetic, addition is always commutative. But in the infinite realm, commutativity is a *privilege*, not a given—it requires absolute convergence.\n" +"**The Intuitive Picture:**\n" +"Imagine three runners on a track. Runner A and Runner C are both heading to the same finish line L, and Runner B is always between them. No matter how A and C weave back and forth, as long as they both end up at L and B stays between them, B must also end up at L. There's simply nowhere else for B to go!\n" "\n" -"Conditionally convergent series are delicate balances between positive and negative contributions. The terms go to zero, but not fast enough to make the series absolutely convergent. This creates a twilight zone where order determines everything.\n" +"**The Mathematical Challenge:**\n" +"The formal proof requires careful epsilon management. Given any tolerance §0, you need to show that §1 gets within §2 of §3. Since §4 and §5 both get within §6 of §7, and §8 is squeezed between them, you can use the transitivity of inequalities to show that §9 is also within §10 of §11." +msgstr "" + +#. §0: `a : ℕ → ℝ` +#. §1: `L` +#. §2: `L ≠ 0` +#. §3: `N` +#. §4: `n ≥ N` +#. §5: `|a (n)| ≥ |L| / 2` +#: Game.Levels.L7Levels.L01_Eventually +msgid "If §0 converges to §1 and §2, then there is an §3 so that\n" +"for all §4, §5." +msgstr "" + +#. §0: `(n + 1) / n` +#. §1: `L` +#: Game.Levels.L3Pset.L3Pset2 +msgid "Prove that the sequence §0 has a limit §1 and determine what it is." +msgstr "" + +#. §0: `a : ℕ → ℝ` +#. §1: `b : ℕ → ℝ` +#. §2: `a + b` +#. §3: `a` +#. §4: `b` +#. §5: `ε/2` +#. §6: `N₁ + N₂` +#. §7: `|(a + b)ₘ - (a + b)ₙ|` +#. §8: `|(aₘ - aₙ) + (bₘ - bₙ)|` +#. §9: `ε / 2` +#. §10: `ε` +#: Game.Levels.L11Levels.L02_IsCauchyOfSum +msgid "# Level 2: Sums of Cauchy Sequences\n" "\n" -"## Historical Impact\n" +"Now that we know convergent sequences are Cauchy, let's explore how Cauchy sequences behave under arithmetic operations. Just like we proved that sums of convergent sequences converge, we'll show that sums of Cauchy sequences are Cauchy.\n" "\n" -"When Riemann proved this in 1854, it revolutionized analysis. Mathematicians realized that:\n" -"- Convergence alone is insufficient to guarantee good behavior\n" -"- Absolute convergence is the \"right\" condition for most theorems\n" -"- Infinite processes are more subtle and treacherous than previously thought\n" +"This theorem is important because it shows that the Cauchy property is preserved by addition—a crucial fact we'll need when we eventually define the real numbers!\n" "\n" -"This theorem helped establish the modern rigorous foundations of analysis, showing that careful definitions and proofs are essential when dealing with infinity.\n" +"## The Setup\n" "\n" -"## The Bigger Lesson\n" +"Given:\n" +"- §0 is Cauchy\n" +"- §1 is Cauchy\n" "\n" -"The contrast between Levels 3 and 4 teaches us that mathematical phenomena often exhibit sharp dichotomies. There's no \"mostly commutative\" or \"almost absolutely convergent\"—you either have the property or you have complete chaos. This all-or-nothing behavior appears throughout mathematics and is part of its austere beauty.\n" +"Prove: §2 is Cauchy\n" "\n" -"## Looking Forward\n" +"## Strategy\n" "\n" -"These ideas extend far beyond series:\n" -"- Fubini's theorem (changing order of integration) requires absolute convergence\n" -"- Products of series (Cauchy product) require absolute convergence\n" -"- Term-by-term operations on series require absolute convergence\n" +"This proof follows a familiar pattern from the sum of limits theorem:\n" "\n" -"The distinction between absolute and conditional convergence is one of the most important concepts in all of analysis. You now understand it at the deepest level!\n" +"1. **Split epsilon**: Apply the Cauchy property to both §3 and §4 using §5\n" +"2. **Take the maximum N**: Use §6 to ensure both Cauchy conditions hold\n" +"3. **Change the goal**: Express §7 as §8\n" +"4. **Triangle inequality**: Split the sum into two pieces\n" +"5. **Combine estimates**: Each piece is less than §9, so the total is less than §10\n" "\n" -"## A Final Thought\n" +"## Key Insight\n" "\n" -"You've just completed one of the most beautiful and surprising journeys in mathematics. From the simple question \"does rearranging terms change the sum?\" we've uncovered a rich theory that distinguishes two fundamentally different types of convergence and reveals the subtle nature of infinity.\n" +"The beauty of the Cauchy property is that we don't need to know *where* the sequences converge—we only need to know that their terms get close to *each other*. This self-referential definition makes the proof very similar to the sum of limits, but without ever mentioning a limit!\n" "\n" -"This is real analysis at its finest—unexpected, profound, and ultimately satisfying. Well done!" +"Let's prove it!" msgstr "" #: Game.Levels.L4PsetIntro msgid "Pset 4" msgstr "" -#: Game.Levels.L3Levels.L01_ArchProp -msgid "Try `use ⌈1 / ε⌉₊ + 1`. Of course you can use other values of `N`, but then I won't be able to give you more hints..." -msgstr "" - #: Game.Levels.L19Lecture msgid "Lecture 19: Rearrangements" msgstr "" -#: Game.Levels.L24Levels.L03 -msgid "`(S : Set ℝ) (L : ℝ) : Prop := IsUB S L ∧ ∀ M, IsUB S M → L ≤ M`\n" -"\n" -"The point `L` is a least upper bound (supremum) of the set `S` if `L` is an upper bound of `S`, and for any other upper bound `M` of `S`, we have `L ≤ M`." -msgstr "" - +#. §0: `a n ≤ K` +#. §1: `L ≤ K` +#. §2: `K` +#. §3: `K` +#. §4: `SeqBddBy` +#. §5: `a` +#. §6: `M` +#. §7: `a n ≤ M` +#. §8: `n` +#. §9: `SeqBdd a` +#. §10: `|a n| ≤ M` +#. §11: `SeqBddBy a M` +#. §12: `M` +#. §13: `a n ≤ M` +#. §14: `a n → L` +#. §15: `a n ≤ K` +#. §16: `n` +#. §17: `L ≤ K` +#. §18: `L > K` +#. §19: `L - K > 0` +#. §20: `ε` +#. §21: `N` +#. §22: `|a N - L| < L - K` +#. §23: `a N > L - (L - K) = K` +#. §24: `a N ≤ K` +#. §25: `K` +#. §26: `K` +#. §27: `a n < K` +#. §28: `n` +#. §29: `L ≤ K` +#. §30: `L < K` +#. §31: `a n = 1/n` +#. §32: `a n > 0` +#. §33: `n` +#. §34: `lim a n = 0` #: Game.Levels.L10Levels.L07_Order msgid "# Level 2: Order Limit Theorem\n" "\n" "So far we've focused on algebraic operations with limits. Now we explore how limits interact with **inequalities**.\n" "\n" -"**The Question:** If every term of a sequence satisfies `a n ≤ K`, does the limit also satisfy `L ≤ K`?\n" +"**The Question:** If every term of a sequence satisfies §0, does the limit also satisfy §1?\n" "\n" -"The answer is **YES**! Limits preserve weak inequalities. This is intuitive: if a sequence is always below some ceiling `K`, it can't suddenly jump above `K` in the limit.\n" +"The answer is **YES**! Limits preserve weak inequalities. This is intuitive: if a sequence is always below some ceiling §2, it can't suddenly jump above §3 in the limit.\n" "\n" -"**New Definition: `SeqBddBy`**\n" +"**New Definition: §4**\n" "\n" -"We say a sequence `a` is **bounded by** `M` if `a n ≤ M` for all `n`.\n" +"We say a sequence §5 is **bounded by** §6 if §7 for all §8.\n" "\n" "Note the difference:\n" -"- `SeqBdd a`: sequence is bounded (both above and below), i.e., `|a n| ≤ M`\n" -"- `SeqBddBy a M`: sequence is bounded **above** by `M`, i.e., `a n ≤ M`\n" +"- §9: sequence is bounded (both above and below), i.e., §10\n" +"- §11: sequence is bounded **above** by §12, i.e., §13\n" "\n" -"**The Theorem:** If `a n → L` and `a n ≤ K` for all `n`, then `L ≤ K`.\n" +"**The Theorem:** If §14 and §15 for all §16, then §17.\n" "\n" "**Proof Strategy: Contradiction!**\n" "\n" -"Assume `L > K`. Then `L - K > 0`. Use this as your `ε` in the definition of convergence:\n" -"- There exists `N` such that `|a N - L| < L - K`\n" -"- This means `a N > L - (L - K) = K`\n" -"- But we know `a N ≤ K` by hypothesis\n" +"Assume §18. Then §19. Use this as your §20 in the definition of convergence:\n" +"- There exists §21 such that §22\n" +"- This means §23\n" +"- But we know §24 by hypothesis\n" "- **Contradiction!**\n" "\n" -"The key insight: if the limit were strictly above `K`, then eventually the terms would have to be above `K` too (by convergence). But they're not!\n" +"The key insight: if the limit were strictly above §25, then eventually the terms would have to be above §26 too (by convergence). But they're not!\n" "\n" -"**Warning:** Strict inequalities are NOT preserved! If `a n < K` for all `n`, we can only conclude `L ≤ K`, not `L < K`.\n" +"**Warning:** Strict inequalities are NOT preserved! If §27 for all §28, we can only conclude §29, not §30.\n" "\n" -"Example: `a n = 1/n` satisfies `a n > 0` for all `n`, but `lim a n = 0`, which is not strictly positive.\n" +"Example: §31 satisfies §32 for all §33, but §34, which is not strictly positive.\n" "\n" "This theorem can also be used to prove the **Squeeze Theorem** (which we already did directly)." msgstr "" -#: Game.Levels.L12Levels.L00_SubseqIterate -msgid "For a function `σ : ℕ → ℕ`, we have that: `σ (σ^[k]) = σ^[k+1]`." -msgstr "" - -#: Game.Levels.L7Levels.L03_SeqInvLim -msgid "## Congratulations, Big Boss Defeated!\n" -"\n" -"You've just completed one of the most challenging proofs in elementary analysis! The\n" -"reciprocal limit theorem is a major milestone—you've proven that reciprocals preserve\n" -"convergence (when the limit is nonzero).\n" -"\n" -"## What You Accomplished\n" -"\n" -"This proof required you to orchestrate multiple sophisticated techniques:\n" -"- Using `EventuallyGeHalfLim` to ensure denominators stay bounded away from zero\n" -"- Choosing a carefully calibrated epsilon (`ε · |L|² / 2`) to make the algebra work\n" -"- Manipulating complex fractional expressions with common denominators\n" -"- Applying `abs_div` to separate absolute values across division\n" -"- Chaining together a sequence of inequalities to reach the final bound\n" -"\n" -"Each step built on the previous levels, showing how mathematical proofs are constructed\n" -"from carefully assembled building blocks.\n" -"\n" -"## Applications and Extensions\n" -"\n" -"With this theorem in hand, you now have a complete toolkit for limits of **rational\n" -"functions**. Combined with earlier results on sums and products, you can now prove:\n" -"\n" -"**If `a n → L` and `c n → M` with `M ≠ 0`, then `a n / c n → L / M`.**\n" -"\n" -"The proof is straightforward: first show `1/c n → 1/M` using the reciprocal theorem you\n" -"just proved, then use the product theorem to show `a n · (1/c n) → L · (1/M) = L/M`.\n" -"\n" -"This completes the fundamental arithmetic of limits: sums, products, and quotients. These\n" -"are the building blocks for analyzing limits of polynomials, rational functions, and much\n" -"more complex expressions throughout calculus and analysis.\n" +#. §0: `f(x) = x ^ 2` +#. §1: `∑ i ∈ Finset.range n, (i + 1) ^ 2 = (n * (n + 1) * (2 * n + 1)) / 6` +#. §2: `f(x) = x ^ 2` +#. §3: `[a,b]` +#: Game.Levels.L22Pset.L04 +msgid "# Level 4: Integral Exercise\n" "\n" -"## Mastery of Technique\n" +"As you may imagine, the proof that §0 is integrable will involve the following formula for the sum of squares:\n" "\n" -"The reciprocal theorem showcases a crucial lesson in mathematical proof: sometimes the\n" -"\"right\" epsilon isn't the obvious choice. The expression `ε · |L|² / 2` might seem\n" -"mysterious at first, but it's precisely engineered to make the final inequalities work out.\n" -"This kind of strategic thinking—working backwards from what you need to figure out what\n" -"you should assume—is at the heart of mathematical problem-solving.\n" +"§1.\n" "\n" -"You've now mastered the essential techniques for proving limit theorems. Well done!" +"(All as real numbers.) Prove it. Then in natural language, prove that §2 is integrable on §3." msgstr "" -#: Game.Levels.L3Levels.L02_OneOverN -msgid "Presumably you know that you\n" -"should `choose N hN using f1` at this stage. But maybe you'd like to give `hN` a more descriptive name (so that I can keep giving you hints). Try `choose N eps_inv_lt_N using f1`." +#. §0: `n` +#. §1: `n < 2 ^ n` +#: Game.Levels.L8Levels.L03_Induction' +#: Game.Levels.L8Pset.L8Pset1 +msgid "For all §0, §1." msgstr "" -#: Game.Levels.L23Levels.L02 -msgid "# Level 2: Integration Converges!\n" -"\n" -"**The Big Question**: We know that continuous functions *should* be integrable, but proving this rigorously is surprisingly subtle. The key insight is that we need *uniform* continuity, not just pointwise continuity.\n" -"\n" -"**What We're Proving**: If `f` is uniformly continuous on `[a,b]`, then the sequence of Riemann sums `{RiemannSum f a b n}` converges as `n → ∞`. This means the integral exists!\n" -"\n" -"**The Strategy**: We'll prove convergence by showing the Riemann sum sequence is Cauchy. For any `ε > 0`:\n" -"1. Use uniform continuity to get a `δ` that works everywhere on `[a,b]`\n" -"2. Choose `N` large enough so that partitions with `≥ N` subintervals are all fine enough\n" -"3. For any `m, n ≥ N`, compare `RiemannSum f a b m` and `RiemannSum f a b n` by using their common multiple `m * n` as an intermediate step\n" -"4. Apply your Level 1 theorem twice to bound the total error\n" +#. §0: `bound` +#. §1: `|X| = X` +#. §2: `h : 0 ≤ X` +#. §3: `abs_of_nonneg` +#. §4: `h : 0 ≤ X` +#. §5: `|X| = X` +#. §6: `have factName : |X| = X := by apply abs_of_nonneg h` +#: Game.Levels.L3Pset.L3Pset4 +msgid "# Problem 4\n" "\n" -"**New Definition - Uniform Continuity**:\n" +"Here's an even more involved limit problem. We've had luck getting §0 to prove §1, especially when there's a hypothesis §2 already available in the list of assumptions. But I've found it not to be reliable, unfortunately. So let me give you one more theorem for your toolchest.\n" "\n" -"`def UnifContOn (f : ℝ → ℝ) (S : Set ℝ) : Prop :=\n" -" ∀ ε > 0, ∃ δ > 0, ∀ x ∈ S, ∀ y ∈ S, |x - y| < δ → |f x - f y| < ε`\n" +"## New Theorem: §3.\n" +"If you have a hypothesis §4 in your toolchest,\n" +"then you can prove that §5 via:\n" "\n" -"**Key Insight**: Notice the quantifier order! Unlike pointwise continuity where `δ` can depend on the specific point `x`, uniform continuity requires a single `δ` that works for *all* pairs of points simultaneously. This seemingly small change makes all the difference for integration theory." +"§6." msgstr "" #: Game.Levels.L1RealAnalysisStory.L08_choose msgid "The choose tactic" msgstr "" -#: Game.Levels.L24Levels.L01 -msgid "A finite list has a maximum element." +#. §0: `f` +#. §1: `[a,b]` +#. §2: `f` +#. §3: `N → ∞` +#: Game.Levels.L23Levels.L02 +msgid "If a function §0 is uniformly continuous on §1, then the Riemann sums of §2 converge to a limit as §3." +msgstr "" + +#. §0: $x ^ 2 + 2 * y = x ^ 2 + 2 * y$ +#. §1: `h` +#. §2: `x = 5` +#. §3: `apply h` +#. §4: `x = 5` +#. §5: `x ^ 2 + 2 * y = x ^ 2 + 2 * y` +#. §6: `apply something` +#. §7: `something` +#. §8: `rfl` +#: Game.Levels.L1RealAnalysisStory.L02_rfl +msgid "# When things are identical to themselves\n" +"\n" +"Sometimes in mathematics, we need to prove that something equals itself. For example, we might need to prove that §0.\n" +"\n" +"This isn't quite the same as our previous exercise. There, we had a hypothesis §1 that told us §2, and we used §3 to prove the goal §4.\n" +"\n" +"But now we don't have any hypothesis that says §5. We're just being asked to prove that some expression equals itself. We can't say §6 because there's no §7.\n" +"\n" +"Instead, we will use what mathematicians call the *reflexive property* of equality: everything is equal to itself. In Lean, if you get to a situation where you're trying to prove an equality, and the two things on both sides are *identical*, then the syntax is to give the command §8 (short for \"reflexivity\").\n" +"\n" +"Try it out!" msgstr "" -#: Game.Levels.L14Levels.L01_BolzanoWeierstrass -msgid "# Level 1 **Big Boss:** Bolzano-Weierstrass\n" +#. §0: `L` +#. §1: `L` +#. §2: `L` +#. §3: `a : ℕ → ℝ` +#. §4: `L` +#. §5: `L ≠ 0` +#. §6: `N` +#. §7: `n ≥ N` +#. §8: `|a (n)| ≥ |L| / 2` +#. §9: `n` +#. §10: `ε = |L| / 2` +#. §11: `L ≠ 0` +#. §12: `|L| > 0` +#. §13: `ε = |L| / 2` +#. §14: `N` +#. §15: `|a (n) - L| < |L| / 2` +#. §16: `n ≥ N` +#. §17: `a (n)` +#. §18: `|L| / 2` +#. §19: `L` +#. §20: `|a (n)| ≥ |L| / 2` +#. §21: $$|L| = |a (n) + (L - a (n))| \\leq |a (n)| + |L - a (n)| < |a (n)| + \\frac{|L|}{2}$$ +#. §22: `|a (n)| > |L| / 2` +#: Game.Levels.L7Levels.L01_Eventually +msgid "# Level 2: Eventually—Convergent Sequences Stay Near Their Limits\n" "\n" -"This is it. The crown jewel. One of the most celebrated theorems in all of real analysis.\n" +"When a sequence converges to a nonzero limit, it doesn't just get arbitrarily close to\n" +"that limit—it **eventually stays away from zero** as well. This \"eventually bounded away\n" +"from zero\" property is crucial for many theorems involving quotients and reciprocals.\n" "\n" -"**The Bolzano-Weierstrass Theorem:** Every bounded sequence has a Cauchy subsequence.\n" +"The intuition is straightforward: if a sequence is converging to some nonzero value §0,\n" +"then eventually the sequence terms must be at least half as large (in absolute value) as\n" +"§1 itself. They can't simultaneously be approaching §2 and shrinking toward zero.\n" "\n" -"Think about what this says. Take *any* sequence confined to a bounded region—no matter how wildly it oscillates, no matter how chaotic its behavior—and this theorem *guarantees* you can extract from it a subsequence that converges (is Cauchy). Boundedness alone is enough to ensure hidden convergent behavior exists somewhere within.\n" +"## What We're Proving\n" "\n" -"This theorem is the foundation for:\n" -"- Proving continuous functions on closed intervals attain their max and min\n" -"- Understanding compactness in metric spaces\n" -"- Existence proofs throughout optimization and differential equations\n" -"- Sequential compactness arguments everywhere in analysis\n" +"**Theorem:** If §3 converges to §4 with §5, then there exists §6 such\n" +"that for all §7, we have §8.\n" "\n" -"And here's the beautiful part: **you've already done all the hard work.** This lecture is about watching the pieces fall into place.\n" +"In other words, once §9 is large enough, the sequence stays at least half as far from\n" +"zero as the limit is.\n" "\n" -"## The Architecture\n" +"## The Strategy\n" "\n" -"Over the past few lectures, you've been building a cathedral. Today, we place the capstone:\n" +"The key is to use the convergence condition with §10:\n" "\n" -"**Lecture 12:** Bounded monotone sequences are Cauchy (you proved this)\n" +"1. Since §11, we have §12, so §13 is a valid positive epsilon\n" +"2. Convergence gives us §14 such that §15 for all §16\n" +"3. This means §17 is within distance §18 of §19\n" +"4. By the reverse triangle inequality, this forces §20\n" "\n" -"**Pset 12:** Bounded antitone sequences are Cauchy (dual by negation)\n" +"The algebraic key is recognizing that:\n" +"§21\n" "\n" -"**Lecture 13:** Sequences without unbounded peaks → have monotone subsequences (you proved this)\n" +"Rearranging gives us §22.\n" "\n" -"**Pset 13:** Sequences with unbounded peaks → have antitone subsequences (you'll prove this)\n" +"## Why This Matters\n" "\n" -"**Today:** We combine everything. Any bounded sequence either has unbounded peaks or doesn't. In either case, we extract a monotone (or antitone) bounded subsequence, which must be Cauchy by our earlier results.\n" +"This result is essential for the next level, where we'll prove that reciprocals of\n" +"convergent sequences converge. We need to know that the denominators don't approach zero,\n" +"which would cause the reciprocals to blow up. This theorem provides exactly that guarantee!" +msgstr "" + +#: Game.Levels.L24Levels.L01 +msgid "A finite list has a maximum element." +msgstr "" + +#. §0: `Ball (x : ℝ) (r : ℝ) : Set ℝ := Ioo (x - r) (x + r)` +#. §1: `r` +#. §2: `x` +#. §3: `(x - r, x + r)` +#: Game.Levels.L23Levels.L03 +msgid "§0\n" "\n" -"The proof is short—maybe the shortest \"big theorem\" proof you'll see—precisely because we've built the right machinery. Every complex proof should feel like this at the end: inevitable.\n" +"A ball of radius §1 centered at §2 is the open interval §3." +msgstr "" + +#. §0: `N * (N + 1)` +#: Game.Levels.L9Pset.L9Pset2 +msgid "# Problem 2\n" "\n" -"## New Theorems (From Your Work)\n" +"Prove that §0 is always even." +msgstr "" + +#. §0: `[a,b]` +#. §1: `[a,b]` +#. §2: `S = {t ∈ [a,b] : [a,t] can be covered by finitely many balls}` +#. §3: `S ⊆ [a,b]` +#. §4: `b` +#. §5: `a` +#. §6: `a ∈ S` +#. §7: `S` +#. §8: `L` +#. §9: `L = b` +#. §10: `L < b` +#. §11: `L` +#. §12: `L` +#. §13: `[L-δ, L+δ]` +#. §14: `L = sup S` +#. §15: `t ∈ S` +#. §16: `t > L-δ` +#. §17: `[a,t]` +#. §18: `t ∈ S` +#. §19: `[t, L+δ]` +#. §20: `L` +#. §21: `[a, L+δ]` +#. §22: `L+δ ∈ S` +#. §23: `L` +#. §24: `S` +#. §25: `[a,b]` +#: Game.Levels.L24Levels.L04 +msgid "# Level 4: Heine-Borel Theorem: Part 2a\n" "\n" -"**abs_le:** The companion to `abs_lt` for non-strict inequalities. Says `|x| ≤ y ↔ -y ≤ x ≤ y`, letting us split absolute value bounds into simultaneous one-sided inequalities.\n" +"**The Hard Direction Begins**: Now for the converse! We need to prove that every closed bounded interval §0 is compact. This is where the real analysis gets deep.\n" "\n" -"**IsCauchy_of_AntitoneBdd:** From Pset 12. If a sequence is antitone (non-increasing) and bounded below, it's Cauchy. Dual to the monotone result.\n" +"**The Challenge**: Given any open cover of §1 by balls, we must extract a finite subcover. But how do you go from \"every point is covered\" to \"finitely many balls suffice\"?\n" "\n" -"**AntitoneSubseq_of_UnBddPeaks:** From Pset 13. If a sequence has unbounded peaks, we can extract an antitone (non-increasing) subsequence by picking the peaks themselves.\n" +"**The Brilliant Strategy - Growing Intervals**:\n" +"We'll use your Least Upper Bound Property in a clever way:\n" "\n" -"## The Strategy\n" +"1. **Define the \"Good Set\"**: Let §2\n" "\n" -"The proof uses **case analysis** with the dichotomy from Lecture 13:\n" +"2. **Show S is Bounded Above**: Obviously §3, so §4 is an upper bound\n" "\n" -"**Case 1: Unbounded peaks exist**\n" -"- Extract an antitone subsequence (by `AntitoneSubseq_of_UnBddPeaks`)\n" -"- It's bounded below (inherits from the original sequence)\n" -"- Therefore it's Cauchy (by `IsCauchy_of_AntitoneBdd`)\n" +"3. **Show S is Non-empty**: Since our cover includes some ball containing §5, we have §6\n" "\n" -"**Case 2: Unbounded peaks don't exist**\n" -"- Extract a monotone subsequence (by `MonotoneSubseq_of_BddPeaks`)\n" -"- It's bounded above (inherits from the original sequence)\n" -"- Therefore it's Cauchy (by `IsCauchy_of_MonotoneBdd`)\n" +"4. **Apply LUB**: By Level 3, §7 has a supremum §8. The magic is showing §9!\n" "\n" -"Either way, we get a Cauchy subsequence. The theorem falls out from the law of excluded middle plus our carefully constructed library of results.\n" +"**The Key Insight**: If §10, then §11 itself is covered by some ball in our covering. But balls have positive radius, so this ball covers not just §12 but some interval §13. Since §14, there's some §15 with §16. Now we can:\n" +"- Cover §17 with finitely many balls (since §18)\n" +"- Cover §19 with the single ball around §20\n" +"- Combine them to cover §21\n" "\n" -"## What You'll Learn\n" +"This means §22, contradicting that §23 is an upper bound for §24!\n" "\n" -"Beyond the theorem itself, this lecture teaches you:\n" +"**Why This Works**: The proof exploits the tension between:\n" +"- **Discrete**: Finite covers (what we want to construct)\n" +"- **Continuous**: The supremum property (what Level 3 gives us)\n" +"- **Open**: Balls have positive radius (what creates the contradiction)\n" "\n" -"1. **Proof architecture:** How to structure a theory so that major theorems become natural consequences of well-chosen lemmas\n" +"**Your Mission**: Implement this supremum-based argument. You'll need to carefully handle the cases and use the fact that every point in §25 is covered by some ball with positive radius.\n" "\n" -"2. **Case analysis:** Using `by_cases` to split on a proposition and handle each case separately\n" +"This is where topology meets real analysis in its full glory!" +msgstr "" + +#. §0: `[a,b]` +#. §1: `[a,b]` +#. §2: `[a,b]` +#. §3: `S is compact ⟺ S is closed and bounded` +#: Game.Levels.L24Levels.L04 +msgid "# The Crown Jewel Achievement!\n" "\n" -"3. **Duality:** How proving one direction (monotone) often gives you the other (antitone) almost for free\n" +"You've just proved that **closed intervals are compact**! This is one of the most important theorems in all of real analysis.\n" "\n" -"4. **Synthesis:** Combining multiple prior results into something greater than the sum of its parts\n" +"**What Made This Proof Extraordinary**:\n" +"- **Three Mathematical Universes Colliding**: Your proof beautifully combined:\n" +" - **Topology** (open covers and balls)\n" +" - **Real Analysis** (supremums and the LUB property)\n" +" - **Logic** (proof by contradiction)\n" +"- **The Supremum Trick**: The idea of considering the set of points where finite covering \"reaches\" was pure genius. You turned a global problem (covering all of §0) into a supremum problem.\n" +"- **Positive Radius Magic**: The contradiction came from the fact that balls have positive radius - if you can finitely cover up to the supremum, the ball covering the supremum lets you \"jump past\" it.\n" "\n" -"## Historical Note\n" +"**Why This Result is Fundamental**:\n" +"- **Calculus Foundation**: Every time you integrate a continuous function on §1, you're using this theorem! Continuous functions on compact sets are uniformly continuous, hence integrable.\n" +"- **Optimization**: Every continuous function on §2 attains its maximum and minimum (extreme value theorem) - because compact sets are where continuous functions behave nicely.\n" +"- **Approximation Theory**: Polynomial approximation theorems (like Weierstrass) rely heavily on compactness of intervals.\n" "\n" -"Bernard Bolzano (1781-1848) and Karl Weierstrass (1815-1897) were pioneers of rigorous analysis. They understood a profound insight:\n" +"**The Historical Significance**: This theorem was the missing piece that made 19th-century analysis rigorous. Before understanding compactness, mathematicians had intuitions about why closed intervals were \"nice\" but couldn't prove it.\n" "\n" -"**Boundedness + Infinity → Accumulation**\n" +"**What's Left**: You've proved that all closed intervals are compact. Level 5 will extend this to prove that ANY closed and bounded set is compact, by showing that closed subsets of compact sets inherit compactness.\n" "\n" -"If you have infinitely many values trapped in a bounded region, they *must* cluster somewhere. There's nowhere else to go. This theorem makes that intuition precise and constructive.\n" +"**The Payoff**: Once you complete Level 5, you'll have the complete Heine-Borel theorem:\n" "\n" -"## The Payoff\n" +"§3\n" "\n" -"With Bolzano-Weierstrass in hand, a vast landscape of analysis opens up:\n" -"- Extreme Value Theorem (continuous functions on closed intervals attain bounds)\n" -"- Intermediate Value Theorem (continuous functions hit all intermediate values)\n" -"- Heine-Borel Theorem (characterizing compact sets in ℝⁿ)\n" -"- Sequential compactness arguments throughout topology\n" -"- Fixed point theorems\n" -"- And so much more...\n" -"\n" -"This isn't just a theorem. It's a *key* that unlocks doors throughout mathematics.\n" -"\n" -"## Let's Do This\n" -"\n" -"You've climbed the mountain. The summit is in sight. Time to prove one of the most important theorems in real analysis.\n" +"You could in theory stop at this point, because closed intervals are what we were after for applications to convergence of Riemann sums and uniform continuity. But the full Heine-Borel theorem is a cornerstone of real analysis, so let's finish the job!\n" "\n" -"The proof is elegant, almost anticlimactic. That's how you know you've done mathematics right: when the final step feels obvious because you've laid the groundwork so carefully.\n" +"**Looking Back**: Your journey from compactness ⟹ boundedness (Level 1) to this deep result shows the power of mathematical abstraction. You've connected the discrete (finite covers), the continuous (supremums), and the topological (open sets) into one unified theory.\n" "\n" -"**Ready? Let's prove Bolzano-Weierstrass.**" +"You're almost at the summit of one of mathematics' great theorems! 🏔️" msgstr "" #: Game.Levels.L1Pset.L1Pset2 @@ -1395,105 +1851,176 @@ msgstr "" msgid "Problem 2" msgstr "" -#: Game.Levels.L8Levels.L03_Induction' -msgid "# Level 1: Induction\n" +#. §0: `(a : ℕ → ℝ) := SeriesConv (fun n ↦ |a n|)` +#. §1: `a : ℕ → ℝ` +#. §2: `∑ |a n|` +#: Game.Levels.L18Levels.L01 +msgid "§0\n" +"\n" +"We say that a sequence §1 converges absolutely if §2 converges." +msgstr "" + +#. §0: `AbsSeriesConv` +#. §1: `Series a` +#. §2: `AbsSeriesConv` +#. §3: `Series (fun n ↦ |a n|)` +#. §4: $$\\sum_{k=1}^{\\infty} \\frac{(-1)^{k+1}}{k} = 1 - \\frac{1}{2} + \\frac{1}{3} - \\frac{1}{4} + \\cdots$$ +#. §5: `Conv_of_AbsSeriesConv` +#. §6: $\\sum |a_k|$ +#. §7: $|\\sum a_k|$ +#. §8: `DiffOfSeries` +#. §9: `Series_abs_add` +#. §10: `Conv_of_AbsSeriesConv` +#: Game.Levels.L18Levels.L01 +msgid "# Level 1: Absolute Convergence Implies Convergence\n" +"\n" +"In this level, we introduce the concept of **absolute convergence** and prove one of the fundamental theorems about series: if a series converges absolutely, then it converges.\n" +"\n" +"## New definition: §0\n" +"\n" +"A series §1 is said to converge *absolutely* (§2) if the series of absolute values\n" +"§3 converges.\n" "\n" -"In this level, you'll prove your first theorem by mathematical induction: for all natural numbers `n`, we have `n < 2^n`. This captures the fundamental fact that exponential functions grow faster than linear functions.\n" +"This is a *stronger* condition than ordinary convergence. For instance, the alternating harmonic series\n" +"§4\n" +"converges but does *not* converge absolutely (since the harmonic series diverges).\n" +"\n" +"## The Main Result\n" +"\n" +"**Theorem** (§5): If a series converges absolutely, then it converges.\n" +"\n" +"In other words: *absolute convergence implies convergence*.\n" "\n" "## Proof Strategy\n" "\n" -"The proof follows the standard induction template:\n" +"The key insight is that if the series of absolute values converges, then it is Cauchy, which means the tails of the series get arbitrarily small. By the triangle inequality, if §6 is small, then §7 is also small.\n" "\n" -"**Base Case (`n = 0`):** Show that `0 < 2^0 = 1`. This is straightforward.\n" +"We will use two helper lemmas (to be proved as homework):\n" +"- §8: The difference of partial sums equals the sum over the interval\n" +"- §9: The triangle inequality for finite sums\n" "\n" -"**Inductive Step:** Assume `k < 2^k` (the inductive hypothesis `hk`). Prove that `k + 1 < 2^(k+1)`.\n" +"Your task: Prove §10 using the Cauchy criterion and these lemmas." +msgstr "" + +#. §0: `∑ k ∈ range (m + 1), f k = f 0 + ∑ k ∈ range m, f (k+1)` +#. §1: `sum_range_succ` +#: Game.Levels.L18Pset.L08 +msgid "§0. This pulls out the first\n" +"term in the sum instead of §1, which pulls out the last term." +msgstr "" + +#. §0: `choose` +#. §1: `k` +#. §2: `τ(n)` +#. §3: `n+1` +#. §4: `n ≤ k` +#. §5: `τ(n)` +#. §6: `n > k` +#. §7: `if-then-else` +#. §8: `τ'` +#. §9: `τ'` +#. §10: `σ` +#. §11: `a(σ(n)) ≤ a(σ(n+1))` +#. §12: `if-then-else` +#. §13: `τ'` +#. §14: `k` +#. §15: `τ` +#. §16: `k` +#. §17: `lt_of_not_ge` +#. §18: `choose` +#. §19: `if-then-else` +#: Game.Levels.L13Levels.L03_MonotoneSubseq +msgid "# 🎉 Congratulations!\n" "\n" -"The key challenge is connecting `k + 1` to `2^(k+1) = 2 · 2^k`. While the inductive hypothesis gives us `k < 2^k`, we need to show `k + 1 < 2 · 2^k`.\n" +"You've just proved one of the most elegant results in real analysis: sequences without unbounded peaks have monotone subsequences. Let's appreciate what you accomplished.\n" "\n" -"If we can show that `k + 1 ≤ 2k`, then we'd have:\n" +"## What You Built\n" "\n" -"`k + 1 ≤ 2k < 2 · 2^k = 2^(k+1)`\n" +"Starting with just the hypothesis that peaks don't go on forever, you:\n" "\n" -"However, `k + 1 ≤ 2k` is only true when `k ≥ 1`. This means you'll need to handle two cases in the inductive step:\n" -"- When `k = 0`: Check directly that `1 < 2`\n" -"- When `k ≠ 0`: Use the inequality `k + 1 ≤ 2k`\n" +"1. **Extracted structure from negation** - Used §0 to get a bound §1 and witnesses §2 beyond which no peaks exist\n" "\n" -"## New Tools You'll Need\n" +"2. **Patched together a global function** - Combined §3 (for §4) and §5 (for §6) using §7 to create §8 that grows everywhere\n" "\n" -"### `induction'`\n" -"The syntax for induction is: `induction' n with k hk`\n" -"- Apply induction on the variable `n`\n" -"- Use `k` as the dummy variable in the inductive step\n" -"- Use `hk` as the name for the induction hypothesis\n" +"3. **Leveraged orbits** - Applied the Lecture 12 technique of iterating §9 to build a strictly increasing subsequence §10\n" "\n" -"This creates two goals:\n" -"1. **Base case:** Prove the statement for `n = 0`\n" -"2. **Inductive step:** With hypothesis `hk : (statement for k)`, prove the statement for `k + 1`\n" +"4. **Extracted monotonicity** - Showed that beyond the peak bound, each step must climb: §11\n" "\n" -"### `ge_one_of_nonzero`\n" -"If `n : ℕ` and `n ≠ 0`, then `1 ≤ n`. Apply this with `apply ge_one_of_nonzero` when you have a hypothesis that `n ≠ 0`.\n" +"The proof is a masterclass in constructive mathematics: you didn't just show a subsequence *exists*—you *built* it explicitly using orbits and witnesses.\n" "\n" -"## Hints\n" +"## The Bigger Picture: A Fundamental Dichotomy\n" "\n" -"- Use `induction' n with k hk` to begin\n" -"- The base case should be handled with `norm_num`\n" -"- In the inductive step, use `by_cases hk0 : k = 0` to split into two cases\n" -"- When `k = 0`, use `rewrite [hk0]` and `norm_num`\n" -"- When `k ≠ 0`, use `ge_one_of_nonzero` to get `1 ≤ k`, then build a chain of inequalities with `bound` and `linarith`\n" -"- Use `ring_nf` to simplify `2 * 2^k = 2^(k+1)`" -msgstr "" - -#: Game.Levels.L18Levels.L01 -msgid "Absolute Convergence Implies Convergence" -msgstr "" - -#: Game.Levels.L21Levels.L07 -msgid "# Outstanding Achievement!\n" +"Every sequence falls into exactly one of two camps:\n" "\n" -"You've just proved the **power rule** from first principles! This is one of the most fundamental results in calculus, and you've established it rigorously using limit definitions.\n" +"- **Unbounded peaks:** Infinitely many positions from which the sequence never recovers → You can extract a **non-increasing** (antitone) subsequence (your homework!)\n" "\n" -"## What You Accomplished\n" +"- **Bounded peaks:** Eventually, no more peaks appear → You just proved there's a **non-decreasing** (monotone) subsequence\n" "\n" -"You proved that for `f(x) = x² - 1`, the derivative function is `f'(x) = 2x` **everywhere**. This means:\n" -"- At any point `x`, the instantaneous rate of change is `2x`\n" -"- The slope of the tangent line at `(x, x² - 1)` is exactly `2x`\n" -"- The function has a well-defined derivative at every real number\n" +"This dichotomy is profound: *chaos is impossible*. No matter how wild a sequence appears, somewhere within it lies monotonic order. Either it keeps hitting new peaks (descending order), or it eventually runs out of peaks (ascending order). There is no third option.\n" "\n" -"## From Specific to General\n" +"## The Technique: Conditional Construction\n" "\n" -"Notice the beautiful progression:\n" -"- **Level 2:** Derivative at one point (`x = 2` gives `f'(2) = 4`)\n" -"- **Level 3:** Derivative everywhere (`f'(x) = 2x` for all `x`)\n" +"The §12 construct was crucial here. We needed a single function §13 that:\n" +"- Works for *all* natural numbers (not just those beyond §14)\n" +"- Grows faster than identity everywhere\n" +"- Matches our witness function §15 where it matters (beyond §16)\n" "\n" -"Your Level 2 result now emerges as a special case: `f'(2) = 2(2) = 4` ✓\n" +"The conditional definition elegantly threaded this needle. Combined with §17 to handle the logic, we converted a partially-defined witness into a globally-defined building block for our orbit.\n" "\n" -"## The Power Rule Emerges\n" +"This pattern—patching together local information into global constructions—appears throughout analysis. You've now mastered a fundamental technique.\n" "\n" -"You've discovered a fundamental pattern:\n" -"- `f(x) = x²` has `f'(x) = 2x = 2x¹`\n" -"- This suggests the general rule: `d/dx[xⁿ] = n·xⁿ⁻¹`\n" +"## Looking Ahead: Bolzano-Weierstrass\n" "\n" -"The constant `-1` disappeared because constants have derivative zero—another fundamental rule you've implicitly used!\n" +"In your homework, you'll prove the complementary result for sequences with unbounded peaks. The proof is actually simpler: just take the peaks themselves as your subsequence!\n" "\n" -"## The Algebraic Magic\n" +"Then in Lecture 14, we'll combine both results with the bounded monotone sequence theorem (Lecture 12) to prove the **Bolzano-Weierstrass Theorem**:\n" "\n" -"The key insight was recognizing that for **any** `x`:\n" -"`(x + h)² - x² = 2xh + h²`\n" +"**Every bounded sequence has a Cauchy subsequence.**\n" "\n" -"This factorization:\n" -"- Makes the `h` in the denominator cancel cleanly\n" -"- Leaves `2x + h`, which approaches `2x` as `h → 0`\n" -"- Works regardless of the value of `x`\n" +"That's right—boundedness alone guarantees convergent behavior. This is one of the crown jewels of real analysis, and you've just built half of its foundation.\n" "\n" -"## Universal vs. Particular\n" +"## What You've Mastered\n" "\n" -"This level demonstrated the power of **universal quantification** (`∀ x`). Instead of proving the result for each individual point, you proved it holds for **every** point simultaneously. This is the essence of mathematical generality!\n" +"✓ **Proof by cases:** Using negation and §18 to extract witnesses from non-existence\n" "\n" -"## Looking Ahead\n" +"✓ **Conditional definitions:** Building functions with §19 to patch local into global\n" "\n" -"You now have the tools to understand **continuity everywhere**. Just as we moved from point derivatives to derivative functions, we can move from point continuity to global continuity. Can you guess what comes next?\n" +"✓ **Orbit construction:** Iterating functions to force monotonic growth\n" "\n" -"The derivative function `f'(x) = 2x` you just found is itself a function—is it continuous? Spoiler alert: absolutely!" +"✓ **Strategic thinking:** Breaking complex proofs into: unpack hypothesis → build auxiliary objects → extract desired properties\n" +"\n" +"These aren't just tricks for one theorem—they're fundamental tools you'll use throughout mathematics.\n" +"\n" +"## Final Thought\n" +"\n" +"You stood at the crossroads of chaos and order. You proved that beyond a certain point, if peaks cease to exist, then climbing never stops. The sequence may not increase at every step, but along some carefully chosen path—an orbit through phase space—it marches upward inexorably.\n" +"\n" +"This is the power of subsequences: they let us *choose* our vantage point, focusing only on the moments that matter. And it's the power of formal proof: what seems intuitively obvious (\"if there are no peaks, something must be going up\") becomes a rigorous construction you can trust completely.\n" +"\n" +"Next up: What happens when peaks *don't* stop? Spoiler: they fall forever.\n" +"\n" +"**Ready for the homework? Time to make those peaks tumble down!**" +msgstr "" + +#: Game.Levels.L18Levels.L01 +msgid "Absolute Convergence Implies Convergence" +msgstr "" + +#. §0: `rfl` +#: Game.Levels.L1RealAnalysisStory.L02_rfl +msgid "Write §0 since we're proving that something equals itself." +msgstr "" + +#. §0: `|x| < y` +#. §1: `-y < x ∧ x < y` +#: Game.Levels.L6Levels.L05_AbsLt +msgid "This says that §0 if and only if §1." +msgstr "" + +#. §0: `N ≤ n` +#. §1: `have f4 : N * ε ≤ n * ε := by bound` +#: Game.Levels.L3Levels.L02_OneOverN +msgid "Multiply the inequality §0 by ε: §1" msgstr "" #: Game.Levels.L13PsetIntro @@ -1506,1500 +2033,2139 @@ msgstr "" msgid "A compact set is closed." msgstr "" +#. §0: `have f2 : |1 / (n : ℝ)| = 1 / n := by bound` #: Game.Levels.L3Levels.L02_OneOverN -msgid "Combine everything with `linarith [eps_inv_lt_N, f4]`" +msgid "Simplify the absolute value: §0. Note the explicit casting to the reals, so that this is not a statement about natural numbers!" +msgstr "" + +#. §0: `x` +#. §1: `x²` +#. §2: `t²` +#. §3: `t` +#: Game.Levels.L1RealAnalysisStory.L07_specialize +msgid "If a function of §0 always equals §1, then it equals §2 when evaluated at §3." +msgstr "" + +#. §0: `norm_num` +#: Game.Levels.L2NewtonsCalculationOfPi.L01_SeqConvDef +msgid "The §0 tactic can normalize numerical constants and functions of them." msgstr "" #: Game.Levels.L18PsetIntro msgid "Pset 18" msgstr "" +#. §0: `bound` +#. §1: `1 / ε < ↑(⌈1 / ε⌉₊ + 1)` +#. §2: `⌈1 / ε⌉₊ + 1` +#. §3: `fact` +#. §4: `bound` +#. §5: `push_cast` +#. §6: `1 / ε < ↑⌈1 / ε⌉₊ + 1` +#. §7: `1` +#: Game.Levels.L3Levels.L01_ArchProp +msgid "You might think that the §0 tactic\n" +"would also be able to solve §1, but No!\n" +"That's because the addition §2 happens as **natural numbers**, and only then is the result cast to the reals; so the\n" +"§3 that was just proved is not useful to §4. Instead try: §5 to get the casting to push down as far as possible.\n" +"The Goal will change to §6, where now the\n" +"ceiling is cast to the reals, and then the real number §7 is added." +msgstr "" + +#. §0: `EventuallyGeHalfLimPos` +#. §1: `L ≠ 0` +#: Game.Levels.L7Levels.L04_ByCases +msgid "Prove §0, but without the assumption that §1." +msgstr "" + +#. §0: `specialize hf t_pos` +#. §1: `t > 0` +#: Game.Levels.L1RealAnalysisStory.L07_specialize +msgid "Now write §0 feed in the proof that §1; then you should be able to finish it yourself." +msgstr "" + +#. §0: `f → L` +#. §1: `x → c` +#. §2: `k · f → k · L` +#: Game.Levels.L20Pset.L03 +msgid "# Level 3: Const Times Limit\n" +"\n" +"Prove that if §0 as §1, then §2." +msgstr "" + #: Game.Levels.L20Levels.L04 -msgid "## What We've Learned\n" +msgid "Sequential Criterion for Limits (Forward Direction)" +msgstr "" + +#. §0: `Series a` +#. §1: `a` +#: Game.Levels.L19Levels.L03 +msgid "If §0 converges absolutely, then any rearrangement of §1 also converges, and to the same sum." +msgstr "" + +#. §0: `ring_nf` +#: Game.Levels.L1RealAnalysisStory.L04_ring_nf +msgid "Write §0 to expand and simplify both sides algebraically." +msgstr "" + +#. §0: `a : ℕ → ℝ` +#: Game.Levels.L6Pset.L6Pset4 +msgid "# Problem 4\n" "\n" -"This theorem is a **bridge between two worlds**: sequences and functions!\n" +"You are given that a sequence §0 with the property that it takes arbitrarily large values exceeding 10 in absolute value.\n" +"Prove that cannot have a limit less than 5." +msgstr "" + +#. §0: `RearrangementThm` +#. §1: `∑ a_n` +#. §2: `σ : ℕ → ℕ` +#. §3: `∑ a_(σ(n))` +#. §4: `AbsSeriesConv a` +#. §5: `L` +#. §6: `Rearrangement` +#. §7: `σ` +#. §8: `SeriesLim (a ∘ σ) L` +#. §9: `Series_image` +#. §10: `σ` +#. §11: `sum_sdiff` +#. §12: `∑ (S₂ \\ S₁) + ∑ S₁ = ∑ S₂` +#. §13: `abs_sum_le_sum_abs` +#: Game.Levels.L19Levels.L03 +msgid "# Level 3 **Big Boss**: Rearrangement Theorem\n" "\n" -"### Why This Matters\n" +"This is it—the moment we've been building toward! We're about to prove one of the most profound and beautiful theorems in all of real analysis.\n" "\n" -"The Sequential Criterion gives us two powerful tools:\n" +"## The Fundamental Theorem\n" "\n" -"1. **Testing function limits with sequences**: Instead of wrestling with `ε`-`δ`, we can use specific sequences\n" -"2. **Connecting different areas of analysis**: Sequence convergence and function limits are deeply related\n" +"**Theorem** (§0): If a series §1 converges absolutely, then for any rearrangement §2, the rearranged series §3 converges to the same limit.\n" "\n" -"### The Proof Strategy: Composing Guarantees\n" +"In symbols: If §4, then there exists §5 such that, for all §6s, §7, (including the identity) and §8.\n" "\n" -"The proof elegantly chains together two limit definitions:\n" +"## The Deep Meaning\n" "\n" -"1. **Function limit** gives us: `ε → δ` (tolerance on output gives tolerance on input)\n" -"2. **Sequence limit** gives us: `δ → N` (tolerance on distance from `c` gives a threshold index)\n" -"3. **Composition**: `ε → δ → N` (tolerance on output gives threshold for the sequence `f(xₙ)`)\n" +"This theorem reveals a profound truth about infinite summation:\n" "\n" -"This is a beautiful example of **modular reasoning**: we use the guarantees from each definition without re-proving them!\n" +"**Infinite summation is commutative if and only if the series is absolutely convergent.**\n" "\n" -"### Looking Ahead\n" +"For finite sums, we can add terms in any order—the sum doesn't change. This theorem says that absolute convergence is *exactly* what's needed to extend this property to infinite sums!\n" "\n" -"There's a converse to this theorem (the backward direction): if `f(xₙ) → L` for **every** sequence `xₙ → c` with `xₙ ≠ c`, then `FunLimAt f L c`.\n" +"## Why This is a Big Deal\n" "\n" -"Together, these give us a complete equivalence:\n" +"Remember from Lecture 18 how we showed that rearranging the infinite matrix changed its sum from 0 to -2? That's because those series were *not* absolutely convergent.\n" "\n" -"`FunLimAt f L c ⟺ (for all sequences xₙ → c with xₙ ≠ c, we have f(xₙ) → L)`\n" +"For absolutely convergent series, we have complete freedom: reorder the terms however you like, and the sum stays the same. It's as if absolute convergence gives infinite series the \"finite property\" of commutativity.\n" "\n" -"This means we can choose our weapon: use `ε`-`δ` when convenient, or use sequences when that's easier!\n" +"## New Theorems\n" "\n" -"**Key insight:** Different formulations of the same concept give us flexibility in proofs. The sequential characterization often provides better intuition than the abstract `ε`-`δ` definition." -msgstr "" - -#: Game.Levels.L18Lecture -msgid "# Lecture 18: Infinite Addition\n" +"- §9: Relates the rearranged series to a sum over the image of §10\n" +"- §11: Handles sums over set differences: §12\n" +"- §13: Triangle inequality for finite sums\n" "\n" -"**SIMPLICIO:** Does rearranging the terms of a series change its sum?\n" +"## The Proof Strategy\n" "\n" -"**SOCRATES:** Great question! Here's the way I like to illustrate this idea (that I learned from Walter Rudin's books). Imagine a massive\n" -"matrix, $M$, infinite in both directions, to the right, and down. It is upper triangular, has $-1$s on the diagonal, and at\n" -"position $(i, j)$ for $i < j$ its entry is $1/ 2 ^ {(j - i + 1)}$. So $M$ looks like this:\n" +"We'll combine everything from Levels 1 and 2:\n" +"1. The strong Cauchy property tells us that scattered large-index terms contribute negligibly\n" +"2. The eventually covers property tells us that rearrangements eventually include all early terms\n" +"3. We'll show the rearranged series stays close to the original by bounding the \"uncovered\" terms\n" "\n" -"$\n" -"\\begin{pmatrix}\n" -"-1 & 1/2 & 1/4 & 1/8 & 1/16 & \\cdots \\\\\n" -"0 & -1 & 1/2 & 1/4 & 1/8 & \\cdots \\\\\n" -"0 & 0 & -1 & 1/2 & 1/4 & \\cdots \\\\\n" -"0 & 0 & 0 & -1 & 1/2 & \\cdots \\\\\n" -"\\vdots & \\vdots & \\vdots & \\vdots & \\vdots & \\ddots\n" -"\\end{pmatrix}\n" -"$\n" +"This is a technical proof, but the idea is beautiful: absolute convergence gives us enough \"slack\" that scrambling the order doesn't matter.\n" "\n" -"What is the sum of the elements in $M$?\n" +"Your task: Prove the Rearrangement Theorem—and unlock one of the deepest truths about infinite series!" +msgstr "" + +#. §0: `MonotoneLimitBound` +#. §1: `a : ℕ → ℝ` +#. §2: `Monotone` +#. §3: `L` +#. §4: `n` +#. §5: `a n ≤ L` +#: Game.Levels.L17Pset.L05' +msgid "# Level 2: Monotone Limit Bound\n" "\n" -"**SIMPLICIO:** Ok let's see if we can work this out. Hmm this isn't so hard, I'll sum the rows, and\n" -"then add those up.\n" +"Prove the theorem §0:\n" +"Suppose that a sequence §1 is §2 and has limit §3. Then\n" +"for every §4, §5." +msgstr "" + +#. §0: `(a : ℕ → X) (n : ℕ) := ∀ m > n, a m ≤ a n` +#. §1: `a : ℕ → X` +#. §2: `X` +#. §3: `ℚ` +#. §4: `ℝ` +#. §5: `n : ℕ` +#. §6: `IsAPeak a n` +#. §7: `∀ m > n, a m ≤ a n` +#: Game.Levels.L13Levels.L03_MonotoneSubseq +msgid "§0\n" "\n" -"The first row sums to $-1 + 1/2 + 1/4 + 1/8 + \\cdots = 0$.\n" +"For a sequence §1 (where §2 is §3 or §4) and §5, we say that §6 if: §7." +msgstr "" + +#. §0: `Continuous on [a,b] → Uniformly Continuous on [a,b] → Integrable on [a,b]` +#. §1: `[a,b]` +#. §2: `ℝ` +#. §3: `∫₀¹ f(x)dx` +#. §4: `[0,1]` +#. §5: `[0,1]` +#: Game.Levels.L23Levels.L03 +msgid "# The Grand Synthesis!\n" "\n" -"The second row sum is $0 + -1 + 1/2 + 1/4 + \\cdots = 0$ as well.\n" +"You've just completed one of the most beautiful proofs in mathematics! You've shown that **continuity + compactness = uniform continuity**.\n" "\n" -"In fact, every row obviously sums to $0$. So the sum of all the elements in $M$ is $0$.\n" +"**What Makes This Proof Extraordinary**:\n" +"- **Local to Global**: You started with local information (continuity at each point) and used compactness to extract global information (uniform continuity everywhere)\n" +"- **Infinite to Finite**: The proof converts an infinite covering problem into a finite one, where you can actually compute minima\n" +"- **Abstract to Concrete**: You used the abstract concept of compactness to solve the concrete problem of finding a uniform δ\n" "\n" -"**SOCRATES:** Very good. What will my next question be?\n" +"**The Complete Picture**: Combining all three levels, you've now proved the fundamental chain:\n" "\n" -"**SIMPLICIO:** I bet you're going to ask me to sum the columns instead of the rows...?\n" +"§0\n" "\n" -"**SOCRATES:** You bet! :)\n" +"**Why This Matters Historically**:\n" +"- **Riemann** (1850s) defined integration but couldn't rigorously prove when it worked\n" +"- **Cauchy** earlier made errors by missing the uniformity requirement\n" +"- **Heine-Borel** (1890s-1900s) finally clarified compactness\n" +"- **Lebesgue** (1900s) built on these foundations for modern integration theory\n" "\n" -"**SIMPLICIO:** Alright, let's do that. The first column sums to $-1 + 0 + 0 + 0 + \\cdots = -1$.\n" +"**The Topological Revolution**: Before topology, mathematicians did analysis with intuition and clever tricks. Compactness gave them the 'right' framework to make rigorous arguments. This is why closed bounded intervals §1 are so special in calculus - they're exactly the compact sets in §2!\n" "\n" -"The second column sums to $1/2 + -1 + 0 + 0 + \\cdots = -1/2$.\n" +"**Real-World Impact**: Every time you compute §3 in calculus and trust that it exists, you're using today's theorem. Every continuous function on §4 is integrable because §5 is compact!\n" "\n" -"The third column sums to $1/4 + 1/2 + -1 + 0 + \\cdots = -1/4$.\n" +"**Looking Forward**: You've seen how topology (compactness) illuminates analysis (integration). This pattern repeats throughout mathematics - the 'right' abstract framework often makes concrete problems much clearer. Welcome to the power of mathematical abstraction!" +msgstr "" + +#. §0: `rewrite` +#. §1: `rewrite [hypothesis_name1, hypothesis_name2, etc]` +#: Game.Levels.L1RealAnalysisStory.L03_rw +msgid "The §0 tactic replaces the left-hand side of an equality with the right-hand side in the goal. The syntax is §1." +msgstr "" + +#. §0: `FunContAt` +#. §1: `f` +#. §2: `c` +#. §3: ``` +#. ∀ ε > 0, ∃ δ > 0, ∀ x, |x - c| < δ → |f x - f c| < ε +#. ``` +#. §4: `FunContAt f c` +#. §5: `FunLimAt` +#. §6: `x ≠ c` +#. §7: `f c` +#. §8: `L` +#. §9: `L` +#. §10: `f c` +#. §11: `f(x) = (x² - 1)/(x - 1)` +#. §12: `x = 1` +#. §13: `f(1) = 0 ≠ 2` +#. §14: `g(x) = x² - 1` +#. §15: `x = 2` +#. §16: `f(x) = x² - 1` +#. §17: `x = 2` +#. §18: `FunContAt (fun x ↦ x^2 - 1) 2` +#. §19: `ε > 0` +#. §20: `δ > 0` +#. §21: `|x - 2| < δ` +#. §22: `|f(x) - f(2)| < ε` +#. §23: `f(2) = 3` +#. §24: `f(x) - f(2) = x² - 1 - 3 = x² - 4 = (x - 2)(x + 2)` +#. §25: `|f(x) - f(2)| = |x - 2| · |x + 2|` +#. §26: `x` +#. §27: `1` +#. §28: `2` +#. §29: `1 < x < 3` +#. §30: `|x + 2| < 5` +#. §31: `δ = min(1, ε/5)` +#. §32: `|f(x) - f(2)|` +#. §33: `use min 1 (ε / 5)` +#. §34: `|x - 2| < 1` +#: Game.Levels.L20Levels.L02 +msgid "# Level 2: Continuity at a Point\n" "\n" -"Ok, I see the pattern. The $n$th column sums to $-1 / 2^{n-1}$. So the sum of all the elements in $M$ is\n" -"$-1 - 1/2 - 1/4 - 1/8 - \\cdots = -2$.\n" +"Excellent work with limits! Now we can define one of the most important concepts in analysis: **continuity**.\n" "\n" -"Uh oh. So what *is* the sum?\n" +"## The Definition\n" "\n" -"**SOCRATES:** Well that's just it! There is *no* 'the sum', because it depends on in what order you add the terms up!\n" +"**Definition (§0):** We say that §1 is **continuous at** §2 if:\n" +"§3\n" "\n" -"**Infinite summation is not commutative!**\n" +"This is written §4.\n" "\n" -"A *lot* of analysis is devoted to the study of this problem.\n" -"A sequence is called 'conditionally convergent' if it converges, but not when you add absolute values.\n" -"That is, the matrix $|M|$ would look like this:\n" -"\n" -"$\n" -"\\begin{pmatrix}\n" -"1 & 1/2 & 1/4 & 1/8 & 1/16 & \\cdots \\\\\n" -"0 & 1 & 1/2 & 1/4 & 1/8 & \\cdots \\\\\n" -"0 & 0 & 1 & 1/2 & 1/4 & \\cdots \\\\\n" -"0 & 0 & 0 & 1 & 1/2 & \\cdots \\\\\n" -"\\vdots & \\vdots & \\vdots & \\vdots & \\vdots & \\ddots\n" -"\\end{pmatrix}\n" -"$\n" +"## Continuity vs. Limits\n" "\n" -"and hopefully it's clear (just from the diagonal!) that the sum of all its elements diverges (to infinity).\n" +"Notice the subtle but crucial differences from §5:\n" "\n" -"People like Euler and Ramanujan were absolute wizards with divergent series, getting out of them all\n" -"kinds of bizarre results, like $1 + 2 + 3 + 4 + \\cdots$ '`=`' $-1/12$. As the great\n" -"Oliver Heaviside supposedly once said, 'This series is divergent, therefore we may be able to do something with it!'\n" +"1. **No §6 condition:** We care about *all* x near c, including c itself\n" +"2. **The limit is §7:** The function value at c must match the limit as x approaches c; we don't need a separate variable name §8 for the limit, since §9 *must* be §10.\n" "\n" -"**SIMPLICIO:** I like it! Let's go." -msgstr "" - -#: Game.Levels.L8Lecture -msgid "# Lecture 8: Mathematical Induction\n" +"In other words: **A function is continuous at c if its limit at c exists and equals f(c).**\n" "\n" -"**SIMPLICIO:** Hey Socrates, I've been thinking about something that's been bothering me. When we prove things in mathematics, we usually prove a specific statement. But what if I want to prove something is true for *all* natural numbers? Like, how do I prove a statement for 0, 1, 2, 3, 4, and so on... forever?\n" +"## Why This Matters\n" "\n" -"**SOCRATES:** Ah, an excellent question! You're right that we can't just check each case one by one—that would take infinitely long. Tell me, Simplicio, have you ever climbed a ladder?\n" +"The function §11 from the previous level had a limit at §12, but it's *not* continuous there (because §13 in Lean's system).\n" "\n" -"**SIMPLICIO:** Of course! What does that have to do with anything?\n" +"However, the function §14 is continuous everywhere, including at §15!\n" "\n" -"**SOCRATES:** Well, imagine an infinitely tall ladder reaching up to the sky. If I wanted to convince you that you *could* climb to any rung on this ladder, what would I need to show you?\n" +"## Your Challenge\n" "\n" -"**SIMPLICIO:** Hmm... I guess you'd need to show me that I can reach the bottom-most rung?\n" +"Prove that the function §16 is continuous at §17:\n" "\n" -"**SOCRATES:** Good start! And what else?\n" +"§18\n" "\n" -"**SIMPLICIO:** Well, if I'm standing on any particular rung, I'd need to know I can reach the next one up. So if I can always step from one rung to the next...\n" +"**Hint:** Given §19, you need to find §20 such that §21 implies\n" +"§22.\n" "\n" -"**SOCRATES:** Exactly! So if you can reach the first rung, and you can always step from rung `k` to rung `k+1`, then what can you conclude?\n" +"Note that §23 and §24.\n" "\n" -"**SIMPLICIO:** Oh! Then I can reach *any* rung I want! If I want to reach rung 100, I just start at rung 0, step to rung 1, then to rung 2, and keep going until I reach rung 100. And the same works for any number!\n" +"So §25.\n" "\n" -"**SOCRATES:** Precisely! This is the essence of **mathematical induction**. To prove something is true for all natural numbers `n`, you need exactly two things:\n" -"- A **base case**: prove it's true for `n = 0`\n" -"- An **inductive step**: prove that *if* it's true for `n = k`, *then* it's true for `n = k + 1`\n" +"If we restrict §26 to be within distance §27 of §28 (i.e., §29), then §30.\n" "\n" -"**SIMPLICIO:** Wait, but in the inductive step, aren't we assuming what we're trying to prove? Isn't that circular reasoning?\n" +"Therefore, if we choose §31, we can control §32!\n" "\n" -"**SOCRATES:** An astute observation! But no, it's not circular. We're not assuming the statement is true for all `n`. We're only assuming it's true for one particular value `k`, and using that assumption to prove that it's true for `k + 1`. We're proving an implication: \"if `P(k)` then `P(k+1)`\". Combined with the base case, this creates a chain reaction that reaches any natural number.\n" +"Try using §33 and split into cases based on whether §34." +msgstr "" + +#. §0: `a : ℕ → ℝ` +#. §1: `SeqConv a` +#: Game.Levels.L17Levels.L04 +msgid "If §0 is Monotone and bounded, then §1." +msgstr "" + +#. §0: `FunContAt f c` +#. §1: `f` +#. §2: `c` +#. §3: `FunCont` +#. §4: `f` +#. §5: `∀ x, FunContAt f x` +#. §6: `FunCont f` +#. §7: `f` +#. §8: `f(x) = x² - 1` +#. §9: `x` +#. §10: `f(x)` +#. §11: `x² - 1` +#. §12: `x` +#. §13: `FunContAt (fun t ↦ t^2 - 1) x` +#. §14: `ε > 0` +#. §15: `δ > 0` +#. §16: `|t - x| < δ` +#. §17: `|f(t) - f(x)| < ε` +#. §18: `f(t) - f(x) = (t² - 1) - (x² - 1) = t² - x² = (t - x)(t + x)` +#. §19: `|f(t) - f(x)| = |t - x| · |t + x|` +#. §20: `|t - x| < 1` +#. §21: `|t + x| < |2x| + 1` +#. §22: `δ = min(1, ε / (|2x| + 1))` +#. §23: `f(x) = x² - 1` +#. §24: `FunCont (fun x ↦ x^2 - 1)` +#. §25: `x` +#. §26: `|t + x|` +#. §27: `x` +#. §28: `5` +#. §29: `min 1 (ε / (|2 * x| + 1))` +#. §30: `δ` +#. §31: `|t - x| < 1` +#. §32: `|t + x| < |2 * x| + 1` +#: Game.Levels.L21Levels.L08 +msgid "# Level 4: Continuous Functions\n" "\n" -"**SIMPLICIO:** Hmm, I think I see. So the assumption \"it's true for `k`\" is called the inductive hypothesis?\n" +"Just as we moved from derivatives at a point to derivative functions, we can move from continuity at a point to continuity everywhere!\n" "\n" -"**SOCRATES:** Exactly! And that hypothesis is your most powerful tool. It's like having a foothold on rung `k` that you can push off from to reach rung `k + 1`.\n" +"## From Point Continuity to Global Continuity\n" "\n" -"**SIMPLICIO:** But why does this work? I mean, why should I believe this principle?\n" +"So far, §0 tells us that §1 is continuous at the specific point §2.\n" "\n" -"**SOCRATES:** Ah, a deep question! It comes from the very definition of the natural numbers themselves. How do you think the natural numbers are constructed?\n" +"But many functions (like polynomials) are continuous at *every* point.\n" "\n" -"**SIMPLICIO:** Well... I guess we start with 0. And then we have 1, which is 0 + 1. And 2 is 1 + 1. So each number is the \"successor\" of the previous one?\n" +"## The New Definition\n" "\n" -"**SOCRATES:** Beautiful! The natural numbers are defined by exactly this process:\n" -"- Zero is a natural number\n" -"- If `k` is a natural number, then `k + 1` is also a natural number\n" -"- These are the *only* natural numbers\n" +"**Definition (§3):** We say that §4 is **continuous** (everywhere) if:\n" "\n" -"Do you see how this mirrors the structure of induction?\n" +"§5\n" "\n" -"**SIMPLICIO:** Oh wow! The base case corresponds to \"zero is a natural number,\" and the inductive step corresponds to \"if `k` is a natural number, then so is `k + 1`.\" Induction is just the construction of the natural numbers turned into a proof technique!\n" +"This is written §6.\n" "\n" -"**SOCRATES:** Precisely! There are no \"gaps\" in the natural numbers—no number that can't be reached by starting at 0 and repeatedly adding 1. This is why induction works.\n" +"In other words: §7 is continuous at every point in its domain.\n" "\n" -"In fact, this is not just a philosophical observation—this is *literally* how the natural numbers are implemented in Lean! In Lean's type theory, a natural number is defined inductively as either:\n" -"- `zero : ℕ`, the base case, or\n" -"- `succ n : ℕ`, the successor of another natural number `n`\n" +"## Why Polynomials Are Continuous\n" "\n" -"Here's how this looks in the core of Lean:\n" +"Intuitively, polynomials like §8 are continuous because:\n" +"- You can draw them without lifting your pen\n" +"- Small changes in §9 produce small changes in §10\n" +"- There are no jumps, breaks, or asymptotes\n" "\n" -"`inductive Nat where`\n" -"- `| zero : Nat`\n" -"- `| succ (n : Nat) : Nat`\n" +"We've worked with continuity of §11 before. Now we'll prove it's continuous **everywhere**!\n" "\n" -"You simply declare the existence of a natural number called `zero`, and then we declare that, given any natural number `n`, there's another one called `succ n`. (The word `succ` is here just a name for this constructor; we could have called it `Alice` instead. The important thing is that we're giving a way to construct a new natural number from a previously existing one.)\n" +"## The Strategy\n" "\n" -"So the number 3, for instance, is literally represented as `succ (succ (succ zero))`. The principle of induction doesn't just *resemble* this construction, it directly exploits it! When you prove something by induction in Lean, you're working with the actual computational structure of how natural numbers exist in the system.\n" +"For any point §12, we need to show §13.\n" "\n" -"**SIMPLICIO:** That's amazing! So induction isn't just a proof technique—it's baked into the very fabric of how Lean understands numbers?\n" +"This means: given §14, find §15 such that §16 implies §17.\n" "\n" -"**SOCRATES:** Exactly. The principle of mathematical induction is a theorem in many mathematical frameworks, but in type theory, it's a fundamental consequence of how the natural numbers are defined.\n" +"The algebra follows a familiar pattern:\n" "\n" -"**SIMPLICIO:** Okay, I'm convinced this is a legitimate proof technique. Can you give me an example?\n" +"§18\n" "\n" -"**SOCRATES:** Certainly." -msgstr "" - -#: Game.Levels.L21Levels.L06 -msgid "# Excellent Work!\n" +"So §19.\n" "\n" -"You've just computed your first derivative using the formal limit definition! This is a foundational skill that connects the abstract world of limits to the concrete world of rates of change.\n" +"If we restrict §20, then §21.\n" "\n" -"## What You Accomplished\n" +"Taking §22 will work!\n" "\n" -"You proved that the derivative of `f(x) = x² - 1` at `x = 2` is exactly `4`. This means:\n" -"- The **instantaneous rate of change** of `f` at `x = 2` is `4`\n" -"- The **slope of the tangent line** to the graph at `(2, 3)` is `4`\n" -"- If you zoom in very close to the point `(2, 3)`, the function looks like the line `y = 4x - 5`\n" +"## Your Challenge\n" "\n" -"## The Power of Algebraic Simplification\n" +"Prove that §23 is continuous everywhere:\n" "\n" -"Your proof showcased a key technique: **algebraic manipulation before taking limits**.\n" +"§24\n" "\n" -"Instead of wrestling with the indeterminate form `0/0`, you:\n" -"1. **Expanded:** `(2 + h)² = 4 + 4h + h²`\n" -"2. **Simplified:** `(4h + h²)/h = h(4 + h)/h = 4 + h`\n" -"3. **Applied the limit:** `lim[h→0] (4 + h) = 4`\n" +"**Hint:** After introducing §25, you need to bound §26 in terms of §27 (not a constant like §28).\n" "\n" -"This \"simplify first, then limit\" approach is essential for derivative computations!\n" +"Use §29 as your §30. The key is showing that when §31, we have §32." +msgstr "" + +#: Game.Levels.L7Levels.L02_SeqOfAbs +msgid "Sequences of Absolute Values" +msgstr "" + +#. §0: `h` +#. §1: `change ∀ ε₁ > 0, ∃ N₁ : ℕ, ∀ n ≥ N₁, |a n - L| < ε₁ at h` +#: Game.Levels.L5Levels.L01_DoubleSeqConv +msgid "Also try unfolding the definition in §0: §1" +msgstr "" + +#: Game.Levels.L18PsetIntro +msgid "# Problem Set 18" +msgstr "" + +#. §0: ``` +#. ∀ n < N, |a n| ≤ ∑ k ∈ range N, |a k| +#. ``` +#. §1: `N` +#. §2: `sum_range_succ` +#. §3: `sum_nonneg` +#. §4: `n < N` +#. §5: `n = N` +#. §6: `TermLeSum` +#. §7: `Bdd_of_ConvNonzero` +#: Game.Levels.L9Levels.L04_FiniteSums +msgid "# 🎉 Excellent Work!\n" "\n" -"## The Beautiful Result: δ = ε\n" +"You've just proven a fundamental result about finite sums! This theorem might seem simple, but it's a powerful building block that appears throughout analysis.\n" "\n" -"Notice how clean the final step was: to prove `|h| < ε`, you simply chose `δ = ε`. This perfect correspondence happens because the simplified difference quotient `4 + h` has slope exactly `1` near the limit point.\n" +"## What You Accomplished\n" "\n" -"This won't always be so simple, but it's a beautiful example of how algebra can make limit proofs elegant.\n" +"You successfully proved that **every term is bounded by the total sum**:\n" +"§0\n" "\n" -"## Connection to Calculus\n" +"### Key Techniques You Mastered:\n" "\n" -"In traditional calculus, you might have computed this as:\n" -"- `d/dx[x²] = 2x`, so at `x = 2` we get `2(2) = 4`\n" -"- The constant `-1` has derivative `0`\n" +"1. **Strategic induction** - You learned to use induction on §1 *before* introducing the universal quantifier, which made the proof structure much cleaner\n" "\n" -"You've now proven this rigorously from first principles! Every time you use the power rule, you're implicitly using the kind of limit argument you just mastered.\n" +"2. **Working with finite sums** - You used §2 to peel off terms and §3 to establish nonnegativity\n" "\n" -"## Looking Ahead\n" +"3. **Case analysis** - You split the proof into two cases (§4 vs §5) and handled each appropriately\n" "\n" -"In the next level, we'll generalize this computation to find the derivative at **every** point, not just `x = 2`. You'll discover the famous **power rule** emerging naturally from limit definitions!" -msgstr "" - -#: Game.Levels.L18Levels.L01 -msgid "`(a : ℕ → ℝ) := SeriesConv (fun n ↦ |a n|)`\n" +"4. **Combining results** - You cleverly used the inductive hypothesis for earlier terms and nonnegativity for the final term\n" "\n" -"We say that a sequence `a : ℕ → ℝ` converges absolutely if `∑ |a n|` converges." -msgstr "" - -#: Game.Levels.L20Levels.L04 -msgid "Sequential Criterion for Limits (Forward Direction)" -msgstr "" - -#: Game.Levels.L3Pset.L3Pset1 -msgid "# Problem 1\n" +"## Why This Matters\n" "\n" -"The \"full\" Archimedean Property is this:\n" -"Take two positive real numbers `x` and `y`. No matter\n" -"how large `y` may be, and how small `x` may be,\n" -"if we add `x` to itself enough times (that is, multiply it by some natural number), we can always get that to exceed `y`." -msgstr "" - -#: Game.Levels.L15Levels.L01_check -msgid "If a sequence `a : ℕ → ℚ` is Cauchy, then it converges (that is, `SeqLim` holds)\n" -"to the real number defined in `Real_of_CauSeq`." -msgstr "" - -#: Game.Levels.L3Pset.L3Pset4 -msgid "Usage: given hypothesis `h : 0 ≤ X`, you can prove: `have : |X| = X := by apply abs_of_nonneg h`" -msgstr "" - -#: Game.Levels.L6Levels.L06_Squeeze -msgid "If `a c : ℕ → ℝ`, with `a` and `c` both converging to `L`,\n" -"and `b` is another sequence, squeezed between `a` and `c`, then `b` also converges to `L`." -msgstr "" - -#: Game.Levels.L13Pset.L13Pset1 -msgid "# Problem 1:\n" +"This result is essential for the next level! You'll use §6 to prove that **convergent sequences are bounded**. Here's the connection:\n" "\n" -"Prove `AntitoneSubseq_of_UnBddPeaks`\n" +"- Every convergent sequence is eventually close to its limit\n" +"- But what about the finitely many terms *before* it gets close?\n" +"- That's where your theorem comes in! You can bound those initial terms by their finite sum\n" +"- Combine this with the eventual bound, and you get a global bound for the entire sequence\n" "\n" -"## New theorem: `Antitone_of_succ`" -msgstr "" - -#: Game.Levels.L3Levels.L02_OneOverN -msgid "Start by converting to the definition of sequential convergence using `change`." -msgstr "" - -#: Game.Levels.L15Pset.L15Pset1 -msgid "# Problem 1:\n" +"## Looking Ahead\n" "\n" -"Prove that $0.999... = 1.0000$. Better yet, let's do it in binary.\n" -"That is, you have two **rational** (Cauchy) sequences, `a n = 1 - 1 / 2^n` and `b n = 1`.\n" -"The two sequences are equivalent if `a n - b n` goes to zero, that is, if for all `ε > 0, ∃ N, ∀ n ≥ N, |a n - b n| < ε`.\n" +"In the next level, you'll prove §7: convergent sequences with nonzero limits are bounded. This is a cornerstone result in analysis that tells us convergent sequences can't escape to infinity.\n" "\n" -"Hint: In Lecture 8, we proved a theorem (now) called `IdLeTwoPow`..." -msgstr "" - -#: Game.Levels.L18Levels.L02 -msgid "Given `a : ℕ → ℝ`, if `a (2 n) → L` and `a (2n+1) → L`, then `a → L`." -msgstr "" - -#: Game.Levels.L21Levels.L05 -msgid "If for every sequence `(xₙ)` converging to `c` with `xₙ ≠ c`, the sequence `f(xₙ)` converges to `L`, then the function `f` has limit `L` at point `c`." +"Ready to see your theorem in action? Let's move on!" msgstr "" -#: Game.Levels.L21Levels.L08 -msgid "`∀ x, FunContAt f x`\n" +#. §0: `⌈·⌉` +#. §1: `bound` +#. §2: `push_cast` +#. §3: `⌈1 / ε⌉₊ + 1` +#. §4: `ℕ` +#. §5: `ℝ` +#. §6: `push_cast` +#: Game.Levels.L3Levels.L01_ArchProp +msgid "Let's compare now to the purely natural language proof:\n" "\n" -"The function `f` is continuous on all of `ℝ`." -msgstr "" - -#: Game.Levels.L19Levels.L03 -msgid "If `Series a` converges absolutely, then any rearrangement of `a` also converges, and to the same sum." -msgstr "" - -#: Game.Levels.L1RealAnalysisStory.L00_the_problem -msgid "Write `apply h` since the hypothesis `h` is what we want to prove." -msgstr "" - -#: Game.Levels.L11Levels.L02_IsCauchyOfSum -msgid "# Level 2: Sums of Cauchy Sequences\n" +"## Natural Language Proof of the Archimedean Property\n" "\n" -"Now that we know convergent sequences are Cauchy, let's explore how Cauchy sequences behave under arithmetic operations. Just like we proved that sums of convergent sequences converge, we'll show that sums of Cauchy sequences are Cauchy.\n" +"**Theorem**: For any positive real number ε > 0, there exists a natural number N such that 1 / ε < N.\n" "\n" -"This theorem is important because it shows that the Cauchy property is preserved by addition—a crucial fact we'll need when we eventually define the real numbers!\n" +"**Proof**:\n" +"Let ε > 0 be given. We need to find a natural number N such that 1 / ε < N.\n" "\n" -"## The Setup\n" +"Use the value N = ⌈1 / ε⌉₊ + 1, where ⌈·⌉₊ denotes the natural number ceiling function.\n" "\n" -"Given:\n" -"- `a : ℕ → ℝ` is Cauchy\n" -"- `b : ℕ → ℝ` is Cauchy\n" +"Since ε > 0, we have 1 / ε > 0. By the definition of the natural number ceiling function, we know that:\n" "\n" -"Prove: `a + b` is Cauchy\n" +"1 / ε ≤ ⌈1 / ε⌉₊\n" "\n" -"## Strategy\n" +"Now, since ⌈1 / ε⌉₊ is a natural number and N = ⌈1 / ε⌉₊ + 1, we have:\n" "\n" -"This proof follows a familiar pattern from the sum of limits theorem:\n" +"⌈1 / ε⌉₊ < ⌈1 / ε⌉₊ + 1 = N\n" "\n" -"1. **Split epsilon**: Apply the Cauchy property to both `a` and `b` using `ε/2`\n" -"2. **Take the maximum N**: Use `N₁ + N₂` to ensure both Cauchy conditions hold\n" -"3. **Change the goal**: Express `|(a + b)ₘ - (a + b)ₙ|` as `|(aₘ - aₙ) + (bₘ - bₙ)|`\n" -"4. **Triangle inequality**: Split the sum into two pieces\n" -"5. **Combine estimates**: Each piece is less than `ε / 2`, so the total is less than `ε`\n" +"Combining these inequalities, we get that:\n" "\n" -"## Key Insight\n" +"1 / ε ≤ ⌈1 / ε⌉₊ < N\n" "\n" -"The beauty of the Cauchy property is that we don't need to know *where* the sequences converge—we only need to know that their terms get close to *each other*. This self-referential definition makes the proof very similar to the sum of limits, but without ever mentioning a limit!\n" +"Therefore, 1 / ε < N, which completes the proof. □\n" "\n" -"Let's prove it!" +"**Significance**: The Archimedean Property is fundamental to analysis because it ensures that the real numbers have no \"infinite\" or \"infinitesimal\" elements. It guarantees that we can always find natural numbers large enough to dominate any given positive real number when we take their reciprocals. This property is essential for many limit processes and is equivalent to the completeness of the real numbers in certain formulations of real analysis.\n" +"\n" +"## Review of Common Pitfalls\n" +"\n" +"- **Don't use the regular ceiling function §0** - it returns integers, not natural numbers!\n" +"- **Watch out for casting issues** - if §1 isn't working, try §2 first\n" +"- **The addition §3 happens in §4**, then gets cast to §5 - this is why we need §6\n" +"\n" +"**Historical Note**: While often attributed to Archimedes (c. 287-212 BCE), this property was likely known to Eudoxus (c. 408-355 BCE) and appears in Euclid's *Elements*. Archimedes used a version of this principle in his method of exhaustion, particularly in calculating areas and volumes by approximating them with polygons of increasing numbers of sides." msgstr "" -#: Game.Levels.L1RealAnalysisStory.L04_ring_nf -msgid "# Algebraic manipulations\n" +#. §0: `have` +#. §1: `h : X = Y` +#. §2: `X` +#. §3: `rewrite [h]` +#. §4: `X` +#. §5: `Y` +#. §6: `h2` +#. §7: `X` +#. §8: `h2` +#. §9: `Y` +#. §10: `rewrite [h] at h2` +#. §11: `rewrite [h]` +#. §12: `at` +#. §13: `ring_nf at h2` +#. §14: `h2` +#: Game.Levels.L1Pset.L1Pset3 +msgid "# Problem 3\n" "\n" -"Now let's learn about algebraic simplification. Suppose you need to prove that $(x + y)^3 = x^3 + 3x^2y + 3xy^2 + y^3$.\n" +"You've just learned to add any necessary\n" +"auxiliary\n" +"facts to the list of hypotheses via the\n" +"§0 tactic.\n" +"In this problem,\n" +"you might find the following new idea useful.\n" "\n" -"This is true by the basic laws of algebra - expanding the left side using the distributive law, commutativity, associativity, etc. But doing this by hand would be extremely tedious.\n" +"You already know that if you\n" +"have a hypothesis §1, and the Goal\n" +"contains §2, then if you §3,\n" +"then any instances of §4 in the goal\n" +"get replaced by §5.\n" +"But what if you have another hypothesis §6,\n" +"and you want to replace §7's in §8 by §9s, what should you do then?\n" +"Elementary, my dear Watson!\n" +"You simply type:\n" "\n" -"Fortunately, Lean has a powerful tactic called `ring_nf` (\"ring normal form\") that can automatically perform algebraic manipulations like:\n" -"- Expanding products\n" -"- Collecting like terms\n" -"- Rearranging using commutativity and associativity\n" -"- Applying the distributive law\n" +"§10.\n" "\n" -"When you have an algebraic identity involving addition, subtraction, and multiplication, `ring_nf` can often prove it automatically.\n" +"So the syntax is §11 as before, then\n" +"the word §12, and finally the name of the\n" +"hypothesis where you want the rewriting to happen.\n" +"Similarly, you can say §13,\n" +"and any algebra in hypothesis §14 will be put into normal form.\n" "\n" -"Try it out on this classic binomial expansion!" +"Now you should be able to solve this problem!" msgstr "" -#: Game.Levels.L8Levels.L03_Induction' -msgid "For all `n`, `n < 2 ^ n`." +#: Game.Levels.L22Levels.L02 +msgid "Uniform Convergence" msgstr "" -#: Game.Levels.L7Levels.L02_SeqOfAbs -msgid "Sequences of Absolute Values" +#: Game.Levels.L1RealAnalysisStory +msgid "Lecture 1: The Story of Real Analysis" msgstr "" -#: Game.Levels.L18PsetIntro -msgid "# Problem Set 18" +#. §0: `ProdLim` +#: Game.Levels.L10Pset.L10Pset3 +msgid "# Problem 2:\n" +"\n" +"Finish the proof of §0." msgstr "" -#: Game.Levels.L18Levels.L01 -msgid "If `n ≤ m`, then `Series a m - Series a n = ∑ k ∈ Ico n m, a k`." +#: Game.Levels.L2Pset.L2Pset1 +#: Game.Levels.L2Pset.L2Pset2 +msgid "Find the correct constant." msgstr "" -#: Game.Levels.L1RealAnalysisStory.L03_rw -msgid "Type `rewrite [Bob]` to replace `x` with `2` in the goal. Then what?" +#. §0: `a : ℕ → ℝ` +#. §1: `L` +#. §2: `b : ℕ → ℝ` +#. §3: `b n = 1 / a n` +#. §4: `n` +#. §5: `b` +#. §6: `1 / L` +#. §7: `L ≠ 0` +#: Game.Levels.L7Levels.L03_SeqInvLim +msgid "If §0 converges to §1, and §2 is its inverse, §3 for all §4, then §5 converges to §6, provided §7." msgstr "" -#: Game.Levels.L19Levels.L02 -msgid "A function `f : X → Y` called `Surjective` if: for all `y : Y`, `∃ x : X` so that `f x = y`." +#: Game.Levels.L12Levels.L00_SubseqIterate +msgid "Iterated Subsequence" msgstr "" -#: Game.Levels.L17Levels.L02 -msgid "Excellent work! You've rigorously proven that the Leibniz series converges to 1.\n" +#. §0: `σ : ℕ → ℕ` +#: Game.Levels.L8Pset.L8Pset4 +msgid "If a sequence §0 is strictly increasing, then it grows at least linearly." +msgstr "" + +#. §0: `CoherenceOfReals` +#. §1: `CoherenceOfReals` +#: Game.Levels.L18Pset.L04 +msgid "# Level 4: §0\n" +"\n" +"Prove §1:" +msgstr "" + +#. §0: `a : ℕ → ℝ` +#. §1: `Antitone` +#. §2: `∀ n, 0 ≤ a n` +#. §3: `n ↦ ∑ k ∈ range (2n+1), (-1)^k * a k` +#. §4: `0` +#: Game.Levels.L18Levels.L02 +msgid "If §0 is §1 and §2, then the odd alternating series §3 is bounded below by §4." +msgstr "" + +#. §0: `huv` +#. §1: `specialize` +#. §2: `u` +#. §3: `v` +#. §4: `x` +#. §5: `y` +#. §6: `have hxy : (x + y) ^ 2 = (x ^ 2 + y ^ 2) + 2 * (x * y) := by ring_nf` +#: Game.Levels.L1Pset.L1Pset2 +msgid "Did you end up using §0?\n" +"And then §1ing it with §2 and §3 replaced, respectively, by §4 and §5?\n" +"Or did you think of going via the more direct route:\n" +"§6?" +msgstr "" + +#: Game.Levels.L9Lecture +msgid "Lecture 9: Algebraic Limit Theorem, Part IV" +msgstr "" + +#. §0: `(f : ℝ → ℝ) (a b : ℝ) := ∃ I, HasIntegral f a b I` +#. §1: `f : ℝ → ℝ` +#. §2: `IntegrableOn` +#. §3: `a` +#. §4: `b` +#. §5: `I` +#. §6: $\\int_a^b f(x)dx$ +#. §7: `I` +#: Game.Levels.L22Levels.L03 +msgid "§0\n" +"\n" +"A function §1 is §2 the interval §3 to §4 if there exists some §5 so that the integral §6 converges and equals §7." +msgstr "" + +#. §0: `change` +#. §1: `X` +#. §2: `Y` +#. §3: `X := Y` +#. §4: `X` +#. §5: `change Y` +#. §6: `Y` +#. §7: `h : X` +#. §8: `change Y at h` +#. §9: `h` +#. §10: `h : Y` +#: Game.Levels.L2NewtonsCalculationOfPi.L01_SeqConvDef +msgid "The §0 tactic changes a goal to something definitionally equal to it. If the definition of §1 is §2, that is, §3, and the Goal is §4, you can write §5 and the Goal will change to §6. You can also\n" +"do this at a hypothesis; if you have a hypothesis §7, you can write §8, and §9 will change to §10." +msgstr "" + +#. §0: `∑ k, 1/(k+2)² = 1/4 + 1/9 + 1/16 + ...` +#. §1: `IsCauchy_of_MonotoneBdd` +#. §2: `Conv_of_IsCauchy` +#. §3: `1/(k+2)² ≤ 1/((k+1)(k+2))` +#. §4: `SeriesOrderThm` +#. §5: `1 - 1/(n+1) < 1` +#. §6: `1/(k+2)² > 0` +#. §7: $\\sum_{k=1}^\\infty 1/k^2 = \\pi^2/6 \\approx 1.6449...$ +#. §8: `∑ 1/k^(2n)` +#. §9: `n` +#. §10: `π^(2n)` +#. §11: `ζ(s) = ∑_{k=1}^∞ 1/k^s` +#. §12: `ζ(2) = π²/6` +#. §13: `ζ(4) = π⁴/90` +#. §14: `ζ(6) = π⁶/945` +#. §15: `ζ(3) = ∑ 1/k³` +#. §16: `π` +#. §17: `ζ(3)` +#. §18: `π` +#: Game.Levels.L17Levels.L04 +msgid "Magnificent! You've proven that the Basel series converges—a major milestone in the history of mathematics!\n" "\n" "## What You've Accomplished\n" "\n" -"**Theorem (LeibnizSeries):** The series `∑ k, 1/((k+1)(k+2))` converges.\n" +"**Theorem:** The series §0 converges.\n" "\n" -"More precisely, you've shown that `SeriesConv a` holds, meaning the partial sums converge to the limit `L = 1`.\n" +"You proved this using the **Monotone Bounded Convergence Theorem**, which you first established by connecting two powerful results:\n" +"- §1: monotone bounded sequences are Cauchy\n" +"- §2: by completeness of ℝ, Cauchy sequences converge\n" "\n" -"## The Proof Structure\n" +"## The Proof Strategy\n" "\n" -"Your proof had three main ingredients:\n" +"Your proof had three elegant components:\n" "\n" -"1. **The explicit formula** from Level 1: `∑ k ∈ range n, a k = 1 - 1/(n+1)`\n" +"1. **Comparison with Leibniz:** You showed §3, so by §4, the Basel partial sums are bounded by the Leibniz partial sums, which equal §5.\n" "\n" -"2. **The Archimedean Property:** Given `ε > 0`, there exists `N` with `1/N < ε`\n" +"2. **Boundedness:** The Basel series has partial sums bounded above by 1.\n" "\n" -"3. **Inequality chaining:** For `n ≥ N`:\n" -" `1/(n+1) ≤ 1/n ≤ 1/N < ε`\n" +"3. **Monotonicity:** Since each term §6, the partial sums form a monotone increasing sequence.\n" "\n" -"The combination of these three ingredients gave you the ε-N proof that the partial sums approach 1!\n" +"Monotone + Bounded = Convergent! This is one of the fundamental patterns in real analysis.\n" "\n" -"## Understanding the Convergence\n" +"## What We Haven't Shown\n" "\n" -"The series converges quite quickly. After `n` terms, the partial sum differs from the limit by only `1/(n+1)`:\n" +"Notice that we've proven convergence but **not** computed the exact value! We know the series converges to *some* real number less than 1, but we don't know what it is.\n" "\n" -"- After 10 terms: error ≈ 0.091\n" -"- After 100 terms: error ≈ 0.0099\n" -"- After 1000 terms: error ≈ 0.001\n" +"Computing the exact value is much harder. Euler's brilliant solution in 1734 showed:\n" +"§7\n" "\n" -"This `O(1/n)` convergence rate is typical for telescoping series.\n" +"See the homework problems for more details!\n" "\n" -"## The Role of the Archimedean Property\n" +"## The Broader Story: Riemann Zeta Function\n" "\n" -"The Archimedean Property was crucial! It guaranteed that `1/N` can be made smaller than any positive `ε`, no matter how tiny. This is what allowed us to control the tail `1/(n+1)`.\n" +"Euler went on to evaluate §8 for all positive integers §9, showing each equals a rational multiple of §10. These are now known as special values of the **Riemann zeta function**:\n" +"§11\n" "\n" -"Without completeness and the Archimedean property, we couldn't have this guarantee. In fact, this property fails in non-Archimedean ordered fields!\n" +"So §12, §13, §14, etc.\n" "\n" -"## From Formula to Convergence\n" +"But what about odd values? Is §15 related to §16, or any other known constant? This question is still open today! Only in 1978, did Roger Apéry manage to prove that §17 is **irrational**! We do not have a **right** to mathematical knowledge; any time our ignorance is momentarily lifted, it is a cause for celebration.\n" "\n" -"This level demonstrated a powerful two-step strategy:\n" -"1. **First**, find an explicit formula for partial sums (often via telescoping, induction, or other techniques)\n" -"2. **Then**, use the formula to prove convergence rigorously\n" +"## The Power of Comparison\n" "\n" -"This approach is cleaner than trying to prove convergence directly without knowing what the limit is!\n" +"Your proof demonstrated the **comparison test** in action: to prove a series converges, find a known convergent series that dominates it term-by-term. This is one of the most practical convergence tests in analysis.\n" "\n" -"## Historical Context\n" +"## Historical Significance\n" "\n" -"Leibniz studied this and similar series in the 1670s as part of his groundbreaking work on infinite series. He didn't have our modern ε-N definition (that came 150 years later with Cauchy), but his intuition about these sums was remarkably accurate.\n" +"The Basel Problem launched Euler's career and revolutionized the study of infinite series. It showed that series could encode deep connections between discrete sums and continuous quantities like §18.\n" "\n" "---\n" "\n" -"**Next level:** We'll prove a comparison theorem that lets us bound one series by another, setting up powerful convergence tests!" +"**Congratulations!** You've completed Lecture 17 and proven some of the most beautiful classical results about infinite series. You've mastered telescoping sums, the comparison test, and the monotone bounded convergence theorem—powerful tools you'll use throughout analysis.\n" +"\n" +"**Next lecture:** We'll explore more sophisticated convergence tests and dive deeper into the theory of series!" msgstr "" -#: Game.Levels.L22Levels.L02 -msgid "Uniform Convergence" +#. §0: `ε` +#. §1: `δ` +#: Game +msgid "*Real Analysis, The Game*\n" +"\n" +"## About this Course\n" +"\n" +"This course follows the historical crises that forced mathematicians to rebuild\n" +"mathematics from the ground up in the 19th century. You'll learn why concepts\n" +"like §0-§1 definitions became necessary and how to use them to do advanced calculus.\n" +"\n" +"## Credits\n" +"\n" +"* **Course Design:** By Alex Kontorovich alex.kontorovich@rutgers.edu\n" +"* **Interactive Implementation:** Lean 4 Game Engine\n" +"* **Mathematical Content:** Following Rudin, Stein-Shakarchi, Abbot, etc.\n" +"* **Many thanks to:** Jon Eugster, Heather Macbeth, Michael Stoll, and the students of 311H for a lot of technical support, encouragement, and many great suggestions for improvement!" msgstr "" -#: Game.Levels.L1RealAnalysisStory -msgid "Lecture 1: The Story of Real Analysis" +#. §0: `AntitoneSeriesOdd` +#. §1: `AntitoneSeriesOdd` +#: Game.Levels.L18Pset.L07 +msgid "# Level 7: §0\n" +"\n" +"Prove §1:" msgstr "" -#: Game.Levels.L2Pset.L2Pset1 -#: Game.Levels.L2Pset.L2Pset2 -msgid "Find the correct constant." +#. §0: `field_simp` +#: Game.Levels.L3Levels.L02_OneOverN +msgid "Clear denominators in the goal: §0" msgstr "" -#: Game.Levels.L12Levels.L00_SubseqIterate -msgid "Iterated Subsequence" +#. §0: `have Npos : (0 : ℝ) < N := by linarith [f3, eps_inv_lt_N]` +#: Game.Levels.L3Levels.L02_OneOverN +msgid "Since 1 / ε < N, we get N > 0: §0. Again we need to be specific about the casting." msgstr "" -#: Game.Levels.L1RealAnalysisStory.L03_rw -msgid "Great! You've learned the `rewrite` tactic.\n" -"\n" -"Notice what happened: after you typed `rewrite [Bob]`, the goal changed from `x + y = 2 + y` to `2 + y = 2 + y`. Then you needed to type `rfl` to finish the proof, since both sides were now identical.\n" -"\n" -"So far you've learned:\n" -"- `apply hypothesis_name` when a hypothesis matches your goal\n" -"- `rfl` when you need to prove something equals itself\n" -"- `rewrite [hypothesis_name]` when you want to use an equality to rewrite your goal\n" -"\n" -"The `rewrite` tactic is incredibly powerful and you'll use it constantly in real analysis!" -msgstr "" - -#: Game.Levels.L24Levels.L03 -msgid "# You've Just Proved ℝ is Complete!\n" -"\n" -"Congratulations! You've just established one of the most fundamental properties of the real numbers: the **Least Upper Bound Property**. This is\n" -"another way to say that `ℝ` is \"complete\" - it has no gaps.\n" +#. §0: `a : ℕ → X` +#. §1: `X` +#. §2: `ℚ` +#. §3: `ℝ` +#. §4: `Monotone` +#. §5: `ε` +#. §6: `k * ε` +#. §7: `k` +#: Game.Levels.L12Levels.L01_MonotoneBdd +msgid "If a sequence §0 (where §1 could be §2 or §3) is §4 and grows along some subsequences by §5, then it eventually grows by §6 for any §7." +msgstr "" + +#. §0: `specialize h1 0` +#. §1: `h1` +#. §2: `h1 : g (0 + 1) = g (0) + 3` +#. §3: `h1` +#. §4: `g (1)` +#. §5: `g (2)` +#. §6: `have` +#. §7: `specialize` +#. §8: `have h3 : g (0 + 1) = g (0) + 3 := by apply h1 0` +#. §9: `h1` +#. §10: `h3` +#. §11: `g (0 + 1) = g (0) + 3` +#. §12: `h1` +#. §13: `x` +#. §14: `g (x + 1) = g (x) + 3` +#. §15: `h1` +#. §16: `x` +#. §17: `x` +#. §18: `g (x + 1) = g (x) + 3` +#. §19: `0` +#. §20: `h1` +#. §21: `specialize` +#. §22: `have` +#: Game.Levels.L1Pset.L1Pset4 +msgid "# Problem 4\n" "\n" -"**What Made This Proof Special**:\n" -"- **Dependent Types Power**: Your proof showcased Lean's dependent type system at its best. The type `ℕ → {p : ℝ × ℝ // ...}` didn't just give you pairs of reals - it gave you pairs *with built-in proofs* that they satisfy all your constraints, and depend on the `n : ℕ`.\n" -"- **Constructive Algorithm**: Your bisection method doesn't just prove a supremum exists - it gives you an algorithm to compute it to arbitrary precision!\n" -"- **Induction on Steroids**: You weren't just proving a property for all `n` - you were constructing a sequence where each element depends on satisfying complex constraints involving the previous ones.\n" +"This problem looks very similar to the previous one, but without a few hints, it\n" +"may cause great difficulty. The issue is that, last time, you likely called §0, and turned §1 into:\n" "\n" -"**Why This Property is Profound**:\n" -"- **`ℚ` Fails Here**: The rationals are missing \"limit points\" like √2. Your proof shows ℝ has no such gaps.\n" -"- **Topology Connection**: Completeness (LUB property) is what makes compact sets in ℝ so well-behaved.\n" -"- **Analysis Foundation**: Virtually every major theorem in real analysis depends on this completeness property.\n" +"§2\n" "\n" -"**The Nested Interval Magic**: Your proof created intervals `[aₙ, bₙ]` with three beautiful properties:\n" -"1. Each `aₙ ∈ S` (reachable from below)\n" -"2. Each `bₙ` is an upper bound (unreachable from `S`)\n" -"3. `bₙ - aₙ → 0` (they squeeze together)\n" +"If you do that now, the original §3 will be *gone*, and you won't have a way of accessing it *again* to bootstrap from §4 to §5. So what should you do?\n" "\n" -"The limit of this squeeze is exactly the supremum!\n" +"Observe that §6 can perform the same\n" +"role as §7 (and much more)! Try starting your solution with:\n" "\n" -"**What's Coming**: Armed with the LUB property, you're now ready for the hard part of Heine-Borel. In Level 4, you'll prove that closed intervals `[a,b]` are compact. This will use your LUB property in a sophisticated way to show that any open cover can be reduced to a finite subcover.\n" +"§8\n" "\n" -"**Historical Note**: This property was one of the last pieces needed to make calculus rigorous. Weierstrass, Dedekind, and Cantor all worked on different ways to construct ℝ with this completeness property in the 1870s.\n" +"This will not affect the original statement\n" +"of §9, but will instead add a *new* hypothesis, §10, which amounts to the\n" +"desired fact that §11.\n" +"Notice what's happening in the proof: §12 says: for all §13, §14.\n" +"So §15 is really a *function* whose input\n" +"is a real number §16, and whose output is a\n" +"*proof* of the fact that, for this value of §17, §18 holds. So when\n" +"we feed §19 into §20, it has the same effect\n" +"as it did when we §21d, thus giving a proof of\n" +" exactly what was claimed in the §22 statement.\n" "\n" -"You've just proved one of the crown jewels of real analysis! 👑" -msgstr "" - -#: Game.Levels.L9Lecture -msgid "Lecture 9: Algebraic Limit Theorem, Part IV" +"Now you should be able to solve this problem." msgstr "" -#: Game.Levels.L11Levels.L03_IsBddOfCauchy -msgid "# Outstanding! You've proven that Cauchy sequences are bounded!\n" +#. §0: `a : ℕ → ℝ` +#. §1: `a : ℕ → ℚ` +#. §2: `X` +#. §3: `X` +#. §4: `x ≤ y` +#. §5: `|x|` +#. §6: `X` +#. §7: `ε` +#. §8: `choose` +#. §9: `a : ℕ → X` +#. §10: `M` +#. §11: `a` +#. §12: `IterateGap` +#. §13: `Monotone` +#. §14: `a : ℕ → X` +#. §15: `a n ≤ a m` +#. §16: `n ≤ m` +#. §17: `Monotone_of_succ` +#. §18: `a m ≤ a (m+1)` +#. §19: `m` +#. §20: `a` +#. §21: `Monotone` +#. §22: `push_neg` +#. §23: `¬∀` +#. §24: `∃¬` +#. §25: `¬∃` +#. §26: `∀¬` +#. §27: `IterateGap` +#. §28: `ε` +#. §29: `τ` +#. §30: `σ` +#. §31: `σ^[k] 0` +#. §32: `k * ε` +#. §33: `theorem IterateGap (a : ℕ → X) (ha : Monotone a) (ε : X) +#. (εpos : ε > 0) +#. (τ : ℕ → ℕ) (hτ : ∀ n, τ n ≥ n) +#. (σ : ℕ → ℕ) (hσ : ∀ n, σ n ≥ τ n) +#. (hgap : ∀ n, ε ≤ |a (σ n) - a (τ n)|) +#. : ∀ (k : ℕ), k * ε ≤ a (σ^[k] 0) - a 0 +#. ` +#: Game.Levels.L12Levels.L01_MonotoneBdd +msgid "# Level 3: Monotone and Bounded Implies Cauchy\n" "\n" -"This was a challenging proof involving case analysis, finite sums, and careful bookkeeping—but you did it! You've shown that the self-referential Cauchy property is powerful enough to guarantee boundedness.\n" +"Now we tackle one of the fundamental theorems of real analysis: every bounded monotone sequence is Cauchy. This result provides a powerful convergence criterion that doesn't require knowing the limit beforehand.\n" "\n" -"## What you've accomplished\n" +"## The Intuitive Picture\n" "\n" -"You've now proven that Cauchy sequences share two key properties with convergent sequences:\n" -"1. **They're bounded** (this level)\n" -"2. **They're closed under addition** (previous level)\n" +"Why should this be true? If a sequence is monotone (that is, non-decreasing) and bounded above, then it can't \"escape to infinity\" - there's a ceiling it can't break through. But it also can't have persistent gaps, because each gap would push it a bit higher, and eventually these accumulated jumps would break through the ceiling. So the sequence must \"settle down\" and become Cauchy.\n" "\n" -"And you did all this **without ever mentioning where they converge**!\n" +"Making this intuition rigorous requires the orbit technique you just mastered.\n" "\n" -"## Why this matters\n" +"## A Question of Generality\n" "\n" -"This theorem is absolutely crucial for the theory of real numbers:\n" +"Before diving in, let's address an important design choice. What type should our sequence have? We could work with §0 (real sequences), but we're building up to constructing the real numbers, so we shouldn't presuppose their existence. We could use §1 (rational sequences), but then we'd need to reprove everything for real sequences later.\n" "\n" -"- In the rationals `ℚ`, there are Cauchy sequences that don't converge (like the decimal approximations to `√2`)\n" -"- But they're still *bounded*, which means they're not escaping to infinity\n" -"- This boundedness will be essential when we prove the **Bolzano-Weierstrauss theorem**: every bounded sequence has a convergent subsequence\n" -"- Eventually, we'll use these facts to show that in `ℝ` (but not in `ℚ`), every Cauchy sequence *does* converge—this is called **completeness**\n" +"The elegant solution: work with an abstract type §2 that has just the properties we need. We'll assume §3 has:\n" +"- A linear order (so we can say §4)\n" +"- A norm (so we can say §5)\n" +"- Field operations (so we can add, subtract, multiply, divide)\n" +"- A few other technical properties for the proof to work\n" "\n" -"## The technique you mastered\n" +"Then this theorem automatically applies to both rational and real sequences - Lean will verify that ℚ and ℝ satisfy all our assumptions about §6.\n" "\n" -"The key technique here was splitting into cases:\n" -"- **Finitely many terms** (`m < N`): Handled by taking a maximum\n" -"- **Infinitely many terms** (`m ≥ N`): Handled by the Cauchy property\n" +"## Strategic Overview\n" "\n" -"This \"finite + infinite\" splitting technique appears throughout analysis!\n" +"The proof uses contradiction. We'll assume a bounded monotone sequence is not Cauchy, which means there are persistent gaps of size §7. Using the §8 tactic (as in the previous level), we'll extract subsequences that witness these gaps. Then we'll apply your orbit result to show these gaps accumulate without bound, contradicting the boundedness.\n" "\n" -"## Looking ahead\n" +"**Your goal:** Prove that if §9 is monotone and bounded above by §10, then §11 is Cauchy.\n" "\n" -"You've now built up the basic theory of Cauchy sequences. Next, we'll start connecting this back to the real numbers and exploring what it means for ℝ to be **complete**—the property that makes real analysis work!\n" +"Note: This level uses a \"black box\" helper lemma §12 that we'll prove in the next level. For now, trust that it captures how gaps accumulate under iteration.\n" "\n" -"Congratulations on completing this lecture!" -msgstr "" - -#: Game.Levels.L19Levels.L01 -msgid "If `Series a` converges absolutely, then for any `ε > 0`, there is an `N`, so that,\n" -" for any finite set `S` whose elements are all at least `N`, `∑ k ∈ S, |a k| < ε`." -msgstr "" - -#: Game.Levels.L10Pset.L10Pset3 -msgid "If sequences `a b : ℕ → ℝ` converge with `a` going to `L` and `b` going to `M`, then `a n * b n` converges to `L * M`." -msgstr "" - -#: Game.Levels.L19Levels.L04 -msgid "# Level 4 **Bigger Boss**: Conditional Convergence Theorem\n" +"## New Tools\n" "\n" -"Prepare yourself for one of the most shocking and counterintuitive theorems in all of mathematics!\n" +"### Definition: §13\n" +"A sequence §14 is monotone if §15 whenever §16.\n" +"\n" +"### Theorem: §17\n" +"To prove monotonicity, it's enough to check consecutive terms: if §18 for all §19, then §20 is §21.\n" +"\n" +"### Tactic: §22\n" +"Pushes negations through quantifiers: §23 becomes §24, §25 becomes §26, etc. Essential for proof by contradiction with complex statements.\n" +"\n" +"### The Helper Lemma: §27\n" +"Given a monotone sequence with persistent gaps of size §28 between subsequences §29 and §30, the orbit §31 accumulates at least §32 growth from the starting point. This will be proven in Level 3.\n" +"\n" +"§33" +msgstr "" + +#. §0: `FunLimAt f L c` +#. §1: `f(x) → L` +#. §2: `x → c` +#. §3: `SeqLim x L` +#. §4: `xₙ → L` +#. §5: `n → ∞` +#. §6: `f` +#. §7: `L` +#. §8: `c` +#. §9: `(xₙ)` +#. §10: `xₙ → c` +#. §11: `xₙ ≠ c` +#. §12: `f(xₙ) → L` +#. §13: `ε-δ` +#. §14: `FunLimAt f L c` +#. §15: `(xₙ)` +#. §16: `xₙ → c` +#. §17: `xₙ ≠ c` +#. §18: `f(xₙ) → L` +#. §19: `|f(xₙ) - L| < ε` +#. §20: `FunLimAt` +#. §21: `|x - c| < δ` +#. §22: `x ≠ c` +#. §23: `|f(x) - L| < ε` +#. §24: `SeqLimit` +#. §25: `|xₙ - c| < δ` +#. §26: `xₙ ≠ c` +#. §27: `|xₙ - c| < δ` +#. §28: `|f(xₙ) - L| < ε` +#. §29: `FunLimAt f L c → (∀ x : ℕ → ℝ, (∀ n, x n ≠ c) → SeqLimit x c → SeqLimit (fun n ↦ f (x n)) L)` +#. §30: `ε` +#. §31: `hε` +#. §32: `hf` +#. §33: `ε` +#. §34: `δ` +#. §35: `hx` +#. §36: `δ` +#. §37: `N` +#. §38: `N` +#. §39: `f(xₙ)` +#. §40: `L` +#: Game.Levels.L20Levels.L04 +msgid "# Level 4: Sequential Criterion for Limits\n" "\n" -"## The Astounding Theorem\n" +"We now have two notions of limits in our arsenal:\n" +"1. **Function limits:** §0 means §1 as §2\n" +"2. **Sequence limits:** §3 means §4 as §5\n" "\n" -"**Theorem (Riemann's Rearrangement Theorem)**: If a series `∑ a_n` converges but does *not* converge absolutely (i.e., it is *conditionally convergent*), then for **any** real number `L`, there exists a rearrangement `σ` such that the rearranged series `∑ a_(σ(n))` converges to `L`.\n" +"Could these concepts be connected? It's **mathematics**, how could they not!\n" "\n" -"In fact (though we won't prove it here), there also exist rearrangements that diverge to `+∞`, diverge to `-∞`, or oscillate without converging at all!\n" +"In this level, we'll prove the first half of the **Sequential Criterion for Limits**.\n" "\n" -"## What This Means\n" +"## The Sequential Criterion (Forward Direction)\n" "\n" -"If a series is only conditionally convergent, then:\n" +"**Theorem:** If §6 has limit §7 at §8, then for *every* sequence §9 with §10 and §11, we have §12.\n" "\n" -"**Infinite summation is as non-commutative as possible!!!**\n" +"In other words: function limits can be **tested** using sequences!\n" "\n" -"By cleverly rearranging the terms, we can make the series converge to *literally any value we want*. The sum depends entirely on the order in which we add the terms. There are no restrictions—pick any target `L ∈ ℝ`, and we can rearrange to hit it exactly.\n" +"## Why This Matters\n" "\n" -"## A Concrete Example\n" +"This theorem is incredibly useful because:\n" +"- It connects two different limit concepts\n" +"- It lets us use sequence intuition to understand function limits\n" +"- It may be easier to work with certain sequences than with the §13 definition\n" "\n" -"Consider the alternating harmonic series:\n" -"`∑_{k=1}^∞ (-1)^(k+1)/k = 1 - 1/2 + 1/3 - 1/4 + 1/5 - 1/6 + ... = ln 2`\n" +"## The Proof Strategy\n" "\n" -"This converges to `ln 2 ≈ 0.693` but not absolutely (the harmonic series diverges).\n" +"**Given:** §14 and a sequence §15 with §16 and §17.\n" "\n" -"By Riemann's theorem, we can rearrange it to converge to:\n" -"- `π` (or any other positive number)\n" -"- `0` (or any negative number)\n" -"- `1000000` (or any huge number)\n" -"- `-1/137` (or any specific target you want)\n" +"**Want:** To show §18, i.e., for all ε > 0, eventually §19.\n" "\n" -"The same terms, but a different order, give a completely different answer!\n" +"**How:**\n" +"1. Given ε > 0, use §20 to get δ > 0 such that §21 and §22 implies §23\n" +"2. Use §24 to get N such that for all n ≥ N, we have §25\n" +"3. For n ≥ N, we know §26 and §27, so §28\n" "\n" -"## The Complete Dichotomy\n" +"## Your Challenge\n" "\n" -"Combined with Level 3, we now have a stunning dichotomy:\n" -"- **Absolute convergence** → rearrangement invariance (sum never changes)\n" -"- **Conditional convergence** → complete chaos (sum can be anything)\n" +"Prove the forward direction of the sequential criterion:\n" "\n" -"There is no middle ground! Either order doesn't matter at all, or order is everything.\n" +"§29\n" "\n" -"## Why You Can't Just Use Positive Terms\n" +"**Hint:** After introducing all the hypotheses, introduce §30 and §31. Use §32 with §33 to get §34 and its properties. Then use §35 with §36 to get §37. Use this §38 to show that the sequence §39 converges to §40." +msgstr "" + +#. §0: `(a : ℕ → ℝ) (L : ℝ) := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε` +#. §1: `a : ℕ → ℝ` +#. §2: `L : ℝ` +#. §3: `SeqLim a L` +#. §4: `ε > 0` +#. §5: `N : ℕ` +#. §6: `n ≥ N` +#. §7: `|a n - L| < ε` +#: Game.Levels.L2NewtonsCalculationOfPi.L01_SeqConvDef +msgid "§0\n" "\n" -"Note that we cannot simply take all the positive terms and ignore the negative terms—that wouldn't be a rearrangement at all, since a rearrangement must include every term of the original series exactly once. The challenge is to interleave positive and negative terms cleverly so that all terms appear while still hitting our target.\n" +"For a sequence §1 and a real number §2, we say that §3 holds if: for every §4, there exists §5 such that for all §6, we have §7." +msgstr "" + +#. §0: `bound` +#: Game.Levels.L3Levels.L01_ArchProp +msgid "The §0 tactic can solve many \\\\\"trivial\\\\\" inequalities involving standard functions and basic arithmetic." +msgstr "" + +#. §0: `a n ≤ b n` +#. §1: `n` +#. §2: `Series a n ≤ Series b n` +#. §3: `n` +#. §4: `∑ k ∈ range n, a k ≤ ∑ k ∈ range n, b k` +#. §5: `0 ≤ a n ≤ b n` +#. §6: `n` +#. §7: `∑ b n` +#. §8: `M` +#. §9: `∑ a n` +#. §10: `∑ a n ≤ M` +#. §11: `0 ≤ 0` +#. §12: $\\sum_{k