From a7344b4151e5bea7f2d9154f8011dcd426413db3 Mon Sep 17 00:00:00 2001
From: Eric <eric.1334@icloud.com>
Date: Mon, 16 Dec 2024 15:24:36 -0800
Subject: [PATCH] Move convergence file

---
 OrderedSemigroups/OrderedGroup/Approximate.lean       |  2 +-
 OrderedSemigroups/{ => OrderedGroup}/Convergence.lean | 10 ++++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)
 rename OrderedSemigroups/{ => OrderedGroup}/Convergence.lean (96%)

diff --git a/OrderedSemigroups/OrderedGroup/Approximate.lean b/OrderedSemigroups/OrderedGroup/Approximate.lean
index f49ffa8..1e73925 100644
--- a/OrderedSemigroups/OrderedGroup/Approximate.lean
+++ b/OrderedSemigroups/OrderedGroup/Approximate.lean
@@ -1,5 +1,5 @@
 import OrderedSemigroups.OrderedGroup.ArchimedeanGroup
-import OrderedSemigroups.Convergence
+import OrderedSemigroups.OrderedGroup.Convergence
 import OrderedSemigroups.Basic
 
 /-!
diff --git a/OrderedSemigroups/Convergence.lean b/OrderedSemigroups/OrderedGroup/Convergence.lean
similarity index 96%
rename from OrderedSemigroups/Convergence.lean
rename to OrderedSemigroups/OrderedGroup/Convergence.lean
index 014fdbf..0e63e84 100644
--- a/OrderedSemigroups/Convergence.lean
+++ b/OrderedSemigroups/OrderedGroup/Convergence.lean
@@ -1,5 +1,15 @@
 import Mathlib.Analysis.Normed.Order.Lattice
 
+/-!
+# Convergence of a particular sequence
+
+This file proves that sequences satisfying a particular condition converge.
+This is used in the proof of Holder's theorem to show that the
+sequence of approximations do converge.
+
+-/
+
+
 open Filter
 
 lemma arch_nat {e C : ℝ} (C_pos : C > 0) (e_pos : e > 0) : ∃n : ℕ+, 1 / n < e/(2*C) := by