big oh

Stream: new members

[Thorsten Altenkirch]

Has anybody done some proofs on big oh and related definitions on asymptote complexity in Lean?

[Johan Commelin]

We have quite a bit of calculus by now. But not really anything on analysis of algorithms a la Knuth / TAOCP

[Thorsten Altenkirch]

Actually it is not so much the algorithm but just proving things about classification of functions.

[Rob Lewis]

There's https://leanprover-community.github.io/mathlib_docs/analysis/asymptotics.html