Big-Oh notation

Stream: Is there code for X?

[Thomas]

Hello everyone, I'm brand new here, so apologies in advance if this is the wrong place to post etc.

Is there code already to deal with big-oh notation? e.g. being able to say things like 2x = O(x) and more complicated things with dependencies, like (x+h)^2 = x^2 + O_h(x), and being able to perform 'calculus' on this, so e.g. combining O(x)+O(xlog x) = O(xlog x).

[Johan Commelin]

There is code to deal with Big-Oh. Unfortunately no notation :rofl:

[Johan Commelin]

docs#asymptotics.is_O

[Johan Commelin]

So basically, yes. You can do what you want. But you'll have to write things slightly differently from the way it's written in usual maths.

[Thomas]

Wonderful, thank you!