avewright/proofwiki-math huggingface dataset:
Theorem: Laplace Transform of Cosine

Let $\cos$ be the real cosine function.
Let $\laptrans f$ denote the Laplace transform of the real function $f$.
Then:
:$\laptrans {\cos a t} = \dfrac s {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > a$.

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\cos a t}
      | r = \laptrans {\frac {e^{i a t} + e^{-i a t} } 2}
      | c = Euler's Cosine Identity
}}
{{eqn | r = \frac 1 2 \paren {\laptrans {e^{i a t} } + \laptrans {e^{-i a t} } }
      | c = Linear Combination of Laplace Transforms
}}
{{eqn | r = \frac 1 2 \paren {\frac 1 {s - i a} + \frac 1 {s + i a} }
      | c = Laplace Transform of Exponential
}}
{{eqn | r = \frac 1 2 \paren {\frac {s + i a + s - i a} {s^2 + a^2} }
      | c = simplifying
}}
{{eqn | r = \frac s {s^2 + a^2}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Cosine

Let $\cos$ be the real cosine function.
Let $\laptrans f$ denote the Laplace transform of the real function $f$.
Then:
:$\laptrans {\cos a t} = \dfrac s {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > a$.

Proof:
By definition of the Laplace Transform:
:$\ds \laptrans {\cos at} = \int_0^{\to +\infty} e^{-s t} \cos at \rd t$
From Integration by Parts:
:$\ds \int f g' \rd t = f g - \int f'g \rd t$
Here:
{{begin-eqn}}
{{eqn | l = f
      | r = \cos at
}}
{{eqn | ll= \leadsto
      | l = f'
      | r = -a \sin a t
      | c = Derivative of Cosine Function
}}
{{eqn | l = g'
      | r = e^{-s t}
}}
{{eqn | ll= \leadsto
      | l = g
      | r = -\frac 1 s e^{-s t}
      | c = Primitive of Exponential Function
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn | n = 1
      | l = \int e^{-s t} \cos a t \rd t
      | r = -\frac 1 s e^{-s t} \cos a t - \frac a s \int e^{-s t} \sin a t \rd t
}}
{{end-eqn}}
Consider:
:$\ds \int e^{-s t} \sin a t \rd t$
Again, using Integration by Parts:
:$\ds \int h j \,' \rd t = h j - \int h'j \rd t$
Here:
{{begin-eqn}}
{{eqn | l = h
      | r = \sin at
}}
{{eqn | ll= \leadsto
      | l = h'
      | r = a \cos at
      | c = Derivative of Sine Function
}}
{{eqn | l = j\,'
      | r = e^{-s t}
}}
{{eqn | ll= \leadsto
      | l = j
      | r = -\frac 1 s e^{-s t}
      | c = Primitive of Exponential Function
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn | l = \int e^{-s t} \sin a t \rd t
      | r = -\frac 1 s e^{-s t} \sin a t + \frac a s \int e^{-s t} \cos a t \rd t
}}
{{end-eqn}}
Substituting this into $(1)$:
{{begin-eqn}}
{{eqn | l = \int e^{-s t} \cos a t \rd t
      | r = -\frac 1 s e^{-s t} \cos a t - \frac a s \paren {-\frac 1 s e^{-s t} \sin a t + \frac a s \int e^{-s t} \cos a t \rd t}
}}
{{eqn | r = -\frac 1 s e^{-s t} \cos a t + \frac a {s^2} e^{-s t} \sin a - \frac {a^2} {s^2} \int e^{-s t} \cos a t \rd t
}}
{{eqn | ll= \leadsto
      | l = \paren {1 + \frac {a^2} {s^2} } \int e^{-s t} \cos a t \rd t
      | r = -\frac 1 s e^{-s t} \cos a t + \frac a {s^2} e^{-s t} \sin a t
}}
{{end-eqn}}
Evaluating at $t = 0$ and $t \to +\infty$:
{{begin-eqn}}
{{eqn | l = \paren {1 + \frac {a^2} {s^2} } \laptrans {\cos at}
      | r = \intlimits {-e^{-s t} \paren {\frac 1 s \cos a t - \frac a {s^2} \sin a t} } {t \mathop = 0} {t \mathop \to +\infty}
}}
{{eqn | r = 0 - \paren {-1 \paren {\frac 1 s \times 1 + \frac a {s^2} \times 0} }
      | c = Boundedness of Real Sine and Cosine, Complex Exponential Tends to Zero
}}
{{eqn | r = \frac 1 s
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\cos at}
      | r = \frac 1 s \paren {1 + \frac {a^2} {s^2} }^{-1}
}}
{{eqn | r = \frac 1 s \paren {\frac {s^2} {a^2 + s^2} }
}}
{{eqn | r = \frac s {s^2 + a^2}
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Sine

Let $\sin$ denote the real sine function.
Let $\laptrans f$ denote the Laplace transform of a real function $f$.
Then:
:$\laptrans {\sin at} = \dfrac a {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > 0$.

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

Let $\sin$ denote the real sine function.
Let $\laptrans f$ denote the Laplace transform of a real function $f$.
Then:
:$\laptrans {\sin at} = \dfrac a {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > 0$.

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

Let $\sin$ denote the real sine function.
Let $\laptrans f$ denote the Laplace transform of a real function $f$.
Then:
:$\laptrans {\sin at} = \dfrac a {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > 0$.

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 Sine

Let $\sin$ denote the real sine function.
Let $\laptrans f$ denote the Laplace transform of a real function $f$.
Then:
:$\laptrans {\sin at} = \dfrac a {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \sin \sqrt t
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {\paren {\sqrt t}^{2 n + 1} } {\paren {2 n + 1}!}
      | c = {{Defof|Real Sine Function}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n} {\paren {2 n + 1}!} t^{n + \frac 1 2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\sin \sqrt t}
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {\map \Gamma {n + \frac 3 2} } {\paren {2 n + 1}! s^{n + \frac 3 2} }
      | c = Laplace Transform of Power, Linear Combination of Laplace Transforms
}}
{{eqn | r = \frac 1 {s^{3/2} } \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {\paren {n + \frac 1 2} \map \Gamma {n + \frac 1 2} } {\paren {2 n + 1}! s^n}
      | c = Gamma Difference Equation
}}
{{eqn | r = \frac {\sqrt \pi} {2 s^{3/2} } \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {\paren {2 n + 1} \paren {2 n}!} {2^{2 n} n! \paren {2 n + 1}! s^n}
      | c = Gamma Function of Positive Half-Integer
}}
{{eqn | r = \frac {\sqrt \pi} {2 s^{3/2} } \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n} {2^{2 n} n! s^n}
      | c = 
}}
{{eqn | r = \frac {\sqrt \pi} {2 s^{3/2} } \sum_{n \mathop = 0}^\infty \frac 1 {n!} \paren {-\frac 1 {2^2 s} }^n
      | c = 
}}
{{eqn | r = \dfrac {\sqrt \pi} {2 s^{3/2} } e^{-1/\paren {2^2 s} }
      | c = {{Defof|Exponential Function/Real|subdef = Power Series Expansion|Exponential Function}}
}}
{{eqn | r = \dfrac {\sqrt \pi} {2 s^{3/2} } \map \exp {-\dfrac 1 {4 s} }
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Sine

Let $\sin$ denote the real sine function.
Let $\laptrans f$ denote the Laplace transform of a real function $f$.
Then:
:$\laptrans {\sin at} = \dfrac a {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > 0$.

Proof:
Let $\map y t := \sin \sqrt t$.
Differentiating twice {{WRT|Differentiation}} $t$, we get:
:$(1): \quad 4 t y' ' + 2 y' ' + y = 0$
Let $\map Y s = \laptrans {\map t y}$ be the Laplace transform of $y$.
Then taking the Laplace transform of $(1)$:
{{begin-eqn}}
{{eqn | l = -4 \map {\dfrac \d {\d s} } {\laptrans {\map {y' '} t} } + 2 \laptrans {\map {y'} t} + \laptrans {\map y t}
      | r = 0
      | c = Derivative of Laplace Transform
}}
{{eqn | ll= \leadsto
      | l = -4 \map {\dfrac \d {\d s} } {s^2 \, \map Y s - s \, \map y 0 - \map {y'} 0} + 2 \paren {s \, \map Y s - \map y 0} + \map Y s
      | r = 0
      | c = Laplace Transform of Derivative, Laplace Transform of Second Derivative
}}
{{eqn | ll= \leadsto
      | l = 4 s^2 \, \map {Y'} s - \paren {6 s - 1} \map Y s
      | r = 0
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \map Y s
      | r = \dfrac c {s^{3/2} } \, \map \exp {\dfrac 1 {4 s} }
      | c = solving the differential equation
}}
{{end-eqn}}
For small $t$, we have:
:$\sin \sqrt t \sim \sqrt t$
and:
:$\laptrans {\sqrt t} = \dfrac {\sqrt \pi} {2 s^{3/2} }$
For large $t$, we have:
:$Y \sim \dfrac c {2 s^{3/2} }$
Hence by comparison:
:$c = \dfrac {\sqrt \pi} 2$
Hence:
:$\laptrans {\sin \sqrt t} = \dfrac {\sqrt \pi} {2 s^{3/2} } \map \exp {-\dfrac 1 {4 s} }$
{{qed}}
Theorem: Laplace Transform of Sine

Let $\sin$ denote the real sine function.
Let $\laptrans f$ denote the Laplace transform of a real function $f$.
Then:
:$\laptrans {\sin at} = \dfrac a {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\laptrans {\sin {a t} } } s
      | r = \int_0^{\to +\infty} e^{-s t} \sin {a t} \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \lim_{L \mathop \to \infty} \int_0^L e^{-s t} \sin {a t} \rd t
      | c = {{Defof|Improper Integral}}
}}
{{eqn | r = \lim_{L \mathop \to \infty} \intlimits {\frac {e^{-s t} \paren {-s \sin a t - a \cos a t} } {\paren {-s}^2 + a^2} } 0 L
      | c = Primitive of $e^{a x} \sin b x$
}}
{{eqn | r = \lim_{L \mathop \to \infty} \paren {\dfrac {e^{-s L} \paren {-s \sin a L - a \cos a L} } {s^2 + a^2} - \dfrac {e^{-s \times 0} \paren {-s \, \map \sin {0 \times a} - a \, \map \cos {0 \times a} } } {s^2 + a^2} }
      | c = 
}}
{{eqn | r = \lim_{L \mathop \to \infty} \paren {\dfrac {s \sin 0 + a \cos 0} {s^2 + a^2} - \dfrac {e^{-s L} \paren {s \sin a L + a \cos a L} } {s^2 + a^2} }
      | c = Exponential of Zero and rearranging
}}
{{eqn | r = \dfrac {s \sin 0 + a \cos 0} {s^2 + a^2} - 0
      | c = Exponential Tends to Zero
}}
{{eqn | r = \frac a {s^2 + a^2}
      | c = Sine of Zero is Zero, Cosine of Zero is One
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Sine

Let $\sin$ denote the real sine function.
Let $\laptrans f$ denote the Laplace transform of a real function $f$.
Then:
:$\laptrans {\sin at} = \dfrac a {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {e^{i a t} }
      | r = \frac 1 {s - i a}
      | c = Laplace Transform of Exponential
}}
{{eqn | r = \frac {s + i a} {s^2 + a^2}
      | c = multiplying top and bottom by $s + i a$
}} 
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | l = \laptrans {e^{i a t} }
      | r = \laptrans {\cos a t + i \sin a t}
      | c = Euler's Formula
}}
{{eqn | r = \laptrans {\cos a t} + i \laptrans {\sin a t}
      | c = Linear Combination of Laplace Transforms
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn | l = \laptrans {\sin a t}
      | r = \map \Im {\laptrans {e^{i a t} } }
}}
{{eqn | r = \map \Im {\frac {s + i a} {s^2 + a^2} }
}}
{{eqn | r = \frac a {s^2 + a^2}
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Sine

Let $\sin$ denote the real sine function.
Let $\laptrans f$ denote the Laplace transform of a real function $f$.
Then:
:$\laptrans {\sin at} = \dfrac a {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\sin a t}
      | r = \laptrans {\frac {e^{i a t} - e^{-i a t} } {2 i} }
      | c = Euler's Sine Identity
}}
{{eqn | r = \frac 1 {2 i} \paren {\laptrans {e^{i a t} } - \laptrans {e^{-i a t} } }
      | c = Linear Combination of Laplace Transforms
}}
{{eqn | r = \frac 1 {2 i} \paren {\frac 1 {s - i a} - \frac 1 {s + i a} }
      | c = Laplace Transform of Exponential
}}
{{eqn | r = \frac 1 {2 i} \paren {\frac {s + i a - s + i a} {s^2 + a^2} }
      | c = simplifying
}}
{{eqn | r = \frac 1 {2 i} \paren {\frac {2 i a} {s^2 + a^2} }
      | c = simplifying
}}
{{eqn | r = \frac a {s^2 + a^2}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Sine

Let $\sin$ denote the real sine function.
Let $\laptrans f$ denote the Laplace transform of a real function $f$.
Then:
:$\laptrans {\sin at} = \dfrac a {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > 0$.

Proof:
By definition of the Laplace transform:
:$\ds \laptrans {\sin a t} = \int_0^{\to +\infty} e^{-s t} \sin a t \rd t$
From Integration by Parts:
:$\ds \int f g' \rd t = f g - \int f' g \rd t$
Here:
{{begin-eqn}}
{{eqn | l = f
      | r = \sin a t
}}
{{eqn | ll= \leadsto
      | l = f'
      | r = a \cos a t
      | c = Derivative of $\sin a x$
}}
{{eqn | l = g'
      | r = e^{-s t}
}}
{{eqn | ll= \leadsto
      | l = g
      | r = -\frac 1 s e^{-s t}
      | c = Primitive of $e^{a x}$
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn | n = 1
      | l = \int e^{-s t} \sin a t \rd t
      | r = -\frac 1 s e^{-s t} \sin a t + \frac a s \int e^{-s t} \cos a t \rd t
}}
{{end-eqn}}
Consider:
:$\ds \int e^{-s t} \cos a t \rd t$
Again, using Integration by Parts:
:$\ds \int h j\,' \rd t = h j - \int h' j \rd t$
Here:
{{begin-eqn}}
{{eqn | l = h
      | r = \cos a t
}}
{{eqn | ll= \leadsto
      | l = h'
      | r = -a \sin a t
      | c = Derivative of Cosine Function
}}
{{eqn | l = j\,'
      | r = e^{-s t}
}}
{{eqn | ll= \leadsto
      | l = j
      | r = -\frac 1 s e^{-s t}
      | c = Primitive of Exponential Function
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn | l = \int e^{-s t} \cos a t \rd t
      | r = -\frac 1 s e^{-st} \cos a t - \frac a s \int e^{-s t} \sin a t \rd t
}}
{{end-eqn}}
Substituting this into $(1)$:
{{begin-eqn}}
{{eqn | l = \int e^{-s t} \sin a t \rd t
      | r = -\frac 1 s e^{-s t} \sin a t + \frac a s \paren {-\frac 1 s e^{-s t} \cos a t - \frac a s \int e^{-s t} \sin a t \rd t}
}}
{{eqn | r = -\frac 1 s e^{-s t} \sin a t - \frac a {s^2} e^{-s t} \cos a t - \frac {a^2} {s^2} \int e^{-s t} \sin a t \rd t
}}
{{eqn | ll= \leadsto
      | l = \paren {1 + \frac {a^2} {s^2} } \int e^{-s t} \sin a t \rd t
      | r = -e^{-s t} \paren {\frac 1 s \sin a t + \frac a {s^2} \cos a t}
}}
{{end-eqn}}
Evaluating at $t = 0$ and $t \to +\infty$:
{{begin-eqn}}
{{eqn | l = \paren {1 + \frac {a^2} {s^2} } \laptrans {\sin a t} 
      | r = \intlimits {-e^{-s t} \paren {\frac 1 s \sin a t + \frac a {s^2} \cos a t} } {t \mathop = 0} {t \mathop \to +\infty}
}}
{{eqn | r = 0 - \paren {-1 \paren {\frac 1 s \times 0 + \frac a {s^2} \times 1} }
      | c = Boundedness of Real Sine and Cosine, Complex Exponential Tends to Zero
}}
{{eqn | r = \frac a {s^2}
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\sin a t}
      | r = \frac a {s^2} \paren {1 + \frac {a^2} {s^2} }^{-1}
}}
{{eqn | r = \frac a {s^2} \paren {\frac {s^2} {a^2 + s^2} }
}}
{{eqn | r = \frac a {s^2 + a^2}
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Sine

Let $\sin$ denote the real sine function.
Let $\laptrans f$ denote the Laplace transform of a real function $f$.
Then:
:$\laptrans {\sin at} = \dfrac a {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > 0$.

Proof:
From Laplace Transform of Second Derivative:
:$(1): \quad \laptrans {\map {f' '} t} = s^2 \laptrans {\map f t} - s \, \map f 0 - \map {f'} 0$
under suitable conditions.
Then:
{{begin-eqn}}
{{eqn | l = \map f t
      | r = \sin a t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {f'} t
      | r = a \cos a t
      | c = 
}}
{{eqn | l = \map {f' '} t
      | r = -a^2 \sin a t
      | c = 
}}
{{eqn | l = \map f 0
      | r = 0
      | c = 
}}
{{eqn | l = \map {f'} 0
      | r = a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \laptrans {-a^2 \sin a t}
      | r = s^2 \laptrans {\sin a t} - s \times 0 - a
      | c = from $(1)$, substituting for $\map f t$, $\map {f'} 0$  and $\map f 0$
}}
{{eqn | ll= \leadsto
      | l = -a^2 \laptrans {\sin a t}
      | r = s^2 \laptrans {\sin a t} - a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\sin a t}
      | r = \dfrac a {s^2 + a^2}
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Sum Rule for Derivatives/General Result

Let $\map {f_1} x, \map {f_2} x, \ldots, \map {f_n} x$ be real functions all differentiable.
Then for all $n \in \N_{>0}$:
:$\ds \map {D_x} {\sum_{i \mathop = 1}^n \map {f_i} x} = \sum_{i \mathop = 1}^n \map {D_x} {\map {f_i} x}$

Proof:
The proof proceeds by induction.
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\ds \map {D_x} {\sum_{i \mathop = 1}^n \map {f_i} x} = \sum_{i \mathop = 1}^n \map {D_x} {\map {f_i} x}$
$\map P 1$ is true, as this just says:
:$\map {D_x} {\map {f_1} x} = \map {D_x} {\map {f_1} x}$
which is trivially true.
Theorem: Product Rule for Derivatives/General Result

Let $\map {f_1} x, \map {f_2} x, \ldots, \map {f_n} x$ be real functions differentiable on the open interval $I$.
then:
:$\forall x \in I: \ds \map {D_x} {\prod_{i \mathop = 1}^n \map {f_i} x} = \sum_{i \mathop = 1}^n \paren {\map {D_x} {\map {f_i} x} \prod_{j \mathop \ne i} \map {f_j} x}$

Proof:
Proof by Principle of Mathematical Induction:
For all $n \in \N_{\ge 1}$, let $\map P n$ be the proposition:
:$\ds \map {D_x} {\prod_{i \mathop = 1}^n \map {f_i} x} = \sum_{i \mathop = 1}^n \paren {\map {D_x} {\map {f_i} x} \prod_{j \mathop \ne i} \map {f_j} x}$
$\map P 1$ is true, as this just says:
:$\map {D_x} {\map {f_1} x} = \map {D_x} {\map {f_1} x}$
Theorem: Derivative of Arccotangent Function

:$\dfrac {\map \d {\arccot x} } {\d x} = \dfrac {-1} {1 + x^2}$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = \arccot x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \cot y
      | c = {{Defof|Real Arccotangent}}
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d y}
      | r = -\csc^2 y
      | c = Derivative of Cotangent Function
}}
{{eqn | r = -\paren {1 + \cot^2 y}
      | c = Difference of Squares of Cosecant and Cotangent
}}
{{eqn | r = -\paren {1 + x^2}
      | c = Definition of $x$
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \frac {-1} {1 + x^2}
      | c = Derivative of Inverse Function
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Arccotangent Function

:$\dfrac {\map \d {\arccot x} } {\d x} = \dfrac {-1} {1 + x^2}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {\map \d {\arccot x} } {\d x}
      | r = \map {\frac \d {\d x} } {\frac \pi 2 - \arctan x}
      | c = Tangent of Complement equals Cotangent
}}
{{eqn | r = -\frac 1 {1 + x^2}
      | c = Derivative of Arctangent Function
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Arcsecant Function/Corollary 2

:$\dfrac {\map \d {\arcsec x} } {\d x} = \dfrac 1 {x^2 \sqrt {1 - \frac 1 {x^2} } }$

Proof:
From Derivative of Arcsecant Function:
:$\dfrac {\map \d {\arcsec x} } {\d x} = \dfrac 1 {\size x \sqrt {x^2 - 1} }$
Since for all $x \in \R$, we have $\size x = \sqrt{x^2}$, we can write:
:$\dfrac {\map \d {\arcsec x} } {\d x} = \dfrac 1 {\sqrt {x^2} \sqrt {x^2 - 1} }$
Multiplying the denominator by $1 = \dfrac {\sqrt{x^2} } {\sqrt{x^2} }$ yields:
:$\dfrac {\map \d {\arcsec x} } {\d x} = \dfrac 1 {x^2 \sqrt {1 - \frac 1 {x^2} } }$
{{qed}}
Theorem: Asymptotic Formula for Bernoulli Numbers

The Bernoulli numbers with even index can be approximated by the asymptotic formula:
:$B_{2 n} \sim \paren {-1}^{n + 1} 4 \sqrt {\pi n} \paren {\dfrac n {\pi e} }^{2 n}$
where:
:$B_n$ denotes the $n$th Bernoulli number
:$\sim$ denotes asymptotically equal.

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \frac {B_{2 n} } {\paren {-1}^{n + 1} 4 \sqrt {\pi n} \paren {\frac n {\pi e} }^{2 n} } 
      | r = \lim_{n \mathop \to \infty} \frac {\paren {-1}^{n + 1} \paren {2 n}! \map \zeta {2 n} } {2^{2 n - 1} \pi^{2 n} \paren {-1}^{n + 1} 4 \sqrt {\pi n} \paren {\frac n {\pi e} }^{2 n} }
      | c = Riemann Zeta Function at Even Integers
}}
{{eqn | r = \lim_{n \mathop \to \infty} \frac {\paren {2 n}! \map \zeta {2 n} } {2^{2 n + 1} \sqrt {\pi n} \paren {\frac n e}^{2 n} }
}}
{{eqn | r = \lim_{n \mathop \to \infty} \frac {2 \sqrt {\pi n} \paren {\frac {2 n} e}^{2 n} \map \zeta {2 n} } {2^{2 n + 1} \sqrt {\pi n} \paren {\frac n e}^{2 n} }
      | c = Stirling's Formula
}}
{{eqn | r = \lim_{n \mathop \to \infty} \map \zeta {2 n}
      | c = 
}}
{{eqn | r = 1
      | c =
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Hyperbolic Cotangent Function

:$\map {\dfrac \d {\d x} } {\coth u} = -\csch^2 u \dfrac {\d u} {\d x}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {\coth u}
      | r = \map {\frac \d {\d u} } {\coth u} \frac {\d u} {\d x}
      | c = Chain Rule for Derivatives
}}
{{eqn | r = -\csch^2 u \frac {\d u} {\d x}
      | c = Derivative of Hyperbolic Cotangent
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Hyperbolic Cosecant Function

:$\map {\dfrac \d {\d x} } {\csch u} = -\csch u \coth u \dfrac {\d u} {\d x}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {\csch u}
      | r = \map {\frac \d {\d u} } {\csch u} \frac {\d u} {\d x}
      | c = Chain Rule for Derivatives
}}
{{eqn | r = -\csch u \coth u \frac {\d u} {\d x}
      | c = Derivative of Hyperbolic Cotangent
}}
{{end-eqn}}
{{qed}}