Abstract
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.