Use of embedded Landau notation

Stream: maths

[Salvatore Mercuri]

Currently in mathlib the Asymptotics library provides Landau notation of the following form f =O[l] g to express that $f = O(g)$ (along the filter l) and similarly for little-o, big theta, etc. 

In Formal Conjectures we often face statements such as the unit distance problem, where the big O appears embedded somewhere within the right-hand expression ($n^{1 + O(1/\log\log n)}$ in this example). AFAIK the current mathlib notation does not allow for big O to be embedded in the RHS like this. To get around this, we often employ the following pattern. To express something like $f$ is $n ^ {1 + O(g)}$:

∃ (e : ℕ → ℝ) (he : e =O[atTop] g),
  f =ᶠ[atTop] fun n ↦ n ^ (1 + e n)

See the formal conjectures repo for the unit distance example.

1. Is this existential pattern the canonical way to express these problems currently?
2. Or would it be better to normalise the RHS to be of the form $f = O(g)$ and use the standard Landau notation?
3. Any other suggestions on best practices here would be very welcome!

[Yaël Dillies]

Have you seen FC#1481? This might be a solution to this problem

[Yongxi Lin (Aaron)]

I do believe the existential pattern fully conveys the idea behind the notation $n^{1 + O(g)}$ and maybe you can even just write f = fun n ↦ n ^ (1 + e n) as he has already gave you the information about the tail behavior.

Also if somebody want to work on FC#1481, feel free to do so... I need to start to learn some metaprogramming before I can really finish that PR :melting_face:

[Yuval Filmus]

This is how I view asymptotic notation, and these are used a lot in the areas I am active in (combinatorics and US-style theoretical computer science).

As an aside, sometimes it is convenient to have big O notation apply for all inputs, or (in the case of natural numbers) for all positive inputs. Presumably this is supported by the current formalism.

Finally, sometimes one is interested in the value of the constants.
For example, Ramsey's theorem implies that every 2-coloring of a graph on _n_ vertices induces a monochromatic clique of size Ω(log _n_).
The standard inductive proof gives one constant, but this was recently improved.
The optimal constant isn't known.
How does one express all this information in Mathlib?

More generally, what should be done when some result is known with sub-optimal quantitative dependence, but is still useful?

[Yury G. Kudryashov]

We have docs#Asymptotics.IsBigOWith for explicit estimates.

[Yury G. Kudryashov]

You can prove it, then deduce IsBigO in 1 line.

[Yury G. Kudryashov]

Also, if there is a trade-off between "better constant" vs "maximal n that breaks the estimate" and you want to preserve this information, then you can formulate a theorem like exists_isClique_mul_log_le_card_of_le_card

[Yury G. Kudryashov]

More generally, we definitely accept results that can be improved/generalized in the future.

[Yury G. Kudryashov]

If someone formalizes a better version in the future, then they can replace what's currently in the library (with some deprecation period).

[Eric Wieser]

Yaël Dillies said:

Have you seen FC#1481? This might be a solution to this problem

Could you elaborate on this inline?

[Eric Wieser]

As a concrete action here; should we include @Salvatore Mercuri's example in the module docs for Landau notation?

[Bhavik Mehta]

I would say the existential pattern is the best way, I've been using it since the unit-fractions project and also heavily in the exponential ramsey project and it works excellently. I've always viewed it as the obvious canonical choice, but I agree we should document it.