Infix notation for `is_O`/`is_o`

Stream: maths

[Yury G. Kudryashov]

Hi,

In #14129 I reorder arguments of is_O/is_o and various trans lemmas so that they work with calc. I use notation f =O[l] g and f =o[l] g. @Eric Wieser doesn't like the idea of using = in the notation of a non-symmetric relation. Any other ideas? I need infix notation for (at least) $f=O(g)$, $f=o(g)$, $f=\Theta(g)$ (not yet in mathlib).

[Violeta Hernández]

I do like the current notation, it matches mathematical usage.

[Kyle Miller]

I think = is fine due to convention, but just to through out an alternative, it could be f ∈O[l] g.

[Violeta Hernández]

Oh, that actually works perfectly

[Violeta Hernández]

I like it even more if I'm being honest

[Reid Barton]

I think =O[l] is better; ∈O[l] doesn't read right in the context of transitivity/calc, besides being nonstandard

[Eric Rodriguez]

\mem is already supported in calc. Also \subset(eq), which leads to some ridiculous looking proofs

[Reid Barton]

I mean =O[l] is transitive, like =. $\in$ is not transitive.

[Yaël Dillies]

Isn't is_o short enough to not warrant a notation?

[Kyle Miller]

I've seen $f \in O(g)$ in the wild, though as a transitive relation it's nonstandard. Arguably this is using ∈ closer to Peano's original definition of the notation, which means "is" (it's a stylized version of the first letter of the Greek word for the Latin word "est").

[Reid Barton]

Yaël Dillies said:

Isn't is_o short enough to not warrant a notation?

Sure, but for calc an infix form would be nice (required?)

[Kyle Miller]

(Small note regarding calc and this: there's still a bug in calc still where it'll completely ignore whatever you put in the square brackets since it only unifies the last two arguments for the relation. Hopefully that will be fixed eventually...)

[Eric Rodriguez]

Reid Barton said:

Yaël Dillies said:

Isn't is_o short enough to not warrant a notation?

Sure, but for calc an infix form would be nice (required?)

I've tried many things and I think it is required.

[Vincent Beffara]

How about ≤O[l] or ≼O[l] or just ≼[l]? It is not mathematically correct and goes against my conditioning of never having both an inequality and a big-O in the same formula, but at least it feels transitive and not symmetric.

[Kevin Buzzard]

I guess it's pretty easy to guess what f <= O(g) means. I suppose you could even write f <= C*g!

[Vincent Beffara]

Yes, it is clear what f ≤ O(g) means, and it is different from what f = O(g) means, which is why the ≤O[l] notation could be misleading

[Yury G. Kudryashov]

What notation do you suggest for small o and theta?

[Vincent Beffara]

I would go for something like f ≼[l] g for f = O(g), f ≪[l] g for f = o(g) and f ≍[l] g for Θ

[Kalle Kytölä]

I like the last two of Vincent's suggestions a lot, and in my opinion they correspond very well to common use of these symbols. The first one may unfortunately have a risk of misinterpretation, still.

[Yury G. Kudryashov]

/poll Notation for is_O, is_o, is_Theta, and is_equivalent
f =O[l] g, f =o[l] g, f =Θ[l] g, and f ~[l] g
f ≼[l] g, f ≪[l] g, f ≍[l] g, and f ~[l] g

[Yury G. Kudryashov]

Feel free to add choices.

[Yury G. Kudryashov]

I like the fact that the symbols O, o, and Θ are present in the first choice.

[Mauricio Collares]

The second of Vincent's suggestions will probably be controversial with number theory people, since $\ll$ means O() in some subfields

[Kalle Kytölä]

I'm not sure I understood the transitivity issue with the $\in$ notation, so I voted for that for now (may change if someone explains). If $g \in O(h)$ then $O(g) \subset O(h)$, so we have as usual $f \in O(g) \Rightarrow f \in O(h)$ and I don't see anything wrong with transitivity.

(I do agree that this notation is not very commonly used, but in formalization we occasionally have to be more pedantic.)

[Kalle Kytölä]

By contrast, Eric Wieser's objection to using = for a non-symmetric relation (and even a non-reflexive relation in the case of $o$) is in my opinion relevant.

[Reid Barton]

calc f =O[l] g : sorry
...    =O[l] h : sorry

looks good to me but

calc f ∈O[l] g : sorry
...    ∈O[l] h : sorry

does not because $\in$ is not transitive

[Reid Barton]

You can't write

calc x ∈ y : sorry
...    ∈ z : sorry

[Reid Barton]

≼[l] is logical, but might not have a universally understood meaning

[Kalle Kytölä]

Thanks for the explanation! I don't think the second one is terrible, however. The same calc does not work for ordinary ∈, but that is because f ∈O[l] g really means f ∈ O(g). However f ∈O[l] g and g ∈O[l] h can be transitively chained because the second implies O(g) ⊆ O(h).

[Kyle Miller]

I was pronouncing ∈O[l] as "is in O[l] of", which feels transitive even if ∈ normally isn't.

[Eric Wieser]

How about having a second syntax just for calc?

calc f ∈O[l] g : sorry
...    ⊆O[l] h : sorry

[Eric Wieser]

They'd both be defined to mean the same thing, but the second one reads better in calc (and would not appear anywhere else). Really the problem is that this relation isn't transitive in a way that makes sense syntactically

[Kalle Kytölä]

I find both f ∈O[l] g ∈O[l] h or g ∈ O(g) ⊆ O(h) acceptable, but this compromise suggestion looks weird to me. There is no binary relation ⊆O[l] that takes a function g as its first argument, right?

[Scott Morrison]

I don't like the idea of duplicating notation just to make calc look smoother. I think the "simple" option of =O[l] and friends has the advantage of an obvious interpretation, even if when it appears multiple times in a calc block there is some dissonance.

[Eric Wieser]

Is changing docs#asymptotics.is_O to be a set a viable option? Then we wouldn't need any special notation for the relation, and could just use ∈ and ⊆.

[Kevin Buzzard]

I think it's fascinating that this discussion even exists. I've never heard anyone talk about this subtlety before.

[Yury G. Kudryashov]

Eric Wieser said:

Is changing docs#asymptotics.is_O to be a set a viable option? Then we wouldn't need any special notation for the relation, and could just use ∈ and ⊆.

This won't work with calc unless you explicitly use a lemma saying f ∈ O(g) → O(f) ⊆ O(g) and I think that we should hide this from the users of calc.

[Kyle Miller]

@[trans] lemma set.mem_of_mem_of_subset {α : Type*} {x : α} {s t : set α}
  (hx : x ∈ s) (hs : s ⊆ t) : x ∈ t := hs hx

@[trans] lemma set.mem_of_mem_of_ssubset {α : Type*} {x : α} {s t : set α}
  (hx : x ∈ s) (hs : s ⊂ t) : x ∈ t := hs.1 hx

example {α : Type*} {x : α} (s t u : set α) (hx : x ∈ s) (hs : s ⊆ t) (ht : t ⊂ u) :
  x ∈ u :=
calc x ∈ s : hx
   ... ⊆ t : hs
   ... ⊂ u : ht

[Kyle Miller]

(That still has the issue you mention though. I just wanted to try using calc for this.)

[Yury G. Kudryashov]

Also, I want to operate with g, not O(g) because we have, e.g., is_O.trans_eventually_eq

[Yury G. Kudryashov]

(not yet in master)

[Yury G. Kudryashov]

(it follows from docs#asymptotics.is_O.congr')

[Yury G. Kudryashov]

And once we fix docs#trans_rel_left, we'll be able to use (with either notation)

calc f  = f' : _
... =O[l] g : _
... = g' : _

[Yury G. Kudryashov]

Another question: can we allow something like this?

x ^ 2 =O[x in at_top] x ^ 3

[Yury G. Kudryashov]

IMHO, it looks better than

(λ x, x ^ 2) =O[at_top] (λ x, x ^ 3)

[Yury G. Kudryashov]

(of course, the same applies to other choices)

[Yury G. Kudryashov]

If possible (especially if it's possible to use it with calc), I'd love to have both f =O[l] g and x ^ 2 =O[x in l] x ^ 3.

[Mario Carneiro]

I toyed around with this a bit, and I think it's not possible in lean 3. The reason is because notations can only bind things to the right of the binder

[Yury G. Kudryashov]

Will it be possible with Lean 4?

[Eric Wieser]

Yury G. Kudryashov said:

Also, I want to operate with g, not O(g) because we have, e.g., is_O.trans_eventually_eq

What's the statement of this lemma?

[Eric Wieser]

Yury G. Kudryashov said:

Eric Wieser said:

Is changing docs#asymptotics.is_O to be a set a viable option? Then we wouldn't need any special notation for the relation, and could just use ∈ and ⊆.

This won't work with calc unless you explicitly use a lemma saying f ∈ O(g) → O(f) ⊆ O(g) and I think that we should hide this from the users of calc.

I agree this would need such a lemma, but I don't think it's unreasonable to make users use such a lemma; IMO it results in less strange notation.

I assume your other remark would be solved by having a eventually_eq f g -> O(f) = O(g) lemma in the same style.

[Yury G. Kudryashov]

is_O.trans_eventually_eq

[Yury G. Kudryashov]

What is the type of O(f), f : α → E?

[Yury G. Kudryashov]

Note that docs#asymptotics.is_O allows different codomains for functions.

[Yury G. Kudryashov]

IMHO, making users explicitly use lemmas like f ∈ O(g) → O(f) ⊆ O(g) makes calc computations with big-O/small-o notation much less convenient

[Yury G. Kudryashov]

For me, the main convenience of calc is that it automatically chooses @[trans] lemmas (also, it's easier to read).

[Eric Wieser]

I'm suggesting instead of writing is_O f g l we write f ∈ O l g, so instead of

def is_O : (α → E) → (α → F) → filter α → Prop

we have

def O : filter α → (α → F) → set (α → E)

Mathematically the content is identical, it's just an argument permutation and re-folding of set.

[Eric Wieser]

I think what you'd write as

calc f₁ =ᶠ[l] f₂ : _
    ... =O[l] g : _
    ... =O[l] g₂ : _

I'm suggesting we write as

calc f₁ =ᶠ[l] f₂ : _
    ... ∈ O l g : _
    ... = O l g₂ : O_congr _

[Yury G. Kudryashov]

Then you really need to use lemmas like O_subset_O_of_mem_O. I really like the fact that f =O[l] g is a relation between two functions. IMHO,

calc f =O[l] g : _
... =o[l] g' : _
... =ᶠ[l] h : _

looks better than

calc f ∈ O l g : _
... ⊆ o l g' : O_subset_o_of_mem_o _
... = o l h : o_congr _

[Yury G. Kudryashov]

BTW, I don't know how to make a trans lemma that will make your example work.

[Eric Wieser]

Which line of my example do you think is missing a trans lemma?

[Yury G. Kudryashov]

How do you glue the first and the second line?

[Yury G. Kudryashov]

=ᶠ[l] and ∈

[Eric Wieser]

Something like:

lemma foo (hf : f₁ =ᶠ[l] f₂) (hf_mem : f₂ ∈ O l g) :
  f₁ ∈ O l g := sorry

which I think is just an application of docs#filter.eventually_eq.trans_is_O with adjusted notation

[Eric Wieser]

Are you suggesting it's mathematically false, or that trans doesn't like it?

[Yury G. Kudryashov]

Could you try to make it work with trans, please (e.g., with constant/axiom instead of actual definitions)?

[Yury G. Kudryashov]

I added "define sets O(f) etc" as a choice in the poll. Let me notify all the people who already voted: @Mauricio Collares @Kyle Miller @Anas Himmi @Violeta Hernández @Scott Morrison @Sebastien Gouezel @Yaël Dillies @Kalle Kytölä @Vincent Beffara @Moritz Doll @Frédéric Dupuis @Anatole Dedecker
Also, it would be nice to hear from @Patrick Massot @Heather Macbeth

[Yury G. Kudryashov]

Should we choose some deadline for the poll so that we don't wait forever? E.g., 24h from now? Or better 48h?

[Eric Wieser]

Yury G. Kudryashov said:

Could you try to make it work with trans, please (e.g., with constant/axiom instead of actual definitions)?

hmm, you're right; I can't get that to work:

import analysis.asymptotics.asymptotic_equivalent

open asymptotics

variables {α E F : Type} [normed_group E] [normed_group F]
variables (E)

def O (l : filter α) (g : α → F) : set (α → E) := {f | is_O f g l }

variables {E}

@[trans, priority 2] theorem filter.eventually_eq.trans_mem_O
  {l : filter α} {f₁ f₂ : α → E} {g : α → F}
  (hf : f₁ =ᶠ[l] f₂) (h : f₂ ∈ O E l g) : f₁ ∈ O E l g :=
sorry

example {l : filter α} {f₁ f₂ : α → E} {g₁ g₂ : α → F}
  (hf : f₁ =ᶠ[l] f₂)
  (hfg : f₂ ∈ O E l g₁) : f₁ ∈ O E l g₁ :=
calc f₁ =ᶠ[l] f₂ : hf
    ... ∈ O E l g₁ : hfg --fails

[Eric Wieser]

Yury G. Kudryashov said:

And once we fix docs#trans_rel_left, we'll be able to use (with either notation)

I think this is the reason though; so none of the proposals will work with trans right now

[Bhavik Mehta]

cc @Alex Kontorovich and @Thomas Bloom, since we talked about a similar question a while ago in the context of analytic number theory

[Eric Wieser]

hmm, you're right; I can't get that to work:

I think calc can only match on the head symbol (ie not on the _ ∈ O E l _ which has a nested expression), which is rather annoying

[Patrick Massot]

I slightly prefer the first option but defining sets would also make sense.

[Kalle Kytölä]

I fully agree there should be a deadline for the poll.

In fact it already looks fairly clear that the non-symmetric and non-reflexive equality symbols are the most popular, which just surprises me a bit. Even the (slightly sloppy but) common math notation $f = o(g)$ doesn't suggest symmetricity or reflexivity as much as f =o[l] g.

[Alex Kontorovich]

In many settings, including all of analytic number theory, it is very common to have long strings of arguments like:

f₁ = f₂ + O(g₁)
   = f₃ + O(g₂)
   = ...

These mean: |f₁ - f₂| = O(g₁), |f₂ - f₃| = O(g₂), etc, and also g₁≪g₂, etc. (By the way, here I'm using ≪ for big-Oh, as used to be the case universally. But then Knuth, just to mess with everybody, redefined it to mean little-oh. So now in CS/algorithms and also parts of pde's etc, you'll see that convention. Not sure what if anything can, or should, be done about this... The absolute worst is seeing topologists write X≫0, which should be totally meaningless...)

Anyway, would be really great if such a thing existed!...

[Yury G. Kudryashov]

Have a look at https://hal.inria.fr/hal-01719918v3

[Yury G. Kudryashov]

I'm not ready to implement it in Lean (yet).

[Yury G. Kudryashov]

Note that the equality sign in your notation is not symmetric too.

[Yury G. Kudryashov]

Kalle Kytölä said:

I fully agree there should be a deadline for the poll.

In fact it already looks fairly clear that the non-symmetric and non-reflexive equality symbols are the most popular, which just surprises me a bit. Even the (slightly sloppy but) common math notation $f = o(g)$ doesn't suggest symmetricity or reflexivity as much as f =o[l] g.

I suggest that people start reviewing #14129. If in a day or two another choice will get more votes, then I'll do a search&replace. One exception: if the "define sets" approach wins, then we'll have to discard #14129 and do a completely different refactor.

[Eric Wieser]

My feeling now is that probably calc needs a rework before the set approach really pays off

[Eric Wieser]

Yury G. Kudryashov said:

Have a look at https://hal.inria.fr/hal-01719918v3

From that paper:

It is not rare to see this reading enforced by the notation f ∈ o(e) in undergraduate-level teaching, allegedly to prevent students' confusion (see for example in [AF88], a textbook from the eighties still popular in France).

My background in the area is similar to that of an undergrad, so it's perhaps not surprising what my opinion is

[Yury G. Kudryashov]

Then I suggest that we use one of the other notations for now. If someone wants to define sets, this person needs to (or find someone to) rework calc first.

[Eric Wieser]

I think a reference to that paper might be a good idea in the module docstrings, in case we want to explore other options in future

[Eric Wieser]

It looks like quite an interesting approach

[Kyle Miller]

I'm not sure if this is already handled somewhere in the PR, but for long strings like in @Alex Kontorovich's example, we might have some notation something like this:

notation f ` = ` g ` +O[`:65 l `](`:0 k `)` := is_O l (f - g) k

@[trans] theorem is_O.trans {f f' f'' : α → E'} {g : α → F'} (h : f = f' +O[l](g))
  (h' : f' = f'' +O[l](g)) : f = f'' +O[l](g) := sorry

example (f g h : ℝ → ℝ) : f = g +O[at_top](h) :=
calc f = f +O[at_top](h) : sorry
   ... = g +O[at_top](h) : sorry

(This is just a quick test that it parses. There's an error due to using is_O l (f - g) k paired with a bug in calc.)

[Kyle Miller]

Did we already consider the version of the notation with parentheses? It should still work with calc.

Some examples from taking the first couple lemmas in analysis/asymptotics/asymptotics:

notation f ` =O[`:50 l `](` g:0 `)` := is_O l f g

lemma is_O_iff_is_O_with : f =O[l](g) ↔ ∃ c : ℝ, is_O_with c l f g := by rw is_O

lemma is_O_iff : f =O[l](g) ↔ ∃ c : ℝ, ∀ᶠ x in l, ∥f x∥ ≤ c * ∥g x∥ :=
by simp only [is_O, is_O_with]

[Kyle Miller]

Yeah, this parses:

example (f g h : ℝ → ℝ) : f =O[at_top](h) :=
calc f =O[at_top](g) : sorry
   ... =O[at_top](h) : sorry

[Yury G. Kudryashov]

Could someone please review #14129? I'm OK with f =O[l](g) or f =O[l] g notation (BTW, one can write f =O[l](g) with f =O[l] g notation).

[Yury G. Kudryashov]

I'm afraid that the PR will rot.