Zulip Chat Archive

Stream: new members

Topic: big oh

Thorsten Altenkirch (Sep 14 2020 at 12:47):

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

Johan Commelin (Sep 14 2020 at 12:48):

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

Thorsten Altenkirch (Sep 14 2020 at 12:49):

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

Rob Lewis (Sep 14 2020 at 12:49):

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

Last updated: Dec 20 2023 at 11:08 UTC