New Smooth Take-Off planet

Game.lean

@@ -32,6 +32,7 @@ import Game.Levels.Cartan
 import Game.Levels.Aquarium
 import Game.Levels.Shade
 import Game.Levels.Slope
+import Game.Levels.Smooth
 
 -- *uncomment the following line to get the incomplete planets.*
 -- import Game.DevPlanets
@@ -67,6 +68,9 @@ Dependency Samarkand → Ciao
 Dependency Iso → Ciao
 Dependency Euklid → Ciao
 
+Dependency Slope → Smooth  -- because of `HasDerivAt` / `hasDerivAt_iff_tendsto_slope`
+Dependency Cartan → Smooth -- because of `eventually_lt_nhds` / `=ᶠ`
+
 -- set_option lean4game.showDependencyReasons true
 
 /-! Build the game. Show's warnings if it found a problem with your game.

Game/Doc/Definition.lean

@@ -597,6 +597,11 @@ DefinitionDoc MvPolynomial as "MvPolynomial" in "R[X]"
 -/
 DefinitionDoc MvPolynomial.X as "X (MvPolynomial.X)" in "R[X]"
 
+/--
+`X n` is the degree `1` monomial $X_n$.
+-/
+DefinitionDoc MvPolynomial.X as "MvPolynomial.X"
+
 /--
 For a matrix `A`, `trace A` is the trace of `A`. The expression is also equivalent to `∑ i, A i i` in Leanic.
 -/
@@ -694,6 +699,20 @@ to expand this into the usual definition of the derivative in terms of the `slop
 -/
 DefinitionDoc HasDerivAt as "HasDerivAt" in "Function"
 
+/-- `p.eval a` evaluates the polynomial `p` at the point `a`, substituting
+`a` for the variable `X`. -/
+DefinitionDoc Polynomial.eval as "eval"
+
+/-- `Real.exp x` is the exponential function $e^x$. -/
+DefinitionDoc Real.exp as "Real.exp" in "Function"
+
+/-- For a polynomial `p`, `derivative p` (also written `p.derivative`) is its
+formal derivative. -/
+DefinitionDoc Polynomial.derivative as "Polynomial.derivative"
+
+/-- For polynomials `p` and `q`, `p.comp q` is their composition as a polynomial,
+obtained by substituting `q` for the variable `X` in `p`; that is, $p(q(X))$. -/
+DefinitionDoc Polynomial.comp as "Polynomial.comp"
 /--
 For types `α` and `β`, `α ≃ β` or (`Equiv α β`) is the type of functions from `α → β` with a
 two-sided inverse.  A term `f : α ≃ β` has four components:

Game/Levels/Babylon/L01_Sum_Simp_Card.lean

@@ -43,9 +43,3 @@ Conclusion "**Babylonier**: Sehr gut, das passt!"
 Conclusion "Conclusion Babylon L01"
 
 NewDefinition Finset.card
-
-/-
-**Robo**: Mir fällt gerade ein, du hattest ja mal gefragt bezüglich `rw` unter Quantoren.
-Mit Summen ist das das gleiche: Hier musst du immer `simp_rw` verwenden, wenn du innerhalb
-einer Summe was umschreiben möchtest."
--/

Game/Levels/Saturn.lean

@@ -1,8 +1,9 @@
 import Game.Levels.Saturn.L01_Rewrite_equality
 import Game.Levels.Saturn.L02_Ring_add_pow_two
-import Game.Levels.Saturn.L03_mul_comm
-import Game.Levels.Saturn.L04_mul_assoc
-import Game.Levels.Saturn.L05_Ring
+import Game.Levels.Saturn.L03_Polynomial
+import Game.Levels.Saturn.L04_mul_comm
+import Game.Levels.Saturn.L05_mul_assoc
+import Game.Levels.Saturn.L06_Ring
 
 /-!
 The planet `Saturn` introduces the tactics `ring` and `rw`.

Game/Levels/Saturn/L03_Polynomial.lean

@@ -0,0 +1,24 @@
+import Game.Metadata
+
+World "Saturn"
+Level 3
+
+Title ""
+
+Introduction "Intro Saturn L03:
+`Polynomial ℚ` is a type of univariate polynomial over `ℚ`.
+And `X` is the polynomial variable in the polynomial ring `ℚ[X]`. "
+
+namespace Polynomial
+
+Statement : (X : Polynomial ℚ) + X + X ^ 2 = X ^ 2 + 2 * X := by
+  ring
+
+Conclusion "Conclusion Saturn L03"
+
+NewTactic ring
+
+/---/
+DefinitionDoc Polynomial as "Polynomial"
+
+NewDefinition Polynomial Polynomial.X

Game/Levels/Saturn/L04_mul_comm.lean

@@ -0,0 +1,20 @@
+import Game.Metadata
+
+World "Saturn"
+Level 4
+
+Introduction "Intro Saturn L04"
+
+namespace Polynomial
+Statement (P : ℚ[X]) : X * P = P * X := by
+  Hint "Explain: `P` is polynomial over `ℚ` with indeterminate `X`"
+  ring
+
+Conclusion "Conclusion Saturn L04"
+NewTactic ring
+
+/---/
+TheoremDoc mul_comm as "mul_comm" in "+ *"
+
+NewTheorem mul_comm
+NewDefinition Polynomial Polynomial.X

Game/Levels/Saturn/L04_mul_assoc.lean → Game/Levels/Saturn/L05_mul_assoc.lean

@@ -1,10 +1,10 @@
 import Game.Metadata
 
 World "Saturn"
-Level 4
+Level 5
 
 -- Introduction "Noch ein Funkspruch."
-Introduction "Intro Saturn L04"
+Introduction "Intro Saturn L05"
 
 namespace Polynomial
 
@@ -31,7 +31,7 @@ Conclusion "
 
 "
 -/
-Conclusion "Conclusion Saturn L04: coefficients were in `ℕ`. Polynomes with coefficients in `ℕ`
+Conclusion "Conclusion Saturn L05: coefficients were in `ℕ`. Polynomes with coefficients in `ℕ`
 are not considered rings. `ring` does also work on half rings."
 
 NewTactic ring

Game/Levels/Saturn/L05_Ring.lean → Game/Levels/Saturn/L06_Ring.lean

@@ -1,7 +1,7 @@
 import Game.Metadata
 
 World "Saturn"
-Level 5
+Level 6
 
 Introduction "Intro Saturn L05"
 
@@ -31,4 +31,4 @@ Conclusion "
   Nichts wie weg!
 "
 -/
-Conclusion "Conclusion Saturn L05"
+Conclusion "Conclusion Saturn L06"

Game/Levels/Smooth.lean

@@ -0,0 +1,23 @@
+import Game.Levels.Smooth.L01
+import Game.Levels.Smooth.L02
+import Game.Levels.Smooth.L03
+import Game.Levels.Smooth.L04
+import Game.Levels.Smooth.L05
+import Game.Levels.Smooth.L06
+import Game.Levels.Smooth.L07
+import Game.Levels.Smooth.L08
+import Game.Levels.Smooth.L09
+import Game.Levels.Smooth.L10
+
+/-!
+The planet Smooth builds the smooth take-off function `f x = if x ≤ 0 then 0 else
+exp (-x⁻¹)`: from polynomial evaluation and `exp` outgrowing polynomials, through
+the derivative rules (`HasDerivAt.comp`, `.mul`, `.exp`, `hasDerivAt_inv`,
+`hasDerivAt_neg`), up to the key fact that every iterated derivative of `f`
+vanishes at `0` — so `f` is infinitely flat there.
+-/
+
+World "Smooth"
+Title "Smooth"
+
+Introduction "Intro Smooth"

Game/Levels/Smooth/L01.lean

@@ -0,0 +1,21 @@
+import Game.Metadata
+
+World "Smooth"
+Level 1
+
+open Polynomial
+
+Introduction "Intro Smooth L01"
+
+/- Evaluating the polynomial `X ^ 2 + 1` at `2` gives `5`. -/
+Statement : (X ^ 2 + 1 : ℝ[X]).eval 2 = 5 := by
+  Hint "A polynomial is a *formal* expression built from the variable `X : ℝ[X]` and constants.
+  It is not yet a function. To get values you *evaluate* it,
+  and `p.eval a` substitutes `a` for `X`."
+  Hint (hidden := true) "[Hint tkwd] `simp` knows how evaluation interacts with `+`, `^`, `X`
+  and constants."
+  simp
+  Hint (hidden := true) "[Hint smth1tr] Try `ring`."
+  ring
+
+NewDefinition Polynomial Polynomial.X Polynomial.eval

Game/Levels/Smooth/L02.lean

@@ -0,0 +1,39 @@
+import Game.Levels.Smooth.L01
+
+World "Smooth"
+Level 2
+
+open Real Filter Topology Polynomial
+
+Introduction "Intro Smooth L02"
+
+/---/
+TheoremDoc Polynomial.tendsto_div_exp_atTop as "Polynomial.tendsto_div_exp_atTop"
+
+/---/
+TheoremDoc tendsto_sq_div_exp_atTop as "tendsto_sq_div_exp_atTop"
+
+/- The square function divided by the exponential tends to `0` at infinity. -/
+Statement tendsto_sq_div_exp_atTop :
+    Tendsto (fun x : ℝ ↦ x ^ 2 / exp x) atTop (𝓝 0) := by
+  Hint (strict := true) "[Hint 2vkf4]
+    `exp` is the exponential function.
+
+    For any polynomial `p`, the quotient `p(x) / exp x`
+    tends to `0` as `x → ∞`.  This is known as `tendsto_div_exp_atTop`.
+
+    First, establish `x^2 = (X^2).eval x`.
+    "
+  Hint (strict := true) (hidden := true) "[Hint u6qjy] Start with `have`."
+  have h (x : ℝ): x^2 = (X^2).eval x := by
+    Hint (hidden := true) "[Hint z5r1d] This is just `simp`."
+    simp
+  Hint "[Hint r8yz8] Now you want to use `{h}` to rewrite the goal. But `rw` does not work well under
+    quantifiers; `simp_rw` works better."
+  simp_rw [h]
+  Hint (hidden := true) "[Hint ewvsj] Now you can apply `tendsto_div_exp_atTop`."
+  apply tendsto_div_exp_atTop
+
+NewTheorem Polynomial.tendsto_div_exp_atTop
+NewDefinition Real.exp
+NewTactic simp_rw

Game/Levels/Smooth/L03.lean

@@ -0,0 +1,44 @@
+import Game.Levels.Smooth.L02
+
+World "Smooth"
+Level 3
+
+open Real Filter Topology
+
+noncomputable section
+
+Introduction "Intro Smooth L03"
+
+namespace STakeOff
+
+/-- Smooth take-off function -/
+def f : ℝ → ℝ := fun x ↦ if x ≤ 0 then 0 else exp (- x⁻¹)
+
+/-- The smooth take-off function `f x = if x ≤ 0 then 0 else exp (-x⁻¹)`. -/
+DefinitionDoc STakeOff.f as "f"
+
+/-- On the non-positive axis the take-off function vanishes: `f x = 0` when `x ≤ 0`. -/
+TheoremDoc STakeOff.zero_of_nonpos as "zero_of_nonpos"
+
+/- On the non-positive axis the take-off function is `0`. -/
+Statement zero_of_nonpos {x : ℝ} (hx : x ≤ 0) : f x = 0 := by
+  Hint "[Hint smth3f] The *smooth take-off function* `f` is
+    $$
+    f(x) = \\begin\{cases}
+      0 & \\text\{if } x \\le 0, \\\\ %(new line)
+      e^\{-1/x} & \\text\{if } x > 0.
+    \\end\{cases}
+    $$
+    It is flat `0` on the left and rises as `exp (-x⁻¹)` on the right — the seam at `0` is
+    where smoothness is interesting.
+
+    On the left of the seam there is nothing to compute: unfolding f, the
+    assumption `{hx}` picks the first branch of the `if`."
+  Branch
+    unfold f
+    Hint "[Hint smth3ts] Use `{hx}` to simplify the goal."
+    simp [hx]
+  Hint (hidden := true) "[Hint smthts3] `simp [f, {hx}]` unfolds and simplifies in one go."
+  simp [f, hx]
+
+NewDefinition STakeOff.f