Zulip Chat Archive

Stream: new members

Topic: big oh


view this post on Zulip Thorsten Altenkirch (Sep 14 2020 at 12:47):

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

view this post on Zulip 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

view this post on Zulip Thorsten Altenkirch (Sep 14 2020 at 12:49):

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

view this post on Zulip Rob Lewis (Sep 14 2020 at 12:49):

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


Last updated: May 08 2021 at 03:17 UTC