Move convergence file

ericluap · Dec 16, 2024 · a7344b4 · a7344b4
1 parent 67bf94e
commit a7344b4
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 1 deletion.
diff --git 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 → ...dSemigroups/OrderedGroup/Convergence.lean b/OrderedSemigroups/Convergence.lean → ...dSemigroups/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