diff --git a/Game/Levels/L25Lecture.lean b/Game/Levels/L25Lecture.lean index 538393e..184cba4 100644 --- a/Game/Levels/L25Lecture.lean +++ b/Game/Levels/L25Lecture.lean @@ -75,7 +75,7 @@ Hilbert steps out of his office, and sighs with disappointment. \"I'm very sorry The clerk is shocked. \"But Professor, why not? We've handled infinitely many buses with infinitely many passengers before! This is just *one* bus!\" -Hilbert says to the clerk, \"Take out the ledger. Let's work backwards. Imagine that we're done placing *every single person* from that bus into a room. So in room `R1`, we have `ABBAAA...`, say, and in room `R2`, we have `AAABBB...`, and in room `R3` is `BABBAA...` and so on. Ok? I claim we're not done, and we've left someone off the ledger. If I can prove to you that there's at least one passenger hasn't been assigned a room, then do you see how the entire enterprise is futile?\" +Hilbert says to the clerk, \"Take out the ledger. Let's work backwards. Imagine that we're done placing *every single person* from that bus into a room. So in room `R1`, we have `ABBAAA...`, say, and in room `R2`, we have `AAABBB...`, and in room `R3` is `BABBAA...` and so on. Ok? I claim we're not done, and we've left someone off the ledger. If I can prove to you that at least *one passenger hasn't been assigned a room, then do you see how the entire enterprise is futile?\" The clerk nods reluctantly. Hilbert continues: \"The person in room `R1` is named `ABBAAA...`, which starts with `A`. So if I give you the name of a person whose first letter is `B`, then that person is certainly not in room `R1`, right?\" The clerk nods. \"Now, the person in room `R2` is named `AAABBB...`. If I give you the name of a person whose *second* letter is `B`, then that differs from the second letter of the person in room `R2`, and so that person is not in room `R2`. Do you follow?\" The clerk nods again. diff --git a/Game/Levels/L25Levels/L01.lean b/Game/Levels/L25Levels/L01.lean index 18a56a2..ca4246d 100644 --- a/Game/Levels/L25Levels/L01.lean +++ b/Game/Levels/L25Levels/L01.lean @@ -11,10 +11,24 @@ Title "Uniform Convergence Implies Integrability" Introduction " # Level 1: Uniform Convergence Implies Integrability -Show that if you have a sequence of functions `fₙ` that converge uniformly to `F`, and each `fₙ` is integrable, then `F` is also integrable, and that `∫ F = lim (∫ fₙ)`. This justifies Newton's calculation from Lecture 2, where we integrated the infinite series term-by-term! Indeed, for any finite sum, we can certainly integrate term-by-term, since the integral is linear. With this theorem, we can now extend that to infinite sums, provided the convergence is uniform (something that remains to be shown for Newton's example...). +We finally prove the fundamental theorem that justifies Newton's bold term-by-term integration of infinite series! If a sequence of integrable functions `fₙ` converges uniformly to `F`, then `F` is also integrable, and crucially: -Note that we assume *nothing* about continuity of either the `fₙ` nor `F` here; integrability is a strictly weaker condition, but suffices for the conclusion! +$$\\int F = \\lim (\\int fₙ)$$ +or equivalently: $$\\int(\\lim fₙ) = \\lim (\\int fₙ)$$ + +This theorem is the rigorous foundation behind Newton's calculation from Lecture 2, where he integrated the binomial series term-by-term to compute π. + +**Why uniform convergence?** As Socrates showed with his examples, pointwise convergence alone fails spectacularly: +- Step functions shifting to infinity: `∫ fₙ = 1` but `∫(lim fₙ) = 0` +- Spike functions on `[0,1]`: `∫ fₙ = 1` but `∫(lim fₙ) = 0` +- Even continuous tent functions: `∫ fₙ = 1` but `∫(lim fₙ) = 0` + +The key insight is that uniform convergence gives us simultaneous control over all function values. If `|fₙ(x) - F(x)| < ε/(b-a)` for all `x` and large `n`, then Riemann sum differences are bounded by `ε`, allowing us to interchange limits and integrals. + +**Remarkable fact**: We assume *nothing* about continuity! Integrability is strictly weaker than continuity, yet suffices for this profound result. + +This theorem bridges the gap between finite and infinite processes, making rigorous what Newton intuited centuries ago. " namespace RealAnalysisGame @@ -78,4 +92,18 @@ linarith [b2, hMmax, hN1, hN2, Nbnd1, Nbnd2] end RealAnalysisGame Conclusion " +**Victory!** You've just proven one of the most important theorems in real analysis. This result: + +- **Validates Newton's genius**: His term-by-term integration of power series, done purely by intuition in the 1660s, now has rigorous justification +- **Bridges finite and infinite**: Extends the linearity of integrals from finite sums to infinite series (under uniform convergence) +- **Enables modern analysis**: Makes possible the rigorous treatment of Fourier series, differential equations with series solutions, and much of mathematical physics + +The proof strategy you used—controlling Riemann sum differences via uniform convergence—is a masterclass in how sophisticated mathematical concepts work together. You leveraged: +- The completeness of ℝ (Cauchy sequences converge) +- The definition of integrability (Riemann sums) +- Uniform convergence (simultaneous control over all function values) + +**Historical note**: This theorem wasn't rigorously proven until the late 1800s, over 200 years after Newton used it! Mathematicians like Weierstrass, Riemann, and others had to develop the very foundations of real analysis to make Newton's intuitive leaps rigorous. + +You've now mastered the deep connection between limits and integrals. In Level 2, we'll use all the machinery we've built to prove the most 'obvious' theorem in mathematics—one so intuitive that it was assumed without proof for over 2000 years! " diff --git a/Game/Levels/L25Levels/L02.lean b/Game/Levels/L25Levels/L02.lean index 9f2bdf5..c14cd79 100644 --- a/Game/Levels/L25Levels/L02.lean +++ b/Game/Levels/L25Levels/L02.lean @@ -9,11 +9,19 @@ Title "Intermediate Value Theorem" Introduction " # Level 2 **BIG BOSS**: Intermediate Value Theorem -And let's finish off the whole course with the \"greatest\" theorem of all! The one everyone assumed was true because -it was completely **obvious**, but which now we can finally prove rigorously using all the tools we've built up so far! +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**. -**The Intermediate Value Theorem**: If a function `f` is continuous on a closed interval `[a, b]`, and takes values `f(a) < 0` and `0 < f(b)`, then there exists some `c ∈ (a, b)` such that `f(c) = 0`. In other words, the function crosses the x-axis somewhere in the interval. +**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`. +*Translation*: A continuous function that changes sign must cross zero somewhere. + +**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**. + +**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! + +**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. + +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? " namespace RealAnalysisGame @@ -124,4 +132,20 @@ use c, hcc, fc end RealAnalysisGame Conclusion " +**COURSE COMPLETE!** You've just proven the most fundamental theorem about continuous functions and conquered the final boss of Real Analysis: The Game. + +**What you accomplished**: You proved that continuous functions have no \"jumps\"—a property so basic that mathematicians assumed it for millennia without proof. Your proof revealed the intimate connection between: +- **Topology** (continuity of functions) +- **Order** (the structure of real numbers) +- **Completeness** (the Least Upper Bound Principle) + +**The deeper significance**: This \"obvious\" theorem actually characterizes what makes ℝ special. In ℚ, continuous functions CAN change sign without crossing zero (like x² - 2). The IVT is really a theorem about the **completeness** of the real line—there are no gaps. + +**Your proof technique** was a masterpiece of mathematical reasoning: you used the supremum of a carefully chosen set, then eliminated both f(c) < 0 and f(c) > 0 through elegant contradictions involving continuity. This is analysis at its finest. + +**Historical triumph**: You've now rigorously proven what Archimedes used, what Newton assumed, and what Euler took for granted. The theorem they used intuitively for centuries finally has the rigorous foundation it deserves. + +**Congratulations!** You've mastered the interplay between limits, continuity, completeness, and proof—the very heart of real analysis. From ε-δ definitions to the deepest theorems about ℝ, you've built mathematics from the ground up. + +*Welcome to the ranks of real analysts.* "