From ea169e4c3eb63e955200501c805d28932c99a537 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 15 Sep 2025 14:41:27 +0200
Subject: [PATCH] Initial checkout

---
 ColloquiumLean.lean                          |  2 +-
 ColloquiumLean/Basic.lean                    |  1 -
 ColloquiumLean/ContinuousLimit.lean          | 22 +++++++++++
 ColloquiumLean/ContinuousLimitSolution.lean  | 35 ++++++++++++++++++
 ColloquiumLean/ContinuousSquare.lean         | 35 ++++++++++++++++++
 ColloquiumLean/ContinuousSquareSolution.lean | 39 ++++++++++++++++++++
 6 files changed, 132 insertions(+), 2 deletions(-)
 delete mode 100644 ColloquiumLean/Basic.lean
 create mode 100644 ColloquiumLean/ContinuousLimit.lean
 create mode 100644 ColloquiumLean/ContinuousLimitSolution.lean
 create mode 100644 ColloquiumLean/ContinuousSquare.lean
 create mode 100644 ColloquiumLean/ContinuousSquareSolution.lean

diff --git a/ColloquiumLean.lean b/ColloquiumLean.lean
index a7d7d34..99e27c6 100644
--- a/ColloquiumLean.lean
+++ b/ColloquiumLean.lean
@@ -1 +1 @@
-import ColloquiumLean.Basic
+import ColloquiumLean.ContinuousLimitSolution
diff --git a/ColloquiumLean/Basic.lean b/ColloquiumLean/Basic.lean
deleted file mode 100644
index 99415d9..0000000
--- a/ColloquiumLean/Basic.lean
+++ /dev/null
@@ -1 +0,0 @@
-def hello := "world"
diff --git a/ColloquiumLean/ContinuousLimit.lean b/ColloquiumLean/ContinuousLimit.lean
new file mode 100644
index 0000000..fccfbb5
--- /dev/null
+++ b/ColloquiumLean/ContinuousLimit.lean
@@ -0,0 +1,22 @@
+import Mathlib
+
+open Real
+
+-- Definition: Function (f : ℝ → ℝ) is continuous at (x₀ : ℝ)
+def continuous_at (f : ℝ → ℝ) (x₀ : ℝ) :=
+  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| < δ → |f x - f x₀| < ε
+
+-- Definition: Sequence (u : ℕ → ℝ) converges to limit (l : ℝ)
+def seq_limit (u : ℕ → ℝ) (l : ℝ) :=
+  ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε
+
+
+-- In the following, f is a function, u is a sequence, and x₀ a real number
+variable
+  {f : ℝ → ℝ} {u : ℕ → ℝ} {x₀ : ℝ}
+
+
+lemma continuity_and_limits
+  (hyp_f : continuous_at f x₀) (hyp_u : seq_limit u x₀) :
+    seq_limit (f ∘ u) (f x₀) := by
+  sorry
diff --git a/ColloquiumLean/ContinuousLimitSolution.lean b/ColloquiumLean/ContinuousLimitSolution.lean
new file mode 100644
index 0000000..8bc73a3
--- /dev/null
+++ b/ColloquiumLean/ContinuousLimitSolution.lean
@@ -0,0 +1,35 @@
+-- Library Import: Basic facts about real numbers
+import Mathlib.Data.Real.Basic
+open Real
+
+-- Definition: Function (f : ℝ → ℝ) is continuous at (x₀ : ℝ)
+def continuous (f : ℝ → ℝ) (x₀ : ℝ) :=
+  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| < δ → |f x - f x₀| < ε
+
+-- Definition: Sequence (u : ℕ → ℝ) converges to limit (l : ℝ)
+def limit (u : ℕ → ℝ) (l : ℝ) :=
+  ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε
+
+-- In the following, f is a function, u is a sequence, and x₀ a real number
+variable {f : ℝ → ℝ} {u : ℕ → ℝ} {x₀ : ℝ}
+
+-- Theorem: If f is continuous at x₀ and the sequence u converges to x₀, then
+-- the sequence f ∘ u converges to f x₀.
+theorem continuity_and_limits
+  (hyp_f : continuous f x₀) (hyp_u : limit u x₀) :
+    limit (f ∘ u) (f x₀) := by
+
+  unfold limit at *
+  unfold continuous at *
+
+  intro ε hε
+
+  obtain ⟨δ, h₁δ, h₂δ⟩ := hyp_f ε hε
+
+  obtain ⟨N, hN⟩ := hyp_u δ h₁δ
+
+  use N
+  intro n hn
+  apply h₂δ
+  apply hN
+  exact hn
diff --git a/ColloquiumLean/ContinuousSquare.lean b/ColloquiumLean/ContinuousSquare.lean
new file mode 100644
index 0000000..1c8d1b1
--- /dev/null
+++ b/ColloquiumLean/ContinuousSquare.lean
@@ -0,0 +1,35 @@
+import Mathlib
+
+open Real
+
+variable
+  {x : ℝ} {y : ℝ}
+
+-- Definition: Function (f : ℝ → ℝ) is continuous at (x₀ : ℝ)
+def continuous_at (f : ℝ → ℝ) (x₀ : ℝ) :=
+  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| < δ → |f x - f x₀| < ε
+
+-- Three lemmas from the lean mathematical library
+example : 0 < x  →  0 < √x := sqrt_pos.2
+
+example : x ^ 2 < y  ↔  (-√y < x) ∧ (x < √y) := sq_lt
+
+example : |x| < y  ↔  -y < x ∧ x < y := abs_lt
+
+-- The square function
+def squareFct : ℝ → ℝ := fun x ↦ x ^ 2
+
+
+theorem continuous_at_squareFct :
+    continuous_at squareFct 0 := by
+  unfold continuous_at
+  intro e he
+  use √e
+  constructor
+  · apply sqrt_pos.2
+    exact he
+  · intro x hx
+    simp_all [squareFct]
+    apply sq_lt.2
+    apply abs_lt.1
+    exact hx
diff --git a/ColloquiumLean/ContinuousSquareSolution.lean b/ColloquiumLean/ContinuousSquareSolution.lean
new file mode 100644
index 0000000..3f6ad00
--- /dev/null
+++ b/ColloquiumLean/ContinuousSquareSolution.lean
@@ -0,0 +1,39 @@
+-- Library Import: Basic facts about real numbers and the root function
+import Mathlib.Data.Real.Sqrt
+open Real
+
+-- In the following, x and y are real numbers
+variable {x : ℝ} {y : ℝ}
+
+-- Definition: Function (f : ℝ → ℝ) is continuous at (x₀ : ℝ)
+def continuous (f : ℝ → ℝ) (x₀ : ℝ) :=
+  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| < δ → |f x - f x₀| < ε
+
+-- Definition: The square function
+def squareFct : ℝ → ℝ := fun x ↦ x ^ 2
+
+
+-- Reminder: Three facts from the library that we will use.
+example : 0 < x → 0 < √x := sqrt_pos.2
+
+example : x ^ 2 < y  ↔  (-√y < x) ∧ (x < √y) := sq_lt
+
+example : |x| < y  ↔  -y < x ∧ x < y := abs_lt
+
+
+-- Theorem: The square function is continuous at x₀ = 0
+theorem ContinuousAt_sq :
+    continuous squareFct 0 := by
+
+  unfold continuous
+
+  intro ε hε
+  use √ε
+
+  constructor
+  · apply sqrt_pos.2
+    exact hε
+  · intro x hx
+    simp_all [squareFct]
+    apply sq_lt.2
+    exact abs_lt.1 hx