diff --git a/Cslib.lean b/Cslib.lean
index 5cfc781da..5b0c8b3fd 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -5,6 +5,7 @@ public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.Sort.Insertion
 public import Cslib.Algorithms.Lean.Sort.Merge
 public import Cslib.Algorithms.Lean.TimeM
+public import Cslib.Algorithms.Lean.TimeM.Asymptotics
 public import Cslib.Algorithms.StatefulProcesses.DiffieHellman.Basic
 public import Cslib.Computability.Automata.Acceptors.Acceptor
 public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
diff --git a/Cslib/Algorithms/Lean/TimeM/Asymptotics.lean b/Cslib/Algorithms/Lean/TimeM/Asymptotics.lean
new file mode 100644
index 000000000..fe9928cad
--- /dev/null
+++ b/Cslib/Algorithms/Lean/TimeM/Asymptotics.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2026 Christian Battaglia. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Battaglia
+-/
+module
+
+public import Cslib.Init
+public import Cslib.Algorithms.Lean.TimeM
+public import Mathlib.Analysis.Asymptotics.Defs
+public import Mathlib.Order.Filter.AtTopBot.Defs
+
+/-!
+# Asymptotic bounds for `TimeM` costs
+
+Mathlib's `Asymptotics.IsBigO` and `Asymptotics.IsTheta` compare two functions along a filter.
+`TimeM.time` is a single cost. These definitions lift a size-indexed computation to that API.
+-/
+
+@[expose] public section
+
+open Asymptotics Filter
+
+namespace Cslib.Algorithms.Lean.TimeM
+
+/-- The cost of `cost`, as a function of input size, is big-O of `g` at infinity. -/
+def isBigO {α T : Type*} [Coe T ℝ] (cost : ℕ → TimeM T α) (g : ℕ → ℝ) : Prop :=
+  IsBigO atTop (fun n => ((cost n).time : ℝ)) g
+
+/-- The cost of `cost`, as a function of input size, is big-Theta of `g` at infinity. -/
+def isTheta {α T : Type*} [Coe T ℝ] (cost : ℕ → TimeM T α) (g : ℕ → ℝ) : Prop :=
+  IsTheta atTop (fun n => ((cost n).time : ℝ)) g
+
+end Cslib.Algorithms.Lean.TimeM