Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Laplace Transforms


view this post on Zulip Email Gateway (Aug 22 2022 at 20:25):

From: Lawrence Paulson <lp15@cam.ac.uk>
We have a new entry, small but valuable, thanks to Fabian Immler:

This entry formalizes the Laplace transform and concrete Laplace transforms for arithmetic functions, frequency shift, integration and (higher) differentiation in the time domain. It proves Lerch's lemma and uniqueness of the Laplace transform for continuous functions. In order to formalize the foundational assumptions, this entry contains a formalization of piecewise continuous functions and functions of exponential order.

It is now online at https://www.isa-afp.org/entries/Laplace_Transform.html.

Larry Paulson


Last updated: Mar 29 2024 at 12:28 UTC