avewright/proofwiki-math huggingface dataset:
Theorem: Laplace Transform of Gauss Error Function

:$\laptrans {\map \erf t} = \dfrac 1 s \map \exp {\dfrac {s^2} 4} \map \erfc {\dfrac s 2}$
where:
:$\laptrans f$ denotes the Laplace transform of the function $f$
:$\erf$ denotes the Gauss error function
:$\erfc$ denotes the complementary error function
:$\exp$ denotes the exponential function.

Proof:
By Derivative of Gauss Error Function, we have: 
:$\ds \map {\frac \d {\d t} } {\map \erf t} = \frac 2 {\sqrt \pi} e^{-t^2}$
By Primitive of Exponential Function, we have: 
:$\ds \int e^{-s t} \rd t = -\frac {e^{-s t} } s$
So: 
{{begin-eqn}}
{{eqn | l = \laptrans {\map \erf t}
      | r = \int_0^\infty e^{-s t} \map \erf t \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \intlimits {-\frac 1 s e^{-s t} \map \erf t} 0 \infty - \int_0^\infty \paren {-\frac 2 {\sqrt \pi} \frac {e^{-s t} } s e^{-t^2} } \rd t
      | c = Integration by Parts
}}
{{eqn | r = -\frac 1 s \lim_{t \mathop \to \infty} \paren {e^{-s t} \map \erf t} + \frac 1 s e^0 \erf 0 + \frac 2 {s \sqrt \pi} \int_0^\infty \exp \paren {-s t - t^2} \rd t
}}
{{end-eqn}}
We have: 
{{begin-eqn}}
{{eqn | l = \lim_{t \mathop \to \infty} \paren {e^{-s t} \map \erf t}
      | r = \paren {\lim_{t \mathop \to \infty} e^{-s t} } \paren {\lim_{t \mathop \to \infty} \map \erf t}
      | c = Product Rule for Limits of Real Functions
}}
{{eqn | r = 0 \times 1
      | c = Exponential Tends to Zero and Infinity, Limit to Infinity of Gauss Error Function
}}
{{eqn | r = 0
}}
{{end-eqn}}
We also have: 
{{begin-eqn}}
{{eqn | l = \frac 1 s e^0 \erf 0
      | r = \frac 1 s \int_0^0 e^{-t^2} \rd t
      | c = Exponential of Zero, {{Defof|Gauss Error Function}}
}}
{{eqn | r = 0
      | c = Definite Integral on Zero Interval
}}
{{end-eqn}}
Therefore: 
{{begin-eqn}}
{{eqn | l = \laptrans {\map \erf t} 
      | r = \frac 2 {s \sqrt \pi} \int_0^\infty \map \exp {-\paren {t^2 + s t} } \rd t
}}
{{eqn | r = \frac 2 {s \sqrt \pi} \int_0^\infty \map \exp {-\paren {\paren {t + \frac s 2}^2 - \frac {s^2} 4} } \rd t
      | c = completing the square
}}
{{eqn | r = \frac 2 {s \sqrt \pi} \map \exp {\frac {s^2} 4} \int_0^\infty \map \exp {-\paren {t + \frac s 2}^2} \rd t
      | c = Exponential of Sum
}}
{{eqn | r = \frac 2 {s \sqrt \pi} \map \exp {\frac {s^2} 4} \int_{\frac s 2}^\infty \map \exp {-u^2} \rd u
      | c = substituting $u = t + \dfrac s 2$
}}
{{eqn | r = \frac 1 s \map \exp {\frac {s^2} 4} \paren {\frac 2 {\sqrt \pi} \int_{\frac s 2}^\infty \map \exp {-u^2} \rd u}
}}
{{eqn | r = \frac 1 s \map \exp {\frac {s^2} 4} \map \erfc {\frac s 2}
      | c = {{Defof|Complementary Error Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Gauss Error Function of Root

:$\laptrans {\map \erf {\sqrt t} } = \dfrac 1 {s \sqrt {s + 1} }$
where:
:$\laptrans f$ denotes the Laplace transform of the function $f$
:$\erf$ denotes the Gauss error function

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map \erf {\sqrt t} }
      | r = \laptrans {\frac 2 {\sqrt \pi} \int_0^{\sqrt t} \map \exp {-u^2} \rd u}
      | c = {{Defof|Gauss Error Function}}
}}
{{eqn | r = \laptrans {\frac 2 {\sqrt \pi} \int_0^{\sqrt t} \paren {\sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {u^{2 n} } {n!} \rd u} }
      | c = {{Defof|Exponential Function/Real|Real Exponential Function|subdef = Power Series Expansion}}
}}
{{eqn | r = \laptrans {\frac 2 {\sqrt \pi} \paren {\sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {\paren {\sqrt t}^{2 n + 1} } {\paren {2 n + 1} n!} } }
      | c = Primitive of Power
}}
{{eqn | r = \frac 2 {\sqrt \pi} \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n} {\paren {2 n + 1} n!} \laptrans {t^{n + \frac 1 2} }
      | c = Linear Combination of Laplace Transforms
}}
{{eqn | r = \frac 2 {\sqrt \pi} \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {\map \Gamma {n + \frac 3 2} } {\paren {2 n + 1} n! s^{n + \frac 3 2} } 
      | c = Laplace Transform of Real Power
}}
{{eqn | r = \frac 2 {s^{3/2} \sqrt \pi} \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {\paren {n + \frac 1 2} \map \Gamma {n + \frac 1 2} } {\paren {2 n + 1} n! s^n}
      | c = Gamma Difference Equation
}}
{{eqn | r = \frac 1 {s^{3/2} \sqrt \pi} \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {\map \Gamma {n + \frac 1 2} } {\map \Gamma {n + 1} s^n} 
      | c = Gamma Function Extends Factorial
}}
{{end-eqn}}
We have: 
{{begin-eqn}}
{{eqn | l = \map \Gamma {n + \frac 1 2}
      | r = \frac \pi {\map \sin {\pi \paren {\frac 1 2 - n} } \map \Gamma {\frac 1 2 - n} }
      | c = Euler's Reflection Formula
}}
{{eqn | r = \frac \pi {\map \cos {-n \pi} \map \Gamma {\frac 1 2 - n} }
      | c = Sine of Complement equals Cosine
}}
{{eqn | r = \frac {\paren {-1}^n \pi} {\map \Gamma {\frac 1 2 - n} }
      | c = Cosine of Integer Multiple of Pi
}}
{{end-eqn}}
So: 
{{begin-eqn}}
{{eqn | l = \frac 1 {s^{3/2} \sqrt \pi} \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {\map \Gamma {n + \frac 1 2} } {\map \Gamma {n + 1} s^n} 
      | r = \frac 1 {s^{3/2} \sqrt \pi} \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {\paren {-1}^n \pi} {\map \Gamma {n + 1} \map \Gamma {\frac 1 2 - n} s^n}
      | c = 
}}
{{eqn | r = \frac 1 {s^{3/2} } \sum_{n \mathop = 0}^\infty \frac {\sqrt \pi} {\map \Gamma {n + 1} \map \Gamma {\frac 1 2 - n} s^n}
      | c = 
}}
{{eqn | r = \frac 1 {s^{3/2} } \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {-\frac 1 2 + 1} } {\map \Gamma {n + 1} \map \Gamma {-\frac 1 2 - n + 1} s^n}
      | c = Gamma Function of One Half
}}
{{eqn | r = \dfrac 1 {s^{3/2} } \sum_{n \mathop = 0}^\infty \binom {-\frac 1 2} n \frac 1 {s^n}
      | c = {{Defof|Binomial Coefficient/Complex Numbers|Binomial Coefficient}}
}}
{{eqn | r = \dfrac 1 {s^{3/2} } \paren {1 + \dfrac 1 s}^{-1/2}
      | c = General Binomial Theorem
}}
{{eqn | r = \dfrac 1 {s \sqrt {s + 1} }
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Sine Integral Function

:$\laptrans {\map \Si t} = \dfrac 1 s \arctan \dfrac 1 s$
where:
:$\laptrans f$ denotes the Laplace transform of the function $f$
:$\Si$ denotes the sine integral function

Proof:
Let $\map f t := \map \Si t = \ds \int_0^t \dfrac {\sin u} u \rd u$.
Then:
:$\map f 0 = 0$
and:
{{begin-eqn}}
{{eqn | l = \map {f'} t
      | r = \dfrac {\sin t} t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = t \map {f'} t
      | r = \sin t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \laptrans {t \map {f'} t}
      | r = \laptrans {\sin t}
      | c = 
}}
{{eqn | r = \dfrac 1 {s^2 + 1}
      | c = Laplace Transform of Sine
}}
{{eqn | ll= \leadsto
      | l = -\dfrac \d {\d s} \laptrans {\map {f'} t}
      | r = \dfrac 1 {s^2 + 1}
      | c = Derivative of Laplace Transform
}}
{{eqn | ll= \leadsto
      | l = \map {\dfrac \d {\d s} } {s \laptrans {\map f t} - \map f 0}
      | r = -\dfrac 1 {s^2 + 1}
      | c = Laplace Transform of Derivative
}}
{{eqn | ll= \leadsto
      | l = s \laptrans {\map f t}
      | r = -\int \dfrac 1 {s^2 + 1} \rd s
      | c = $\map f 0 = 0$, and integrating both sides {{WRT|Integration}} $s$
}}
{{eqn | ll= \leadsto
      | l = s \laptrans {\map f t}
      | r = -\arctan s + C
      | c = Primitive of $\dfrac 1 {x^2 + a^2}$
}}
{{end-eqn}}
By the Initial Value Theorem of Laplace Transform:
:$\ds \lim_{s \mathop \to \infty} s \laptrans {\map f t} = \lim_{t \mathop \to 0} \map f t = \map f 0 = 0$
which leads to:
:$c = \dfrac \pi 2$
Thus:
{{begin-eqn}}
{{eqn | l = s \laptrans {\map f t}
      | r = \dfrac \pi 2 - \arctan s
      | c = 
}}
{{eqn | r = \arccot s
      | c = Sum of Arctangent and Arccotangent
}}
{{eqn | r = \arctan \dfrac 1 s
      | c = Arctangent of Reciprocal equals Arccotangent
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\map f t}
      | r = \dfrac 1 s \arctan \dfrac 1 s
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Sine Integral Function

:$\laptrans {\map \Si t} = \dfrac 1 s \arctan \dfrac 1 s$
where:
:$\laptrans f$ denotes the Laplace transform of the function $f$
:$\Si$ denotes the sine integral function

Proof:
Let $\map f t := \map \Si t = \ds \int_0^t \dfrac {\sin u} u \rd u$.
Then:
:$\map f 0 = 0$
and:
{{begin-eqn}}
{{eqn | l = \map \Si t
      | r = \int_0^t \dfrac {\sin u} u \rd u
      | c = {{Defof|Sine Integral Function}}
}}
{{eqn | r = \int_0^t \dfrac 1 u \paren {u - \dfrac {u^3} {3!} + \dfrac {u^5} {5!} - \dfrac {u^7} {7!} + \dotsb} \rd u
      | c = {{Defof|Real Sine Function}}
}}
{{eqn | r = t - \dfrac {t^3} {3 \times 3!} + \dfrac {t^5} {5 \times 5!} - \dfrac {t^7} {7 \times 7!} + \dotsb
      | c = Primitive of Power
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\map \Si t}
      | r = \laptrans {t - \dfrac {t^3} {3 \times 3!} + \dfrac {t^5} {5 \times 5!} - \dfrac {t^7} {7 \times 7!} + \dotsb}
      | c = 
}}
{{eqn | r = \dfrac 1 {s^2} - \dfrac 1 {3 \times 3!} \dfrac {3!} {s^4} + \dfrac 1 {5 \times 5!} \dfrac {5!} {s^6} - \dfrac 1 {7 \times 7!} \dfrac {7!} {s^8} + \dotsb
      | c = Laplace Transform of Positive Integer Power
}}
{{eqn | r = \dfrac 1 {s^2} - \dfrac 1 {3 s^4} + \dfrac 1 {5 s^6} - \dfrac 1 {7 s^8} + \dotsb
      | c = simplifying
}}
{{eqn | r = \dfrac 1 s \paren {\dfrac {\paren {1 / s} } 1 - \dfrac {\paren {1 / s}^3} 3 + \dfrac {\paren {1 / s}^5} 5 - \dfrac {\paren {1 / s}^7} 7 + \dotsb}
      | c = rearranging
}}
{{eqn | r = \dfrac 1 s \arctan \dfrac 1 s
      | c = Power Series Expansion for Real Arctangent Function
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Sine Integral Function

:$\laptrans {\map \Si t} = \dfrac 1 s \arctan \dfrac 1 s$
where:
:$\laptrans f$ denotes the Laplace transform of the function $f$
:$\Si$ denotes the sine integral function

Proof:
Let $\map f t := \map \Si t = \ds \int_0^t \dfrac {\sin u} u \rd u$.
Then:
:$\map f 0 = 0$
and:
{{begin-eqn}}
{{eqn | l = \map \Si t
      | r = \int_0^t \dfrac {\sin u} u \rd u
      | c = {{Defof|Sine Integral Function}}
}}
{{eqn | r = \int_0^1 \dfrac {\sin t v} v \rd v
      | c = Integration by Substitution $u = t v$
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\map \Si t}
      | r = \laptrans {\int_0^1 \dfrac {\sin t v} v \rd v}
      | c = 
}}
{{eqn | r = \int_0^\infty e^{-s t} \paren {\int_0^1 \dfrac {\sin t v} v \rd v} \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \int_0^1 \dfrac 1 v \paren {\int_0^\infty e^{-s t} \sin t v \rd t} \rd v
      | c = exchanging order of integration
}}
{{eqn | r = \int_0^1 \dfrac {\laptrans {\sin t v} } v \rd v
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \int_0^1 \dfrac {\d v} {s^2 + v^2}
      | c = Laplace Transform of Sine
}}
{{eqn | r = \intlimits {\dfrac 1 s \arctan \dfrac v s} 0 1
      | c = Primitive of $\dfrac 1 {x^2 + a^2}$
}}
{{eqn | r = \dfrac 1 s \arctan \dfrac 1 s
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Cosine Integral Function

:$\laptrans {\map \Ci t} = \dfrac {\map \ln {s^2 + 1} } {2 s}$
where:
:$\laptrans f$ denotes the Laplace transform of the function $f$
:$\Ci$ denotes the cosine integral function.

Proof:
Let $\map f t := \map \Ci t = \ds \int_t^\infty \dfrac {\cos u} u \rd u$.
Then:
{{begin-eqn}}
{{eqn | l = \map {f'} t
      | r = -\dfrac {\cos t} t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = t \map {f'} t
      | r = -\cos t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \laptrans {t \map {f'} t}
      | r = -\laptrans {\cos t}
      | c = 
}}
{{eqn | r = -\dfrac s {s^2 + 1}
      | c = Laplace Transform of Cosine
}}
{{eqn | ll= \leadsto
      | l = -\dfrac \d {\d s} \laptrans {\map {f'} t}
      | r = -\dfrac s {s^2 + 1}
      | c = Derivative of Laplace Transform
}}
{{eqn | ll= \leadsto
      | l = \map {\dfrac \d {\d s} } {s \laptrans {\map f t} - \map f 0}
      | r = \dfrac s {s^2 + 1}
      | c = Laplace Transform of Derivative
}}
{{eqn | ll= \leadsto
      | l = s \laptrans {\map f t}
      | r = \int \dfrac s {s^2 + 1} \rd s
      | c = $\map f 0 = 0$, and integrating both sides {{WRT|Integration}} $s$
}}
{{eqn | ll= \leadsto
      | l = s \laptrans {\map f t}
      | r = \dfrac 1 2 \map \ln {s^2 + 1} + C
      | c = Primitive of $\dfrac x {x^2 + a^2}$
}}
{{end-eqn}}
By the Initial Value Theorem of Laplace Transform:
:$\ds \lim_{s \mathop \to \infty} s \laptrans {\map f t} = \lim_{t \mathop \to 0} \map f t = \map f 0 = 0$
which leads to:
:$c = 0$
Thus:
{{begin-eqn}}
{{eqn | l = s \laptrans {\map f t}
      | r = \dfrac 1 2 \map \ln {s^2 + 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\map f t}
      | r = \dfrac {\map \ln {s^2 + 1} } {2 s}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Exponential Integral Function

Let $\Ei: \R_{>0} \to \R$ denote the exponential integral function:
:$\map \Ei x = \ds \int_{t \mathop = x}^{t \mathop \to +\infty} \frac {e^{-t} } t \rd t$
Then:
:$\laptrans {\map \Ei t} = \dfrac {\map \ln {s + 1} } s$
where $\laptrans f$ denotes the Laplace transform of the function $f$

Proof:
Let $\map f t := \map \Ei t = \ds \int_t^\infty \dfrac {e^{-u} } u \rd u$.
Then:
{{begin-eqn}}
{{eqn | l = \map {f'} t
      | r = -\dfrac {e^{-t} } t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = t \map {f'} t
      | r = -e^{-t}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \laptrans {t \map {f'} t}
      | r = -\laptrans {e^{-t} }
      | c = 
}}
{{eqn | r = -\dfrac 1 {s + 1}
      | c = Laplace Transform of Exponential
}}
{{eqn | ll= \leadsto
      | l = -\dfrac \d {\d s} \laptrans {\map {f'} t}
      | r = -\dfrac 1 {s + 1}
      | c = Derivative of Laplace Transform
}}
{{eqn | ll= \leadsto
      | l = \map {\dfrac \d {\d s} } {s \laptrans {\map f t} - \map f 0}
      | r = \dfrac 1 {s + 1}
      | c = Laplace Transform of Derivative
}}
{{eqn | ll= \leadsto
      | l = s \laptrans {\map f t}
      | r = \int \dfrac 1 {s + 1} \rd s
      | c = $\map f 0 = 0$, and integrating both sides {{WRT|Integration}} $s$
}}
{{eqn | ll= \leadsto
      | l = s \laptrans {\map f t}
      | r = \map \ln {s + 1} + C
      | c = Primitive of $\dfrac 1 {a x + b}$
}}
{{end-eqn}}
By the Initial Value Theorem of Laplace Transform:
:$\ds \lim_{s \mathop \to \infty} s \laptrans {\map f t} = \lim_{t \mathop \to 0} \map f t = \map f 0 = 0$
which leads to:
:$c = 0$
Thus:
{{begin-eqn}}
{{eqn | l = s \laptrans {\map f t}
      | r = \map \ln {s + 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\map f t}
      | r = \dfrac {\map \ln {s + 1} } s
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Heaviside Step Function

Let $\map {u_c} t$ denote the Heaviside step function:
:<nowiki>$\map {u_c} t = \begin {cases}
1 & : t > c \\
0 & : t < c
\end {cases}$</nowiki>
The Laplace transform of $\map {u_c} t$ is given by:
:$\laptrans {\map {u_c} t} = \dfrac {e^{-s c} } s$
for $\map \Re s > c$.

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map {u_c} t}
      | r = \int_0^{\to +\infty} \map {u_c} t e^{-s t} \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \int_0^c \map {u_c} t e^{-s t} \rd t + \int_c^{\to +\infty} \map {u_c} t e^{-s t} \rd t
      | c = Sum of Integrals on Adjacent Intervals for Integrable Functions
}}
{{eqn | r = \int_0^c 0 \times e^{-s t} \rd t + \int_c^{\to +\infty} 1 \times e^{-s t} \rd t
      | c = {{Defof|Heaviside Step Function}}
}}
{{eqn | r = \int_c^{\to +\infty} e^{-s t} \rd t
      | c = 
}}
{{eqn | r = \lim_{L \mathop \to +\infty} \int_c^L e^{-s t} \rd t
      | c = {{Defof|Improper Integral}}
}}
{{eqn | r = \lim_{L \mathop \to +\infty} \intlimits {\dfrac {e^{-s t} } {-s} } c L
      | c = Primitive of $e^{a x}$
}}
{{eqn | r = \lim_{L \mathop \to +\infty} \dfrac {e^{-s L} } {-s} - \dfrac {e^{-s c} } {-s}
      | c = 
}}
{{eqn | r = 0 + \dfrac {e^{-s c} } s
      | c = simplification
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Laplace Transform of Heaviside Step Function

Let $\map {u_c} t$ denote the Heaviside step function:
:<nowiki>$\map {u_c} t = \begin {cases}
1 & : t > c \\
0 & : t < c
\end {cases}$</nowiki>
The Laplace transform of $\map {u_c} t$ is given by:
:$\laptrans {\map {u_c} t} = \dfrac {e^{-s c} } s$
for $\map \Re s > c$.

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans 1
      | r = \dfrac 1 s
      | c = Laplace Transform of 1
}}
{{eqn | ll= \leadsto
      | l = \laptrans {1 \times \map {u_c} t}
      | r = \dfrac 1 s \times e^{-c s}
      | c = Second Translation Property of Laplace Transforms
}}
{{eqn | r = \dfrac {e^{-s c} } s
      | c = simplification
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Laplace Transform of Dirac Delta Function

Let $\map \delta t$ denote the Dirac delta function.
The Laplace transform of $\map \delta t$ is given by:
:$\laptrans {\map \delta t} = 1$

Proof:
=== Lemma ===
{{:Laplace Transform of Dirac Delta Function/Lemma}}{{qed|lemma}}
Then:
{{begin-eqn}}
{{eqn | l = \laptrans {\map \delta t}
      | r = \lim_{\epsilon \mathop \to 0} \laptrans {\map {F_\epsilon} t}
      | c = {{Defof|Dirac Delta Function|index = 1}}
}}
{{eqn | r = \lim_{\epsilon \mathop \to 0} \dfrac {1 - e^{-s \epsilon} } {\epsilon s}
      | c = Lemma
}}
{{eqn | r = \lim_{\epsilon \mathop \to 0} \dfrac 1 {\epsilon s} \paren {1 - \paren {1 - s \epsilon + \dfrac {s^2 \epsilon^2} {2!} - \dotsb} }
      | c = {{Defof|Exponential Function/Real|subdef = Power Series Expansion|Exponential Function}}
}}
{{eqn | r = \lim_{\epsilon \mathop \to 0} \paren {1 - \dfrac {s \epsilon} {2!} + \dotsb}
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Dirac Delta Function

Let $\map \delta t$ denote the Dirac delta function.
The Laplace transform of $\map \delta t$ is given by:
:$\laptrans {\map \delta t} = 1$

Proof:
=== Lemma ===
{{:Laplace Transform of Dirac Delta Function/Lemma}}{{qed|lemma}}
Then:
{{begin-eqn}}
{{eqn | l = \laptrans {\map \delta t}
      | r = \lim_{\epsilon \mathop \to 0} \laptrans {\map {F_\epsilon} t}
      | c = {{Defof|Dirac Delta Function|index = 1}}
}}
{{eqn | r = \lim_{\epsilon \mathop \to 0} \dfrac {1 - e^{-s \epsilon} } {\epsilon s}
      | c = Lemma
}}
{{eqn | r = \lim_{\epsilon \mathop \to 0} \dfrac {\map {\dfrac \d {\d s} } {1 - e^{-s \epsilon} } } {\map {\dfrac \d {\d s} } {\epsilon s} }
      | c = L'Hôpital's Rule
}}
{{eqn | r = \lim_{\epsilon \mathop \to 0} \dfrac {\paren {-\epsilon} \times \paren {-e^{-s \epsilon} } } \epsilon
      | c = 
}}
{{eqn | r = \lim_{\epsilon \mathop \to 0} e^{-s \epsilon}
      | c = simplification
}}
{{eqn | r = 1
      | c = Exponential of Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Shifted Dirac Delta Function

Let $\map \delta t$ denote the Dirac delta function.
The Laplace transform of $\map \delta {t - a}$ is given by:
:$\laptrans {\map \delta {t - a} } = e^{-a s}$

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map \delta {t - a} }
      | r = \int_0^{\to +\infty} e^{-s t} \map \delta {t - a} \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = e^{-s \times a}
      | c = Integral to Infinity of Shifted Dirac Delta Function by Continuous Function
}}
{{eqn | r = e^{-a s}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Null Function

Let $\NN: \R \to \R$ be a null function.
The Laplace transform of $\map \NN t$ is given by:
:$\laptrans {\map \NN t} = 0$

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map \NN t}
      | r = \int_0^{\to +\infty} e^{-s t} \map \NN t \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{end-eqn}}
{{finish}}
Theorem: Second Translation Property of Laplace Transforms/Proof 1

Let $f$ be a function such that $\laptrans f$ exists.
Let $\laptrans {\map f t} = \map F s$ denote the Laplace transform of $f$.
Let $a \in \C$ or $\R$ be constant.
{{:Second Translation Property of Laplace Transforms}}

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map f {t - a} }
      | r = \int_0^{\to + \infty} e^{-s t} \map f {t - a} \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \int_0^{\to + \infty} e^{-s \paren {t - a} } e^{-a s} \map f {t - a} \rd \paren {t - a}
      | c = 
}}
{{eqn | r = e^{-a s} \int_0^{\to + \infty} e^{-s \paren {t - a} } \map f {t - a} \rd \paren {t - a}
      | c = 
}}
{{eqn | r = e^{-a s}\map F s
      | c = {{Defof|Laplace Transform}}
}}
{{end-eqn}}
{{qed}}
Theorem: Second Translation Property of Laplace Transforms/Proof 2

Let $f$ be a function such that $\laptrans f$ exists.
Let $\laptrans {\map f t} = \map F s$ denote the Laplace transform of $f$.
Let $a \in \C$ or $\R$ be constant.
{{:Second Translation Property of Laplace Transforms}}

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map g t}
      | r = \int_0^\infty e^{-s t} \map g t \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \int_0^a e^{-s t} \map g t \rd t + \int_a^\infty e^{-s t} \map g t \rd t
      | c = 
}}
{{eqn | r = \int_0^a 0 \times e^{-s t} \rd t + \int_a^\infty e^{-s t} \map f {t - a} \rd t
      | c = Definition of $\map g t$
}}
{{eqn | r = \int_a^\infty e^{-s t} \map f {t - a} \rd t
      | c = 
}}
{{eqn | r = \int_0^\infty e^{-s \paren {u + a} } \map f u \rd u
      | c = Integration by Substitution: $t = u + a$
}}
{{eqn | r = e^{-a s} \int_0^\infty e^{-s u} \map f u \rd u
      | c = 
}}
{{eqn | r = e^{-a s} \map F s
      | c = {{Defof|Laplace Transform}}
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Sine of t over t

Let $\sin$ denote the real sine function.
Let $\laptrans f$ denote the Laplace transform of a real function $f$.
Then:
:$\laptrans {\dfrac {\sin t} t} = \arctan \dfrac 1 s$

Proof:
From Limit of $\dfrac {\sin x} x$ at Zero:
:$\ds \lim_{x \mathop \to 0} \frac {\sin x} x = 1$
From Laplace Transform of Sine:
:$(1): \quad \laptrans {\sin t} = \dfrac 1 {s^2 + 1}$
From Laplace Transform of Integral:
:$(2): \quad \ds \laptrans {\dfrac {\map f t} t} = \int_s^{\to \infty} \map F u \rd u$
Hence:
{{begin-eqn}}
{{eqn | l = \laptrans {\dfrac {\sin t} t}
      | r = \int_s^{\to \infty} \dfrac 1 {u^2 + 1} \rd u
      | c = $(1)$ and $(2)$
}}
{{eqn | r = \lim_{L \mathop \to \infty} \int_s^L \dfrac 1 {u^2 + 1} \rd u
      | c = {{Defof|Improper Integral}}
}}
{{eqn | r = \lim_{L \mathop \to \infty} \bigintlimits {\arctan u} s L
      | c = Primitive of $\dfrac 1 {x^2 + a^2}$
}}
{{eqn | r = \lim_{L \mathop \to \infty} \paren {\arctan L - \arctan s}
      | c = 
}}
{{eqn | r = \dfrac \pi 2 - \arctan s
      | c = 
}}
{{eqn | r = \arccot s
      | c = Sum of Arctangent and Arccotangent
}}
{{eqn | r = \arctan \dfrac 1 s
      | c = Arctangent of Reciprocal equals Arccotangent
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Sine of t over t/Corollary

:$\laptrans {\dfrac {\sin a t} t} = \arctan \dfrac a s$

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\dfrac {\sin t} t}
      | r = \arctan \dfrac 1 s
      | c = Laplace Transform of Sine of t over t
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\dfrac {\sin a t} {a t} }
      | r = \dfrac 1 a \arctan \dfrac 1 {s / a}
      | c = Laplace Transform of Function of Constant Multiple
}}
{{eqn | r = \dfrac 1 a \arctan \dfrac a s
      | c = 
}}
{{end-eqn}}
But:
{{begin-eqn}}
{{eqn | l = \laptrans {\dfrac {\sin a t} {a t} }
      | r = \int_0^\infty e^{-s t} \dfrac {\sin a t} {a t} \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \dfrac 1 a \int_0^\infty e^{-s t} \dfrac {\sin a t} t \rd t
      | c = 
}}
{{eqn | r = \dfrac 1 a \laptrans {\dfrac {\sin a t} t}
      | c = 
}}
{{end-eqn}}
The result follows.
{{Qed}}
Theorem: Integral to Infinity of Function over Argument

:$\ds \int_0^\infty {\dfrac {\map f t} t} = \int_0^{\to \infty} \map F u \rd u$
provided the integrals converge.

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\dfrac {\map f t} t}
      | r = \int_s^{\to \infty} \map F u \rd u
      | c = Integral of Laplace Transform
}}
{{eqn | ll= \leadsto
      | l = \int_0^\infty e^{-s t} {\dfrac {\map f t} t} \rd t
      | r = \int_s^{\to \infty} \map F u \rd u
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | ll= \leadsto
      | l = \lim_{s \mathop \to 0} \int_0^\infty e^{-s t} \dfrac {\map f t} t \rd t
      | r = \lim_{s \mathop \to 0} \int_s^{\to \infty} \map F u \rd u
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int_0^\infty \dfrac {\map f t} t \rd t
      | r = \int_0^{\to \infty} \map F u \rd u
      | c = 
}}
{{end-eqn}}
{{qed}}