From 61d5f39b9c34d04aa8edde0f0d6fba287561d92b Mon Sep 17 00:00:00 2001 From: Rmal <97214596+CoolRmal@users.noreply.github.com> Date: Sun, 4 Jan 2026 21:36:11 -0500 Subject: [PATCH 1/6] Update Basic.lean --- .../Analysis/Asymptotics/Basic.lean | 41 +++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean b/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean index 9c31d6253..5ab05f553 100644 --- a/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean +++ b/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean @@ -16,6 +16,47 @@ limitations under the License. import Mathlib.Analysis.Asymptotics.Defs import Mathlib.Order.Filter.AtTopBot.Defs +import Mathlib.Analysis.SpecialFunctions.Log.Basic +import Mathlib.Analysis.SpecialFunctions.Gamma.Basic + +open scoped Nat notation f " ≫ " g => Asymptotics.IsBigO Filter.atTop g f notation g " ≪ " f => Asymptotics.IsBigO Filter.atTop g f + +/-- The type of common functions used to estimate growth rate. -/ +inductive CommonFn : Type + | const : ℝ → CommonFn + | id : CommonFn + | log : CommonFn + | exp : CommonFn + | Gamma : CommonFn + | add : CommonFn → CommonFn → CommonFn + | mul : CommonFn → CommonFn → CommonFn + | comp : CommonFn → CommonFn → CommonFn + +namespace CommonFn + +/-- The evaluation map of the type of common growth functions. -/ +noncomputable def Real.eval : CommonFn → ℝ → ℝ + | const c => fun _ => c + | id => fun x => x + | log => fun x => x.log + | exp => fun x => x.exp + | Gamma => fun x => x.Gamma + | add f g => fun x => eval f x + eval g x + | mul f g => fun x => eval f x * eval g x + | comp f g => eval f ∘ eval g + +/-- The evaluation map of the type of common growth functions. -/ +noncomputable def Nat.eval : CommonFn → ℕ → ℝ + | const c => fun _ => c + | id => fun x => x + | log => fun x => (x : ℝ).log + | exp => fun x => (x : ℝ).log + | Gamma => fun x => x ! + | add f g => fun x => eval f x + eval g x + | mul f g => fun x => eval f x * eval g x + | comp f g => Real.eval f ∘ eval g + +end CommonFn From bf3e1eab126fa69e299569d15aca97d6b738efd0 Mon Sep 17 00:00:00 2001 From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com> Date: Mon, 5 Jan 2026 15:35:41 -0500 Subject: [PATCH 2/6] Update FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean b/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean index 5ab05f553..a9254e4ad 100644 --- a/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean +++ b/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean @@ -25,7 +25,7 @@ notation f " ≫ " g => Asymptotics.IsBigO Filter.atTop g f notation g " ≪ " f => Asymptotics.IsBigO Filter.atTop g f /-- The type of common functions used to estimate growth rate. -/ -inductive CommonFn : Type +inductive ElementaryGrowth : Type | const : ℝ → CommonFn | id : CommonFn | log : CommonFn From 08726aad88a9efa2b7ac848df17c039d90fb9343 Mon Sep 17 00:00:00 2001 From: Rmal <97214596+CoolRmal@users.noreply.github.com> Date: Mon, 5 Jan 2026 15:37:58 -0500 Subject: [PATCH 3/6] Update Basic.lean --- .../ForMathlib/Analysis/Asymptotics/Basic.lean | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean b/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean index 5ab05f553..501ffc056 100644 --- a/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean +++ b/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean @@ -30,7 +30,6 @@ inductive CommonFn : Type | id : CommonFn | log : CommonFn | exp : CommonFn - | Gamma : CommonFn | add : CommonFn → CommonFn → CommonFn | mul : CommonFn → CommonFn → CommonFn | comp : CommonFn → CommonFn → CommonFn @@ -43,20 +42,8 @@ noncomputable def Real.eval : CommonFn → ℝ → ℝ | id => fun x => x | log => fun x => x.log | exp => fun x => x.exp - | Gamma => fun x => x.Gamma | add f g => fun x => eval f x + eval g x | mul f g => fun x => eval f x * eval g x | comp f g => eval f ∘ eval g -/-- The evaluation map of the type of common growth functions. -/ -noncomputable def Nat.eval : CommonFn → ℕ → ℝ - | const c => fun _ => c - | id => fun x => x - | log => fun x => (x : ℝ).log - | exp => fun x => (x : ℝ).log - | Gamma => fun x => x ! - | add f g => fun x => eval f x + eval g x - | mul f g => fun x => eval f x * eval g x - | comp f g => Real.eval f ∘ eval g - end CommonFn From a5d0e7220b3c0d1ce1bd45be132a83f8a7e2938a Mon Sep 17 00:00:00 2001 From: Rmal <97214596+CoolRmal@users.noreply.github.com> Date: Mon, 5 Jan 2026 15:38:31 -0500 Subject: [PATCH 4/6] Update Basic.lean --- .../Analysis/Asymptotics/Basic.lean | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean b/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean index 8aa85b708..980524eda 100644 --- a/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean +++ b/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean @@ -26,18 +26,18 @@ notation g " ≪ " f => Asymptotics.IsBigO Filter.atTop g f /-- The type of common functions used to estimate growth rate. -/ inductive ElementaryGrowth : Type - | const : ℝ → CommonFn - | id : CommonFn - | log : CommonFn - | exp : CommonFn - | add : CommonFn → CommonFn → CommonFn - | mul : CommonFn → CommonFn → CommonFn - | comp : CommonFn → CommonFn → CommonFn + | const : ℝ → ElementaryGrowth + | id : ElementaryGrowth + | log : ElementaryGrowth + | exp : ElementaryGrowth + | add : ElementaryGrowth → ElementaryGrowth → ElementaryGrowth + | mul : ElementaryGrowth → ElementaryGrowth → ElementaryGrowth + | comp : ElementaryGrowth → ElementaryGrowth → ElementaryGrowth -namespace CommonFn +namespace ElementaryGrowth /-- The evaluation map of the type of common growth functions. -/ -noncomputable def Real.eval : CommonFn → ℝ → ℝ +noncomputable def Real.eval : ElementaryGrowth → ℝ → ℝ | const c => fun _ => c | id => fun x => x | log => fun x => x.log @@ -46,4 +46,4 @@ noncomputable def Real.eval : CommonFn → ℝ → ℝ | mul f g => fun x => eval f x * eval g x | comp f g => eval f ∘ eval g -end CommonFn +end ElementaryGrowth From a704a0f898a9de5539a113d3084342f4501a40c8 Mon Sep 17 00:00:00 2001 From: Rmal <97214596+CoolRmal@users.noreply.github.com> Date: Mon, 5 Jan 2026 16:32:15 -0500 Subject: [PATCH 5/6] Update Basic.lean --- .../Analysis/Asymptotics/Basic.lean | 29 ++++++++++++++----- 1 file changed, 21 insertions(+), 8 deletions(-) diff --git a/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean b/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean index 980524eda..0f6960192 100644 --- a/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean +++ b/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean @@ -17,9 +17,9 @@ limitations under the License. import Mathlib.Analysis.Asymptotics.Defs import Mathlib.Order.Filter.AtTopBot.Defs import Mathlib.Analysis.SpecialFunctions.Log.Basic -import Mathlib.Analysis.SpecialFunctions.Gamma.Basic open scoped Nat +open Filter notation f " ≫ " g => Asymptotics.IsBigO Filter.atTop g f notation g " ≪ " f => Asymptotics.IsBigO Filter.atTop g f @@ -30,20 +30,33 @@ inductive ElementaryGrowth : Type | id : ElementaryGrowth | log : ElementaryGrowth | exp : ElementaryGrowth + | atTop : (f : ℝ → ℝ) → (Tendsto f atTop atTop) → ElementaryGrowth | add : ElementaryGrowth → ElementaryGrowth → ElementaryGrowth | mul : ElementaryGrowth → ElementaryGrowth → ElementaryGrowth | comp : ElementaryGrowth → ElementaryGrowth → ElementaryGrowth namespace ElementaryGrowth +def neg : ElementaryGrowth → ElementaryGrowth := fun f => mul (const (-1)) f + +def sub : ElementaryGrowth → ElementaryGrowth → ElementaryGrowth := fun f g => add f (neg g) + +def pow : ElementaryGrowth → ElementaryGrowth → ElementaryGrowth := + fun f g => comp exp (mul g (comp log f)) + +def inv : ElementaryGrowth → ElementaryGrowth := fun f => pow f (const (-1)) + +def div : ElementaryGrowth → ElementaryGrowth → ElementaryGrowth := fun f g => mul f (inv g) + /-- The evaluation map of the type of common growth functions. -/ noncomputable def Real.eval : ElementaryGrowth → ℝ → ℝ - | const c => fun _ => c - | id => fun x => x - | log => fun x => x.log - | exp => fun x => x.exp - | add f g => fun x => eval f x + eval g x - | mul f g => fun x => eval f x * eval g x - | comp f g => eval f ∘ eval g + | const c => fun _ => c + | id => fun x => x + | log => fun x => x.log + | exp => fun x => x.exp + | atTop f _ => f + | add f g => fun x => eval f x + eval g x + | mul f g => fun x => eval f x * eval g x + | comp f g => eval f ∘ eval g end ElementaryGrowth From 3b91a444e99e0ce1bbe1e8ed7e0cd9e56313ea05 Mon Sep 17 00:00:00 2001 From: Rmal <97214596+CoolRmal@users.noreply.github.com> Date: Mon, 5 Jan 2026 17:00:33 -0500 Subject: [PATCH 6/6] Update Basic.lean --- FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean b/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean index 0f6960192..e57788293 100644 --- a/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean +++ b/FormalConjectures/ForMathlib/Analysis/Asymptotics/Basic.lean @@ -18,7 +18,6 @@ import Mathlib.Analysis.Asymptotics.Defs import Mathlib.Order.Filter.AtTopBot.Defs import Mathlib.Analysis.SpecialFunctions.Log.Basic -open scoped Nat open Filter notation f " ≫ " g => Asymptotics.IsBigO Filter.atTop g f