feat: functions of elementary growth #1481
Conversation
By Stirling's formula, this is unnecessary |
| /-- 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 |
There was a problem hiding this comment.
I am rather sure you will need to allow functions tending to zero or infinity, so that we can state things like ~ x ^(1 + o(1)) or >> x log x beta(x) where beta -> infty (one Erdos problem has partial progress of this form where beta is reverse Ackermann)
YaelDillies
added
the
awaiting-author
Co-authored-by: Yaël Dillies <[email protected]>
…al/formal-conjectures into CommonGrowthRateFunctions
YaelDillies
changed the title
|
@YaelDillies I think I get the idea but I am not sure how to realize this in Lean. What is the type of this elaborator? Do I need some knowledge in metaprogramming in order to define this? |
|
Indeed, this would be metaprogramming. What you need to do is basically to follow this section of MetIL and possibly this one too. |
Closes #389 Some remarks: 1. In the paper [ESS94] On Sum Sets of Sidon Sets, the authors formulate this conjecture by using limit, which will be equivalent to the formulation on the website. The limit formulation is easier to formalize and this is why I defined the function `f`. This definition of `f` also makes it easier to talk about the growth rate. 2. For the conjecture related to infinite Sidon sets, one needs the results in the PR #1481, so I left it as a TODO. <img width="1052" height="413" alt="Screenshot 2026-01-06 at 1 40 26 AM" src="https://github.com/user-attachments/assets/28b211a9-0c66-4089-972e-a722939ffc45" /> --------- Co-authored-by: Moritz Firsching <[email protected]>
Closes google-deepmind#389 Some remarks: 1. In the paper [ESS94] On Sum Sets of Sidon Sets, the authors formulate this conjecture by using limit, which will be equivalent to the formulation on the website. The limit formulation is easier to formalize and this is why I defined the function `f`. This definition of `f` also makes it easier to talk about the growth rate. 2. For the conjecture related to infinite Sidon sets, one needs the results in the PR google-deepmind#1481, so I left it as a TODO. <img width="1052" height="413" alt="Screenshot 2026-01-06 at 1 40 26 AM" src="https://github.com/user-attachments/assets/28b211a9-0c66-4089-972e-a722939ffc45" /> --------- Co-authored-by: Moritz Firsching <[email protected]>
|
I guess by the same token that Gamma is definable in terms of the other growth rates via Stirling's formula, addition is definable in terms of exp, mul, and log. Perhaps that's a change worth making? |
|
|
||
| notation f " ≫ " g => Asymptotics.IsBigO Filter.atTop g f | ||
| notation g " ≪ " f => Asymptotics.IsBigO Filter.atTop g f | ||
|
|
There was a problem hiding this comment.
I think it might be better to include this code in a file ../Asymptotics/ElementaryGrowth.lean since I suspect more content will be added to it after! It would also be useful to add a module docstring to the file documenting what you've added, and the intended use (perhaps with some examples!).
4 participants
This PR intends to define the type of common functions used to estimate growth rate so that for example we can formalize a better statement in #1476 and potentially other Erdos problems.
I only include constants, identity function, log, exp, gamma (factorial), addition, multiplication, and composition because
a^x = exp x * (log a)x^a = exp a * (log x)x^x = exp x * (log x)f/g = exp (log f - log g)This should include most of functions we are interested in.
I also only defined evaluation map for
ℝ → ℝandℕ → ℝinstead of functions with more general domain/codomain because I think these are enough for Erdos problems.