diff --git a/.i18n/en/Game.pot b/.i18n/en/Game.pot index 00202e0..7b94a3b 100644 --- a/.i18n/en/Game.pot +++ b/.i18n/en/Game.pot @@ -1160,10 +1160,6 @@ msgstr "" msgid "Lecture 19: Rearrangements" msgstr "" -#: Game -msgid "A First Course in Real Analysis" -msgstr "" - #: Game.Levels.L24Levels.L03 msgid "`(S : Set ℝ) (L : ℝ) : Prop := IsUB S L ∧ ∀ M, IsUB S M → L ≤ M`\n" "\n" @@ -1288,10 +1284,6 @@ msgstr "" msgid "A finite list has a maximum element." msgstr "" -#: Game -msgid "An Introduction to (Formal) Real Analysis" -msgstr "" - #: Game.Levels.L14Levels.L01_BolzanoWeierstrass msgid "# Level 1 **Big Boss:** Bolzano-Weierstrass\n" "\n" @@ -2576,6 +2568,120 @@ msgid "# Level 5: Heine-Borel Theorem: Part 2b\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.L2NewtonsCalculationOfPi.L01_SeqConvDef +msgid "# Level 1: The Main Definition\n" +"\n" +"Our first step to making Newton's argument rigorous is\n" +"to spell out *exactly* what we mean by a sequence\n" +"$a_n$ converging. It will take a little work to build up to the definition, and more importantly, *why*\n" +"that might seem like a reasonable definition to have.\n" +"\n" +"But first: for some reason (likely Euler is to blame), mathematics has *two* completely different conventions for how to write functions. For general functions $f : \\mathbb R \\to\\mathbb R$,\n" +"we write $f(x)$, with parentheses. But when work with sequences, $a_n$, meaning,\n" +"$a_0, a_1, a_2, \\dots$, we bizarrely switch instead to subscripts.\n" +"Why? Historical accident.\n" +"A sequence is nothing but a function whose \"domain\" (that is, the set of\n" +"inputs to the function) is the natural numbers; so we will break\n" +"with tradition and unify the two conventions, henceforth writing\n" +"$a : \\mathbb N \\to \\mathbb R$ for sequences of real numbers, $a (0), a (1),\n" +"a (2), \\dots$.\n" +"\n" +"Now, the definition that mathematicians eventually came up with\n" +"for what it means for a sequence to converge, was so intricate (at least\n" +"at first sight) that it had to be invented *twice*!\n" +"The eventual formulation crystallized through the work of Karl Weierstrass in the 1860s, who transformed analysis from an intuitive art into a rigorous science. However, the seeds of this idea appeared much earlier in the work of Bernard Bolzano. In the 1810s and 1820s, Bolzano was developing remarkably modern ideas about continuity and limits, but he was too far ahead of his time for the mathematical community to accept these abstract concepts.\n" +"Only by Weierstrass's time -- a half-century later -- did these ideas catch on.\n" +"\n" +"Without further ado, here it is:\n" +"\n" +"Given a sequence `a : ℕ → ℝ` and a real number `L : ℝ`, we\n" +"write `lim a = L` and\n" +"say that the sequence `a` **converges** to `L`,\n" +" if:\n" +"\n" +"For every `ε > 0`, there exists `N : ℕ` such that, for all `n ≥ N`, we have `|a (n) - L| < ε`.\n" +"\n" +"\n" +"This definition is probably not the first, or second, or tenth thing you might've come up with.\n" +"But over time, I hope you'll come to see that it\n" +" embodies a beautiful negotiation between precision and effort.\n" +"\n" +" I like to think of it as a conversation between an Engineer and a Machinist. The Engineer arrives with specifications: 'We're going to make this widget, and I need its length to be 1 foot, with an error tolerance\n" +" of 1/100 of an inch'. The Machinist replies: 'Sure, I can do that, but I'll have to run my special equipment for at least 10 hours to guarantee that tolerance.' The Enginner\n" +" replies: 'I'm sorry, I misspoke, can we change the tolerance\n" +" to 1/1000 of an inch?' The Machinist replies: 'Oof, yeah we can do it, but it'll cost ya. I'll need at least 40 hours of operation, but after that, I'll guarantee it.'\n" +"\n" +"As long as this conversation can continue regardless of *whatever* tolerance `ε > 0` the Engineer requires, with the Machinist\n" +"always being able to reply with a finite minimum number of hours `N`,\n" +"after which the tolerance will be achieved, we can say\n" +"that the equipment **converges**.\n" +"\n" +"Now let's read Weierstrauss's (or is it Bolzano's?) definition again. We have some process\n" +"that at time `n` returns a reading `a (n)` (think: widget length). Our ultimate goal is to make the length `L`. If\n" +"for any tolerance `ε > 0`, no matter how small, there will always exist some minimum\n" +"time `N`, so that, for any future time, `n ≥ N`,\n" +"we are guaranteed to be within that tolerance, `|a (n) - L| < ε`, that's exactly the condition under which we'll\n" +"say that the sequence `a (n)` **converges** to `L`.\n" +"\n" +"[![A Sequence Converging](images/SeqLim.jpg)](https://en.wikipedia.org/wiki/Limit_of_a_sequence)\n" +"\n" +"What makes this definition so powerful is its universality. The Machinist is essentially promising: 'Give me *any* tolerance requirement, no matter how stringent, and I can meet it -- though I might need more resources (larger `N`) for tighter specifications.'\n" +"\n" +"\n" +"Notice something else about the definition: It makes no mention of something happening \"eventually\", or \"at infinity\" or any other wishy-washy squirm words. We have traded the ambiguity of speaking about infinity for the precision of existential and universal quantifiers. No more hand-waving about what happens \"as `n` gets large\" - instead, we have a concrete challenge: given *any* tolerance `ε`, can you find a specific threshold `N`? *That* idea was the key breakthrough that allowed Calculus to enter the realm of rigorous mathematics.\n" +"\n" +"In Lean, the definition is written like so:\n" +"\n" +"`def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=\n" +" ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε`\n" +"\n" +"This syntax should be familiar from the `have` tactic you already know and love.\n" +"The special symbol `def` (instead of `have`) means that we're about to define something, and\n" +"`SeqLim` is its name (for sequence limit, of course; but we could have called it whatever we want). Then our assumptions are a sequence `a : ℕ → ℝ` and\n" +"some real number `L : ℝ`. Then after the colon `:` goes our output, which in this case is `Prop`, that is, a statement (proposition) that can be true or false. So `SeqLim` is really a function that takes a sequence and hypothetical limiting value, and returns true or false based on whether\n" +"the condition is satisfied. Then comes a colon-equals `:=`, after which the\n" +"exact condition to be tested is specified. And the condition is what we already said, for all epsilon, yadda yadda. The big difference is that you can write `have` inside a proof, but you can't write `def` inside a proof;\n" +"`def` is reserved for making global definitions that\n" +"can be referenced forever once they're introduced.\n" +"Notice that on the right hand side, the list\n" +"of Definitions now includes `SeqLim`, and, as usual,\n" +"if you forget what it means, you can click on it for a reminder.\n" +"\n" +"Let's try out the definition in practice!\n" +"\n" +"**Your Task**\n" +"\n" +"Prove that the constant sequence converges to the same constant.\n" +"That is, suppose that you have a sequence `a : ℕ → ℝ`, and there's a real number\n" +"`L`, and a hypothesis that, for all values of `n`, we have `a (n) = L`; then prove that `a` does converge, and converges to `L`. This is the simplest possible case: if our 'factory' always produces the exact target value `L`, then we can meet any tolerance requirement immediately!\n" +"\n" +"You may find useful a new tactic called `change`. It allows you to replace a goal (or hypothesis) by\n" +"something that is definitionally equal to it. In our example here,\n" +"You will see the goal as `SeqLim a L`. What are you supposed to do with that,\n" +"how can you make progress? Well, if you remember how `SeqLim` is defined,\n" +"then you can replace the goal with the definition, by writing\n" +"\n" +"`change ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε`\n" +"\n" +"Lean will then change the goal to its definition.\n" +"Remember that `ε`, `N`, and `n` are all dummy variables\n" +"here, so you can have some fun:\n" +"\n" +"`change ∀ Alice > 0, ∃ Bob : ℕ, ∀ blah ≥ Bob, |a blah - L| < Alice`\n" +"\n" +"This may come in handy later. (Not Alice and Bob *per se*, but the ability to give better names for dummy variables, so as not to clash with already existing variable names...)\n" +"\n" +"**⚠️⚠️⚠️ CAUTION ⚠️⚠️⚠️** Remember how Lean *must* have space after a function name, it won't accept `f(x)` but instead requires `f (x)`? Well... it's the other way around for absolute\n" +"values. Lean won't accept a space after an absolute value.\n" +"So if you write `| a n - L|`, you'll get an error message.\n" +"Same with `|a n - L |` -- the space at the end is the problem. Sorry! I didn't write the syntax.\n" +"\n" +"**Normalizing Numerical Values**: And one last tactic you might also find useful is `norm_num` (for normalizing numerical values); it evaluates numerical expressions and proves equalities/inequalities involving concrete numbers. For example, if you're stuck with an `|0|` at some point,\n" +"and you want to convert it to plain old `0`, try calling `norm_num`.\n" +"\n" +"Ok, get to it!" +msgstr "" + #: Game.Levels.L7Levels.L01_Eventually msgid "If `a : ℕ → ℝ` converges to `L` and `L ≠ 0`, then there is an `N` so that\n" "for all `n ≥ N`, `|a (n)| ≥ |L| / 2`." @@ -3744,23 +3850,6 @@ msgstr "" msgid "We need to find `N`. Use the Archimedean Property: there exists `N` such that `1 / ε < N`. Try: `have f1 : ∃ (N : ℕ), 1 / ε < N := by apply ArchProp hε`" msgstr "" -#: Game -msgid "*An Introduction to Formal Real Analysis - Interactive Edition*\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 `ε`-`δ` 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.L12Levels.L01_MonotoneBdd msgid "## What You've Accomplished\n" "\n" @@ -6152,22 +6241,6 @@ msgid "# Level 4: Reciprocals of Convergent Sequences — Big Boss Level\n" "involving fractions. You have all the tools you need—now it's time to put them together!" msgstr "" -#: Game -msgid "# Welcome to Real Analysis, The Game!\n" -"\n" -"This course is currently being developed for Rutgers University Math 311H by [Alex Kontorovich](https://math.rutgers.edu/~alexk).\n" -" Please email alex.kontorovich@rutgers.edu for suggestions/corrections,\n" -"or better yet, post a PR/issue to\n" -"https://github.com/AlexKontorovich/RealAnalysisGame.\n" -"\n" -"For the main course website, go to: https://alexkontorovich.github.io/2025F311H.\n" -"\n" -"This course takes you through an Introduction to the Real Numbers, rigorous `ε`-`δ` Calculus,\n" -"and basic Point-Set Topology.\n" -"To get started, click on\n" -"**\"Level 1: The Story of Real Analysis\"**, and good luck!" -msgstr "" - #: Game.Levels.L16Levels.L01_check msgid "Series" msgstr "" @@ -7455,6 +7528,23 @@ msgstr "" msgid "Lecture 6: Algebraic Limit Theorem, Part II" msgstr "" +#: 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 `ε`-`δ` 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.L21Levels.L05 msgid "# Level 1: Sequential Criterion for Limits (Backward Direction)\n" "\n" @@ -9327,6 +9417,11 @@ msgid "# Level 2: Uniform Convergence\n" "Ready to fix Cauchy's \"mistake\" and see how the right kind of convergence preserves continuity? The $\\varepsilon/3$ method awaits!" msgstr "" +#: Game +#: Game +msgid "Real Analysis, The Game" +msgstr "" + #: Game.Levels.L23Levels.L03 msgid "Compactness" msgstr "" @@ -9934,6 +10029,19 @@ msgstr "" msgid "Prove `Bdd_of_LimAt`" msgstr "" +#: Game +msgid "# Welcome to Real Analysis, The Game! (v0.1)\n" +"\n" +"This course is was developed for Rutgers University Math 311H by [Alex Kontorovich](https://math.rutgers.edu/~alexk).\n" +"\n" +"Follow along with the course lecture notes and videos, available here: https://alexkontorovich.github.io/2025F311H.\n" +"\n" +"This course takes you through an Introduction to the Real Numbers, rigorous `ε`-`δ` Calculus,\n" +"and basic Point-Set Topology.\n" +"To get started, click on\n" +"**\"Level 1: The Story of Real Analysis\"**, and good luck!" +msgstr "" + #: Game.Levels.L18Pset.L01 msgid "This is the analog of `sum_range_succ` to summing on intervals." msgstr "" @@ -10335,120 +10443,6 @@ msgid "# Level 3: Cauchy Implies Bounded\n" "Good luck!" msgstr "" -#: Game.Levels.L2NewtonsCalculationOfPi.L01_SeqConvDef -msgid "# Level 1: The Main Definition\n" -"\n" -"Our first step to making Newton's argument rigorous is\n" -"to spell out *exactly* what we mean by a sequence\n" -"$a_n$ converging. It will take a little work to build up to the definition, and more importantly, *why*\n" -"that might seem like a reasonable definition to have.\n" -"\n" -"But first: for some reason (likely Euler is to blame), mathematics has *two* completely different conventions for how to write functions. For general functions $f : \\mathbb R \\to\\mathbb R$,\n" -"we write $f(x)$, with parentheses. But when work with sequences, $a_n$, meaning,\n" -"$a_0, a_1, a_2, \\dots$, we bizarely switch instead to subscripts.\n" -"Why? Historical accident.\n" -"A sequence is nothing but a function whose \"domain\" (that is, the set of\n" -"inputs to the function) is the natural numbers; so we will break\n" -"with tradition and unify the two conventions, henceforth writing\n" -"$a : \\mathbb N \\to \\mathbb R$ for sequences of real numbers, $a (0), a (1),\n" -"a (2), \\dots$.\n" -"\n" -"Now, the definition that mathematicians eventually came up with\n" -"for what it means for a sequence to converge, was so intricate (at least\n" -"at first sight) that it had to be invented *twice*!\n" -"The eventual formulation crystallized through the work of Karl Weierstrass in the 1860s, who transformed analysis from an intuitive art into a rigorous science. However, the seeds of this idea appeared much earlier in the work of Bernard Bolzano. In the 1810s and 1820s, Bolzano was developing remarkably modern ideas about continuity and limits, but he was too far ahead of his time for the mathematical community to accept these abstract concepts.\n" -"Only by Weierstrass's time -- a half-century later -- did these ideas catch on.\n" -"\n" -"Without further ado, here it is:\n" -"\n" -"Given a sequence `a : ℕ → ℝ` and a real number `L : ℝ`, we\n" -"write `lim a = L` and\n" -"say that the sequence `a` **converges** to `L`,\n" -" if:\n" -"\n" -"For every `ε > 0`, there exists `N : ℕ` such that, for all `n ≥ N`, we have `|a (n) - L| < ε`.\n" -"\n" -"\n" -"This definition is probably not the first, or second, or tenth thing you might've come up with.\n" -"But over time, I hope you'll come to see that it\n" -" embodies a beautiful negotiation between precision and effort.\n" -"\n" -" I like to think of it as a conversation between an Engineer and a Machinist. The Engineer arrives with specifications: 'We're going to make this widget, and I need its length to be 1 foot, with an error tolerance\n" -" of 1/100 of an inch'. The Machinist replies: 'Sure, I can do that, but I'll have to run my special equipment for at least 10 hours to guarantee that tolerance.' The Enginner\n" -" replies: 'I'm sorry, I misspoke, can we change the tolerance\n" -" to 1/1000 of an inch?' The Machinist replies: 'Oof, yeah we can do it, but it'll cost ya. I'll need at least 40 hours of operation, but after that, I'll guarantee it.'\n" -"\n" -"As long as this conversation can continue regardless of *whatever* tolerance `ε > 0` the Engineer requires, with the Machinist\n" -"always being able to reply with a finite minimum number of hours `N`,\n" -"after which the tolerance will be achieved, we can say\n" -"that the equipment **converges**.\n" -"\n" -"Now let's read Weierstrauss's (or is it Bolzano's?) definition again. We have some process\n" -"that at time `n` returns a reading `a (n)` (think: widget length). Our ultimate goal is to make the length `L`. If\n" -"for any tolerance `ε > 0`, no matter how small, there will always exist some minimum\n" -"time `N`, so that, for any future time, `n ≥ N`,\n" -"we are guaranteed to be within that tolerance, `|a (n) - L| < ε`, that's exactly the condition under which we'll\n" -"say that the sequence `a (n)` **converges** to `L`.\n" -"\n" -"[![A Sequence Converging](images/SeqLim.jpg)](https://en.wikipedia.org/wiki/Limit_of_a_sequence)\n" -"\n" -"What makes this definition so powerful is its universality. The Machinist is essentially promising: 'Give me *any* tolerance requirement, no matter how stringent, and I can meet it -- though I might need more resources (larger `N`) for tighter specifications.'\n" -"\n" -"\n" -"Notice something else about the definition: It makes no mention of something happening \"eventually\", or \"at infinity\" or any other wishy-washy squirm words. We have traded the ambiguity of speaking about infinity for the precision of existential and universal quantifiers. No more hand-waving about what happens \"as `n` gets large\" - instead, we have a concrete challenge: given *any* tolerance `ε`, can you find a specific threshold `N`? *That* idea was the key breakthrough that allowed Calculus to enter the realm of rigorous mathematics.\n" -"\n" -"In Lean, the definition is written like so:\n" -"\n" -"`def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=\n" -" ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε`\n" -"\n" -"This syntax should be familiar from the `have` tactic you already know and love.\n" -"The special symbol `def` (instead of `have`) means that we're about to define something, and\n" -"`SeqLim` is its name (for sequence limit, of course; but we could have called it whatever we want). Then our assumptions are a sequence `a : ℕ → ℝ` and\n" -"some real number `L : ℝ`. Then after the colon `:` goes our output, which in this case is `Prop`, that is, a statement (proposition) that can be true or false. So `SeqLim` is really a function that takes a sequence and hypothetical limiting value, and returns true or false based on whether\n" -"the condition is satisfied. Then comes a colon-equals `:=`, after which the\n" -"exact condition to be tested is specified. And the condition is what we already said, for all epsilon, yadda yadda. The big difference is that you can write `have` inside a proof, but you can't write `def` inside a proof;\n" -"`def` is reserved for making global definitions that\n" -"can be referenced forever once they're introduced.\n" -"Notice that on the right hand side, the list\n" -"of Definitions now includes `SeqLim`, and, as usual,\n" -"if you forget what it means, you can click on it for a reminder.\n" -"\n" -"Let's try out the definition in practice!\n" -"\n" -"**Your Task**\n" -"\n" -"Prove that the constant sequence converges to the same constant.\n" -"That is, suppose that you have a sequence `a : ℕ → ℝ`, and there's a real number\n" -"`L`, and a hypothesis that, for all values of `n`, we have `a (n) = L`; then prove that `a` does converge, and converges to `L`. This is the simplest possible case: if our 'factory' always produces the exact target value `L`, then we can meet any tolerance requirement immediately!\n" -"\n" -"You may find useful a new tactic called `change`. It allows you to replace a goal (or hypothesis) by\n" -"something that is definitionally equal to it. In our example here,\n" -"You will see the goal as `SeqLim a L`. What are you supposed to do with that,\n" -"how can you make progress? Well, if you remember how `SeqLim` is defined,\n" -"then you can replace the goal with the definition, by writing\n" -"\n" -"`change ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε`\n" -"\n" -"Lean will then change the goal to its definition.\n" -"Remember that `ε`, `N`, and `n` are all dummy variables\n" -"here, so you can have some fun:\n" -"\n" -"`change ∀ Alice > 0, ∃ Bob : ℕ, ∀ blah ≥ Bob, |a blah - L| < Alice`\n" -"\n" -"This may come in handy later. (Not Alice and Bob *per se*, but the ability to give better names for dummy variables, so as not to clash with already existing variable names...)\n" -"\n" -"**⚠️⚠️⚠️ CAUTION ⚠️⚠️⚠️** Remember how Lean *must* have space after a function name, it won't accept `f(x)` but instead requires `f (x)`? Well... it's the other way around for absolute\n" -"values. Lean won't accept a space after an absolute value.\n" -"So if you write `| a n - L|`, you'll get an error message.\n" -"Same with `|a n - L |` -- the space at the end is the problem. Sorry! I didn't write the syntax.\n" -"\n" -"**Normalizing Numerical Values**: And one last tactic you might also find useful is `norm_num` (for normalizing numerical values); it evaluates numerical expressions and proves equalities/inequalities involving concrete numbers. For example, if you're stuck with an `|0|` at some point,\n" -"and you want to convert it to plain old `0`, try calling `norm_num`.\n" -"\n" -"Ok, get to it!" -msgstr "" - #: Game.Levels.L6Levels.L04_Cases' msgid "Cases'" msgstr "" diff --git a/images/cover.png b/images/cover.png new file mode 100644 index 0000000..8958477 Binary files /dev/null and b/images/cover.png differ