chore: split Mathlib.Analysis.Asymptotics.Asymptotics (#20785)

This was a long file. Co-authored-by: Michael Rothgang <[email protected]>
leanprover-community · Jan 18, 2025 · 95878d0 · 95878d0
1 parent af5ebc2
commit 95878d0
Show file tree

Hide file tree

Showing 13 changed files with 799 additions and 769 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1123,7 +1123,8 @@ import Mathlib.Analysis.Analytic.RadiusLiminf
 import Mathlib.Analysis.Analytic.Uniqueness
 import Mathlib.Analysis.Analytic.Within
 import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
-import Mathlib.Analysis.Asymptotics.Asymptotics
+import Mathlib.Analysis.Asymptotics.Defs
+import Mathlib.Analysis.Asymptotics.Lemmas
 import Mathlib.Analysis.Asymptotics.SpecificAsymptotics
 import Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
 import Mathlib.Analysis.Asymptotics.TVS

diff --git a/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean b/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
-import Mathlib.Analysis.Asymptotics.Asymptotics
+import Mathlib.Analysis.Asymptotics.Lemmas
 import Mathlib.Analysis.Asymptotics.Theta
 import Mathlib.Analysis.Normed.Order.Basic
 

diff --git a/...lib/Analysis/Asymptotics/Asymptotics.lean → Mathlib/Analysis/Asymptotics/Defs.lean b/...lib/Analysis/Asymptotics/Asymptotics.lean → Mathlib/Analysis/Asymptotics/Defs.lean
diff --git a/Mathlib/Analysis/Asymptotics/Lemmas.lean b/Mathlib/Analysis/Asymptotics/Lemmas.lean
diff --git a/Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean b/Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
 import Mathlib.Analysis.Normed.Order.Basic
-import Mathlib.Analysis.Asymptotics.Asymptotics
+import Mathlib.Analysis.Asymptotics.Lemmas
 import Mathlib.Analysis.Normed.Module.Basic
 
 /-!

diff --git a/Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean b/Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Devon Tuma
 -/
 import Mathlib.Algebra.Polynomial.Eval.Defs
-import Mathlib.Analysis.Asymptotics.Asymptotics
+import Mathlib.Analysis.Asymptotics.Lemmas
 import Mathlib.Analysis.Normed.Order.Basic
 import Mathlib.Topology.Algebra.Order.LiminfLimsup
 

diff --git a/Mathlib/Analysis/Asymptotics/TVS.lean b/Mathlib/Analysis/Asymptotics/TVS.lean
@@ -3,12 +3,12 @@ Copyright (c) 2023 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Eric Wieser
 -/
-import Mathlib.Analysis.Asymptotics.Asymptotics
 import Mathlib.Analysis.Convex.EGauge
 import Mathlib.Analysis.LocallyConvex.BalancedCoreHull
 import Mathlib.Analysis.Seminorm
 import Mathlib.Tactic.Peel
 import Mathlib.Topology.Instances.ENNReal.Lemmas
+import Mathlib.Analysis.Asymptotics.Defs
 
 /-!
 # Asymptotics in a Topological Vector Space

diff --git a/Mathlib/Analysis/Asymptotics/Theta.lean b/Mathlib/Analysis/Asymptotics/Theta.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Analysis.Asymptotics.Asymptotics
+import Mathlib.Analysis.Asymptotics.Lemmas
 import Mathlib.Analysis.Normed.Module.Basic
 
 /-!

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean
@@ -6,6 +6,7 @@ Authors: Jeremy Avigad, Sébastien Gouëzel, Yury Kudryashov
 import Mathlib.Analysis.Calculus.TangentCone
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics
 import Mathlib.Analysis.Asymptotics.TVS
+import Mathlib.Analysis.Asymptotics.Lemmas
 
 /-!
 # The Fréchet derivative

diff --git a/Mathlib/Analysis/Normed/Group/InfiniteSum.lean b/Mathlib/Analysis/Normed/Group/InfiniteSum.lean
@@ -28,7 +28,6 @@ In a complete (semi)normed group,
 infinite series, absolute convergence, normed group
 -/
 
-
 open Topology NNReal
 
 open Finset Filter Metric

diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/Asymptotics.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/Asymptotics.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo
 -/
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic
-import Mathlib.Analysis.Asymptotics.Asymptotics
+import Mathlib.Analysis.Asymptotics.Defs
 /-!
 # Asymptotic statements about the operator norm
 

diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean
@@ -6,7 +6,7 @@ Authors: Anatole Dedecker, Sébastien Gouëzel, Yury Kudryashov, Dylan MacKenzie
 import Mathlib.Algebra.BigOperators.Module
 import Mathlib.Algebra.Order.Field.Power
 import Mathlib.Algebra.Polynomial.Monic
-import Mathlib.Analysis.Asymptotics.Asymptotics
+import Mathlib.Analysis.Asymptotics.Lemmas
 import Mathlib.Analysis.Normed.Field.InfiniteSum
 import Mathlib.Analysis.Normed.Module.Basic
 import Mathlib.Analysis.SpecificLimits.Basic

diff --git a/Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean b/Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Birkbeck, David Loeffler
 -/
 import Mathlib.Algebra.Module.Submodule.Basic
-import Mathlib.Analysis.Asymptotics.Asymptotics
+import Mathlib.Analysis.Asymptotics.Lemmas
 import Mathlib.Algebra.Algebra.Pi
 
 /-!
-Original file line number
+Diff line change
@@ Expand Up / @@ -28,7 +28,6 @@ In a complete (semi)normed group, @@
     infinite series, absolute convergence, normed group
     -/
     open Topology NNReal
     open Finset Filter Metric
@@ Expand Down @@