From 2e6208198643e3bd91f42802c84fa71b6e49f030 Mon Sep 17 00:00:00 2001
From: Shaunticlair <66981420+Shaunticlair@users.noreply.github.com>
Date: Fri, 27 Mar 2026 04:54:49 -0400
Subject: [PATCH 1/3] Fix upperseq definition in Example_6_4_9

This minus sign shouldn't be here, I don't think. 1. it would better mirror lowerseq 2. the largest term should always be the next positive one.
---
 analysis/Analysis/Section_6_4.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/analysis/Analysis/Section_6_4.lean b/analysis/Analysis/Section_6_4.lean
index 6bcaa8bc..73f8f3a6 100644
--- a/analysis/Analysis/Section_6_4.lean
+++ b/analysis/Analysis/Section_6_4.lean
@@ -119,7 +119,7 @@ example : Example_6_4_8.liminf = ⊥ := by sorry
 noncomputable abbrev Example_6_4_9 : Sequence :=
   (fun (n:ℕ) ↦ if Even n then (n+1:ℝ)⁻¹ else -(n+1:ℝ)⁻¹)
 
-example (n:ℕ) : Example_6_4_9.upperseq n = if Even n then (n+1:ℝ)⁻¹ else -(n+2:ℝ)⁻¹ := by sorry
+example (n:ℕ) : Example_6_4_9.upperseq n = if Even n then (n+1:ℝ)⁻¹ else (n+2:ℝ)⁻¹ := by sorry
 
 example : Example_6_4_9.limsup = 0 := by sorry
 

From 8b6261b6b2aa0893d3d390c26c654a843ec5d334 Mon Sep 17 00:00:00 2001
From: Shaunticlair <66981420+Shaunticlair@users.noreply.github.com>
Date: Fri, 27 Mar 2026 06:49:32 -0400
Subject: [PATCH 2/3] Update example limsup reference in Section 6.4

Example_6_4_9.limsup showed up twice previously, the second instance looked like it should contextually be Example_6_4_10.limsup
---
 analysis/Analysis/Section_6_4.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/analysis/Analysis/Section_6_4.lean b/analysis/Analysis/Section_6_4.lean
index 73f8f3a6..660fad43 100644
--- a/analysis/Analysis/Section_6_4.lean
+++ b/analysis/Analysis/Section_6_4.lean
@@ -131,7 +131,7 @@ noncomputable abbrev Example_6_4_10 : Sequence := (fun (n:ℕ) ↦ (n+1:ℝ))
 
 example (n:ℕ) : Example_6_4_10.upperseq n = ⊤ := by sorry
 
-example : Example_6_4_9.limsup = ⊤ := by sorry
+example : Example_6_4_10.limsup = ⊤ := by sorry
 
 example (n:ℕ) : Example_6_4_9.lowerseq n = n+1 := by sorry
 

From 7975da7a4a99d5f0c9398e5d440cdd977b1fc0fa Mon Sep 17 00:00:00 2001
From: Shaunticlair <66981420+Shaunticlair@users.noreply.github.com>
Date: Fri, 27 Mar 2026 06:59:42 -0400
Subject: [PATCH 3/3] Additional Ex numbering fixes

---
 analysis/Analysis/Section_6_4.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/analysis/Analysis/Section_6_4.lean b/analysis/Analysis/Section_6_4.lean
index 660fad43..f26b1867 100644
--- a/analysis/Analysis/Section_6_4.lean
+++ b/analysis/Analysis/Section_6_4.lean
@@ -133,9 +133,9 @@ example (n:ℕ) : Example_6_4_10.upperseq n = ⊤ := by sorry
 
 example : Example_6_4_10.limsup = ⊤ := by sorry
 
-example (n:ℕ) : Example_6_4_9.lowerseq n = n+1 := by sorry
+example (n:ℕ) : Example_6_4_10.lowerseq n = n+1 := by sorry
 
-example : Example_6_4_9.liminf = ⊤ := by sorry
+example : Example_6_4_10.liminf = ⊤ := by sorry
 
 /-- Proposition 6.4.12(a) -/
 theorem Sequence.gt_limsup_bounds {a:Sequence} {x:EReal} (h: x > a.limsup) :