Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Two new AFP articles: Landau Symbols and the A...


view this post on Zulip Email Gateway (Aug 22 2022 at 10:54):

From: Tobias Nipkow <nipkow@in.tum.de>
Landau Symbols
Manuel Eberl

This entry provides Landau symbols to describe and reason about the asymptotic
growth of functions for sufficiently large inputs. A number of simplification
procedures are provided for additional convenience: cancelling of dominated
terms in sums under a Landau symbol, cancelling of common factors in products,
and a decision procedure for Landau expressions containing products of powers of
functions like x, ln(x), ln(ln(x)) etc.

http://afp.sourceforge.net/entries/Landau_Symbols.shtml

The Akra-Bazzi theorem and the Master theorem
Manuel Eberl

This article contains a formalisation of the Akra-Bazzi method based on a proof
by Leighton. It is a generalisation of the well-known Master Theorem for
analysing the complexity of Divide & Conquer algorithms. We also include a
generalised version of the Master theorem based on the Akra-Bazzi theorem, which
is easier to apply than the Akra-Bazzi theorem itself.

Some proof methods that facilitate applying the Master theorem are also
included. For a more detailed explanation of the formalisation and the proof
methods, see the accompanying paper (publication forthcoming).

Enjoy!
smime.p7s


Last updated: Apr 26 2024 at 16:20 UTC