avewright/proofwiki-math huggingface dataset:
Theorem: Cosine of x minus Sine of x/Cosine Form

:$\cos x - \sin x = \sqrt 2 \, \map \cos {x + \dfrac \pi 4}$

Proof:
{{begin-eqn}}
{{eqn | l = \cos x - \sin x
      | r = \sqrt 2 \, \map \sin {x + \dfrac {3 \pi} 4}
      | c = Cosine of x minus Sine of x: Sine Form
}}
{{eqn | r = \sqrt 2 \, \map \cos {\frac \pi 2 - \paren {x + \dfrac {3 \pi} 4} }
      | c = Cosine of Complement equals Sine
}}
{{eqn | r = \sqrt 2 \, \map \cos {\frac \pi 2 - x - \dfrac {3 \pi} 4}
      | c = simplifying
}}
{{eqn | r = \sqrt 2 \, \map \cos {-\frac \pi 4 - x}
      | c = simplifying
}}
{{eqn | r = \sqrt 2 \, \map \cos {x + \frac \pi 4}
      | c = Cosine Function is Even
}}
{{end-eqn}}
{{qed}}
Category:Cosine of x minus Sine of x
ekun1gl18pi8ym2j2y406sjnmmgv58u
Theorem: Power Series Expansion for Exponential of x by Cosine of x

{{begin-eqn}}
{{eqn | l = e^x \cos x
      | r = \sum_{n \mathop = 1}^\infty \frac {2^{n / 2} \, \map \cos {n \pi / 4} x^n} {n!}
      | c = 
}}
{{eqn | r = 1 + x - \frac {x^3} 3 - \frac {x^4} 6 + \cdots
      | c = 
}}
{{end-eqn}}
for all $x \in \R$.

Proof:
Let $\map f x = e^x \cos x$.
By definition of Maclaurin series:
:$(1): \quad \map f x \sim \ds \sum_{n \mathop = 0}^\infty \frac {x^n} {n!} \map {f^{\paren n} } 0$
where $\map {f^{\paren n} } 0$ denotes the $n$th derivative of $f$ {{WRT|Differentiation}} $x$ evaluated at $x = 0$.
It remains to be shown that:
:$\map {f^{\paren n} } 0 = 2^{n / 2} \map \cos {\dfrac {n \pi} 4}$
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\map {f^{\paren n} } x = 2^{n / 2} e^x \map \cos {x + \dfrac {n \pi} 4}$
Theorem: Power Series Expansion for Logarithm of Sine of x

{{begin-eqn}}
{{eqn | l = \ln \size {\sin x}
      | r = \ln \size x - \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n 2^{2 n - 1} B_{2 n} \, x^{2 n} } {n \paren {2 n}!}
      | c = 
}}
{{eqn | r = \ln \size x - \frac {x^2} 6 - \frac {x^4} {180} - \frac {x^6} {2835} + \cdots
      | c = 
}}
{{end-eqn}}
for all $x \in \R$ such that $0 < \size x < \pi$.

Proof:
From Power Series Expansion for Cotangent Function:
{{begin-eqn}}
{{eqn | n = 1
      | l = \cot x
      | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!}
      | c = 
}}
{{eqn | r = \frac 1 x - \frac x 3 - \frac {x^3} {45} - \frac {2 x^5} {945} + \cdots
      | c = 
}}
{{end-eqn}}
for $0 < \size x < \pi$.
From Power Series is Termwise Integrable within Radius of Convergence, $(1)$ can be integrated term by term:
{{begin-eqn}}
{{eqn | l = \int_0^x \cot x \rd x
      | r = \sum_{n \mathop = 0}^\infty \int_0^x \frac {\paren {-1}^{n - 1} 2^{2 n} B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!} \rd x
      | c = 
}}
{{eqn | r = \int_0^x \frac 1 x \rd x + \sum_{n \mathop = 1}^\infty \int_0^x \frac {\paren {-1}^{n - 1} 2^{2 n} B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!} \rd x
      | c = extracting the zeroth term
}}
{{eqn | ll= \leadsto
      | l = \ln \size {\sin x}
      | r = \ln \size x + \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} B_{2 n} \, x^{2 n} } {\paren {2 n} \paren {2 n}!}
      | c = Primitive of $\cot x$, Integral of Power, Primitive of Reciprocal
}}
{{eqn | ll= \leadsto
      | l = \ln \size {\sin x}
      | r = \ln \size x - \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n 2^{2 n - 1} B_{2 n} \, x^{2 n} } {n \paren {2 n}!}
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Power Series Expansion for Logarithm of Cosine of x

{{begin-eqn}}
{{eqn | l = \ln \size {\cos x}
      | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n 2^{2 n - 1} \paren {2^{2 n} - 1} B_{2 n} \, x^{2 n} } {n \paren {2 n}!}
      | c = 
}}
{{eqn | r = -\frac {x^2} 2 - \frac {x^4} {12} - \frac {x^6} {45} - \frac {17 x^8} {2520} - \cdots
      | c = 
}}
{{end-eqn}}
for all $x \in \R$ such that $\size x < \dfrac \pi 2$.

Proof:
From Power Series Expansion for Tangent Function:
{{begin-eqn}}
{{eqn | n = 1
      | l = \tan x
      | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!}
      | c = 
}}
{{eqn | r = x + \frac {x^3} 3 + \frac {2 x^5} {15} + \frac {17 x^7} {315} + \cdots
      | c = 
}}
{{end-eqn}}
for $\size x < \dfrac \pi 2$.
From Power Series is Termwise Integrable within Radius of Convergence, $(1)$ can be integrated term by term:
{{begin-eqn}}
{{eqn | l = \int_0^x \tan x \rd x
      | r = \sum_{n \mathop = 0}^\infty \int_0^x \frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!} \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = -\ln \size {\cos x}
      | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} \, x^{2 n} } {\paren {2 n} \paren {2 n}!}
      | c = Primitive of $\tan x$: Cosine Form, Integral of Power
}}
{{eqn | ll= \leadsto
      | l = \ln \size {\cos x}
      | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n 2^{2 n - 1} \paren {2^{2 n} - 1} B_{2 n} \, x^{2 n} } {n \paren {2 n}!}
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Expectation of Normal Distribution

Let $X \sim N \paren {\mu, \sigma^2}$ for some $\mu \in \R, \sigma \in \R_{> 0}$, where $N$ is the normal distribution.
Then: 
:$\expect X = \mu$

Proof:
From the definition of the normal distribution, $X$ has probability density function:
:$\map {f_X} x = \dfrac 1 {\sigma \sqrt{2 \pi} } \map \exp {-\dfrac {\paren {x - \mu}^2} {2 \sigma^2} }$
From the definition of the expected value of a continuous random variable: 
:$\ds \expect X = \int_{-\infty}^\infty x \map {f_X} x \rd x$
So:
{{begin-eqn}}
{{eqn | l = \expect X
      | r = \frac 1 {\sigma \sqrt {2 \pi} } \int_{-\infty}^\infty x \map \exp {-\frac {\paren {x - \mu}^2} {2 \sigma^2} } \rd x
}}
{{eqn | r = \frac {\sqrt 2 \sigma} {\sigma \sqrt {2 \pi} } \int_{-\infty}^\infty \paren {\sqrt 2 \sigma t + \mu} \map \exp {-t^2} \rd t
      | c = substituting $t = \dfrac {x - \mu} {\sqrt 2 \sigma}$
}}
{{eqn | r = \frac 1 {\sqrt \pi} \paren {\sqrt 2 \sigma \int_{-\infty}^\infty t \map \exp {-t^2} \rd t + \mu \int_{-\infty}^\infty \map \exp {-t^2} \rd t}
}}
{{eqn | r = \frac 1 {\sqrt \pi} \paren {\sqrt 2 \sigma \intlimits {-\frac 1 2 \map \exp {-t^2} } {-\infty} \infty + \mu \sqrt \pi}
      | c = Fundamental Theorem of Calculus, Gaussian Integral
}}
{{eqn | r = \frac {\mu \sqrt \pi} {\sqrt \pi}
      | c = Exponential Tends to Zero and Infinity
}}
{{eqn | r = \mu
}}
{{end-eqn}}
{{qed}}
Theorem: Expectation of Normal Distribution

Let $X \sim N \paren {\mu, \sigma^2}$ for some $\mu \in \R, \sigma \in \R_{> 0}$, where $N$ is the normal distribution.
Then: 
:$\expect X = \mu$

Proof:
By Moment Generating Function of Normal Distribution, the moment generating function of $X$ is given by: 
:$\map {M_X} t = \map \exp {\mu t + \dfrac 1 2 \sigma^2 t^2}$
From Moment in terms of Moment Generating Function: 
:$\expect X = \map {M'_X} 0$
We have: 
{{begin-eqn}}
{{eqn | l = \map {M_X'} t
      | r = \frac \d {\d t} \map \exp {\mu t + \dfrac 1 2 \sigma^2 t^2}
}}
{{eqn | r = \map {\frac \d {\d t} } {\mu t + \frac 1 2 \sigma^2 t^2} \frac \d {\map \d {\mu t + \dfrac 1 2 \sigma^2 t^2} } \map \exp {\mu t + \dfrac 1 2 \sigma^2 t^2}
      | c = Chain Rule for Derivatives
}}
{{eqn | r = \paren {\mu + \sigma^2 t} \map \exp {\mu t + \dfrac 1 2 \sigma^2 t^2}
      | c = Derivative of Power, Derivative of Exponential Function
}}
{{end-eqn}}
Setting $t = 0$: 
{{begin-eqn}}
{{eqn | l = \map {M_X'} 0
      | r = \paren {\mu + 0 \sigma^2} \map \exp {0 \mu + 0 \sigma^2}
}}
{{eqn | r = \mu \exp 0 
}}
{{eqn | r = \mu
      | c = Exponential of Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Power Series Expansion for Logarithm of Tangent of x

{{begin-eqn}}
{{eqn | l = \ln \size {\tan x}
      | r = \ln \size x + \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n - 1} - 1} B_{2 n} \, x^{2 n} } {n \paren {2 n}!}
      | c = 
}}
{{eqn | r = \ln \size x + \frac {x^2} 3 + \frac {7 x^4} {90} + \frac {62 x^6} {2835} + \cdots
      | c = 
}}
{{end-eqn}}
for all $x \in \R$ such that $0 < \size x < \dfrac \pi 2$.

Proof:
From Power Series Expansion for Cosecant Function:
{{begin-eqn}}
{{eqn | l = 2 \csc 2 x
      | r = 2 \sum_{n \mathop = 0}^\infty \dfrac {\paren {-1}^{n - 1} 2 \paren {2^{2 n - 1} - 1} B_{2 n} \paren {2 x}^{2 n - 1} } {\paren {2 n}!}
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = 2 \csc 2 x
      | r = \sum_{n \mathop = 0}^\infty \dfrac {\paren {-1}^{n - 1} 2^{2 n + 1} \paren {2^{2 n - 1} - 1} B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!}
      | c = 
}}
{{end-eqn}}
for $0 < \size {2 x} < \pi$.
From Power Series is Termwise Integrable within Radius of Convergence, $(1)$ can be integrated term by term:
{{begin-eqn}}
{{eqn | l = \int 2 \csc 2 x \rd x
      | r = \sum_{n \mathop = 0}^\infty \int \dfrac {\paren {-1}^{n - 1} 2^{2 n + 1} \paren {2^{2 n - 1} - 1} B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!} \rd x
      | c = 
}}
{{eqn | l = \int 2 \csc 2 x \rd x
      | r = \int \frac 1 x \rd x + \sum_{n \mathop = 1}^\infty \int \dfrac {\paren {-1}^{n - 1} 2^{2 n + 1} \paren {2^{2 n - 1} - 1} B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!} \rd x
      | c = extracting the zeroth term
}}
{{eqn | ll= \leadsto
      | l = \ln \size {\tan x}
      | r = \ln \size x + \sum_{n \mathop = 1}^\infty \dfrac {\paren {-1}^{n - 1} 2^{2 n + 1} \paren {2^{2 n - 1} - 1} B_{2 n} \, x^{2 n} } {\paren {2 n} \paren {2 n}!}
      | c = Primitive of $\csc a x$, Integral of Power, Primitive of Reciprocal
}}
{{eqn | r = \ln \size x + \sum_{n \mathop = 1}^\infty \dfrac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n - 1} - 1} B_{2 n} \, x^{2 n} } {n \paren {2 n}!}
      | c = simplification
}}
{{end-eqn}}
for $0 < \size x < \dfrac \pi 2$.
{{qed}}
Theorem: Power Series Expansion for Logarithm of 1 + x over 1 + x

{{begin-eqn}}
{{eqn | l = \frac {\map \ln {1 + x} } {1 + x}
      | r = \sum_{n \mathop = 1}^\infty \paren {-1}^{n + 1} H_n x^n
      | c = 
}}
{{eqn | r = x - H_2 x^2 + H_3 x^3 - H_4 x^4 + \cdots
      | c = 
}}
{{end-eqn}}
where $H_n$ denotes the $n$th harmonic number:
:$H_n = \ds \sum_{r \mathop = 1}^n \dfrac 1 r = 1 + \dfrac 1 2 + \dfrac 1 3 \cdots + \dfrac 1 r$
valid for all $x \in \R$ such that $\size x < 1$.

Proof:
Let $\map f x = \dfrac {\map \ln {1 + x} } {1 + x}$.
By definition of Maclaurin series:
:$(1): \quad \map f x \sim \ds \sum_{n \mathop = 0}^\infty \frac {x^n} {n!} \map {f^{\paren n} } 0$
where $\map {f^{\paren n} } 0$ denotes the $n$th derivative of $f$ {{WRT|Differentiation}} $x$ evaluated at $x = 0$.
From Nth Derivative of Natural Logarithm by Reciprocal:
:$\dfrac {\d^n} {\d x^n} \dfrac {\map \ln {1 + x} } {1 + x} = \paren {-1}^{n + 1} n! \dfrac {H_n - \map \ln {1 + x} } {\paren {1 + x}^{n + 1} }$
The result follows by setting $x = 0$ and substituting for $\map {f^{\paren n} } 0$ in $(1)$.
From the Ratio Test, we have:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \size {\frac {a_{n + 1} } {a_n} }
      | r = \lim_{n \mathop \to \infty} \size {-\frac {H_{n + 1} x^{n + 1} } {H_n x^n} }
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {-\frac {\paren {1 + \frac 1 2 + \frac 1 3 \cdots + \frac 1 n + \frac 1 {n + 1} } x^{n + 1} } {\paren {1 + \frac 1 2 + \frac 1 3 \cdots + \frac 1 n} x^n} }
      | c = {{Defof|Harmonic Numbers}}
}}
{{eqn | r = \lim_{n \mathop \to \infty} x \paren {1 + \frac 1 {\paren {n + 1} \paren {1 + \frac 1 2 + \frac 1 3 \cdots + \frac 1 n} } }
      | c = 
}}
{{eqn | r = x
      | c = 
}}
{{end-eqn}}
If $\size x < 1 $, then $\ds \sum_{n \mathop = 1}^\infty \paren {-1}^{n + 1} H_n x^n$ converges absolutely.
{{qed}}
Theorem: Derivative of Logarithm over Power

:$\dfrac \d {\d x} \dfrac {\ln x} {x^n} = \dfrac {1 - n \ln x} {x^{n + 1} }$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac \d {\d x} \dfrac {\ln x} {x^n}
      | r = \dfrac \d {\d x} x^{-n} \ln x
      | c = 
}}
{{eqn | r = \ln x \dfrac \d {\d x} x^{-n} + x^{-n} \dfrac \d {\d x} \ln x
      | c = Product Rule for Derivatives
}}
{{eqn | r = - n x^{-n - 1} \ln x + x^{-n} \dfrac 1 x
      | c = Primitive of Reciprocal, Primitive of Power
}}
{{eqn | r = -n x^{-n - 1} \ln x + x^{-n - 1}
      | c = 
}}
{{eqn | r = \frac {1 - n \ln x} {x^{n + 1} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Derivatives involving Logarithm Functions
Category:Logarithms
r3jya6w77eafud5obhr44jwqkwi4hwr
Theorem: Nth Derivative of Natural Logarithm by Reciprocal

:$\dfrac {\d^n} {\d x^n} \dfrac {\ln x} x = \paren {-1}^{n + 1} n! \dfrac {H_n - \ln x} {x^{n + 1} }$
where $H_n$ denotes the $n$th harmonic number:
:$H_n = \ds \sum_{r \mathop = 1}^n \dfrac 1 r = 1 + \dfrac 1 2 + \dfrac 1 3 + \cdots + \dfrac 1 r$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{> 0}$, let $\map P n$ be the proposition:
:$\dfrac {\d^n} {\d x^n} \dfrac {\ln x} x = \paren {-1}^{n + 1} n! \dfrac {H_n - \ln x} {x^{n + 1} }$
Theorem: Variance of Normal Distribution

Let $X \sim N \paren {\mu, \sigma^2}$ for some $\mu \in \R, \sigma \in \R_{> 0}$, where $N$ is the normal distribution.
Then: 
:$\var X = \sigma^2$

Proof:
From the definition of the normal distribution, $X$ has probability density function:
:$\map {f_X} x = \dfrac 1 {\sigma \sqrt {2 \pi} } \map \exp {-\dfrac {\paren {x - \mu}^2} {2 \sigma^2} }$
From Variance as Expectation of Square minus Square of Expectation: 
:$\ds \var X = \int_{-\infty}^\infty x^2 \map {f_X} x \rd x - \paren {\expect X}^2$
So:
{{begin-eqn}}
{{eqn | l = \var X
      | r = \frac 1 {\sigma \sqrt {2 \pi} } \int_{-\infty}^\infty x^2 \map \exp {-\frac {\paren {x - \mu}^2} {2 \sigma^2} } \rd x - \mu^2
      | c = Expectation of Normal Distribution
}}
{{eqn | r = \frac {\sqrt 2 \sigma} {\sigma \sqrt {2 \pi} } \int_{-\infty}^\infty \paren {\sqrt 2 \sigma t + \mu}^2 \map \exp {-t^2} \rd t - \mu^2
      | c = substituting $t = \dfrac {x - \mu} {\sqrt 2 \sigma}$
}}
{{eqn | r = \frac 1 {\sqrt \pi} \paren {2 \sigma^2 \int_{-\infty}^\infty t^2 \map \exp {-t^2} \rd t + 2 \sqrt 2 \sigma \mu \int_{-\infty}^\infty t \map \exp {-t^2} \rd t + \mu^2 \int_{-\infty}^\infty \map \exp {-t^2} \rd t} - \mu^2
}}
{{eqn | r = \frac 1 {\sqrt \pi} \paren {2 \sigma^2 \int_{-\infty}^\infty t^2 \map \exp {-t^2} \rd t + 2 \sqrt 2 \sigma \mu \intlimits {-\frac 1 2 \map \exp {-t^2} } {-\infty} \infty + \mu^2 \sqrt \pi} - \mu^2
      | c = Fundamental Theorem of Calculus, Gaussian Integral
}}
{{eqn | r = \frac 1 {\sqrt \pi} \paren {2 \sigma^2 \int_{-\infty}^\infty t^2 \map \exp {-t^2} \rd t + 2\sqrt 2 \sigma \mu \cdot 0} + \mu^2 - \mu^2
      | c = Exponential Tends to Zero and Infinity
}}
{{eqn | r = \frac {2 \sigma^2} {\sqrt \pi} \int_{-\infty}^\infty t^2 \map \exp {-t^2} \rd t
}}
{{eqn | r = \frac {2 \sigma^2} {\sqrt \pi} \paren {\intlimits {-\frac t 2 \map \exp {-t^2} } {-\infty} \infty + \frac 1 2 \int_{-\infty}^\infty \map \exp {-t^2} \rd t}
      | c = Integration by Parts
}}
{{eqn | r = \frac {2 \sigma^2} {\sqrt \pi} \cdot \frac 1 2 \int_{-\infty}^\infty \map \exp {-t^2} \rd t
      | c = Exponential Tends to Zero and Infinity
}}
{{eqn | r = \frac{2 \sigma^2 \sqrt \pi} {2 \sqrt \pi}
      | c = Gaussian Integral
}}
{{eqn | r = \sigma^2
}}
{{end-eqn}}
{{qed}}
Theorem: Variance of Normal Distribution

Let $X \sim N \paren {\mu, \sigma^2}$ for some $\mu \in \R, \sigma \in \R_{> 0}$, where $N$ is the normal distribution.
Then: 
:$\var X = \sigma^2$

Proof:
By Moment Generating Function of Normal Distribution, the moment generating function of $X$ is given by: 
:$\map {M_X} t = \map \exp {\mu t + \dfrac 1 2 \sigma^2 t^2}$
From Variance as Expectation of Square minus Square of Expectation: 
:$\var X = \expect {X^2} - \paren {\expect X}^2$
From Moment Generating Function of Normal Distribution: Second Moment: 
:$\map { {M_X}' '} t = \paren {\sigma^2 + \paren {\mu + \sigma^2 t}^2 } \map \exp {\mu t + \dfrac 1 2 \sigma^2 t^2}$
From Moment in terms of Moment Generating Function, we also have: 
:$\expect {X^2} = \map { {M_X}' '} 0$
Setting $t = 0$, we obtain the second moment: 
{{begin-eqn}}
{{eqn  | l = \map {M' '_X} 0 
       | r = \expect {X^2}
}}
{{eqn | r = \paren {\sigma^2 + \paren {\mu + \sigma^2 0}^2 } \map \exp {\mu 0 + \dfrac 1 2 \sigma^2 0^2}
}}
{{eqn | r = \paren {\sigma^2 + \mu^2 } \exp 0 
}}
{{eqn | r = \sigma^2 + \mu^2
      | c = Exponential of Zero
}}
{{end-eqn}}
So: 
{{begin-eqn}}
{{eqn | l = \var X
      | r = \sigma^2 + \mu^2 - \paren {\expect X}^2
}}
{{eqn | r = \sigma^2 + \mu^2 - \mu^2
      | c = Expectation of Normal Distribution
}}
{{eqn | r = \sigma^2
}}
{{end-eqn}}
{{qed}}
Theorem: Variance as Expectation of Square minus Square of Expectation/Continuous

Let $X$ be a continuous random variable.
Then the variance of $X$ can be expressed as:
:$\var X = \expect {X^2} - \paren {\expect X}^2$
That is, it is the expectation of the square of $X$ minus the square of the expectation of $X$.

Proof:
Let $\mu = \expect X$. 
Let $X$ have probability density function $f_X$. 
As $f_X$ is a probability density function: 
:$\ds \int_{-\infty}^\infty \map {f_X} x \rd x = \Pr \paren {-\infty < X < \infty} = 1$
Then:
{{begin-eqn}}
{{eqn	| l = \var X
	| r = \expect {\paren {X - \mu}^2}
	| c = {{Defof|Variance of Continuous Random Variable}}
}}
{{eqn	| r = \int_{-\infty}^\infty \paren {X - \mu}^2 \map {f_X} x \rd x
	| c = {{Defof|Expectation of Continuous Random Variable}}
}}
{{eqn	| r = \int_{-\infty}^\infty \paren {x^2 - 2 \mu x + \mu^2} \map {f_X} x \rd x
}}
{{eqn	| r = \int_{-\infty}^\infty x^2 \map {f_X} x \rd x - 2 \mu \int_{-\infty}^\infty x f_X \paren x \rd x + \mu^2 \int_{-\infty}^\infty \map {f_X} x \rd x
}}
{{eqn	| r = \expect {X^2} - 2 \mu^2 + \mu^2
	| c = {{Defof|Expectation of Continuous Random Variable}}
}}
{{eqn	| r = \expect {X^2} - \mu^2
}}
{{eqn	| r = \expect {X^2} - \paren {\expect X}^2
}}
{{end-eqn}}
{{qed}}
Theorem: Variance as Expectation of Square minus Square of Expectation/Discrete

Let $X$ be a discrete random variable.
Then the variance of $X$ can be expressed as:
:$\var X = \expect {X^2} - \paren {\expect X}^2$
That is, it is the expectation of the square of $X$ minus the square of the expectation of $X$.

Proof:
We let $\mu = \expect X$, and take the expression for variance:
:$\var X := \ds \sum_{x \mathop \in \Img X} \paren {x - \mu}^2 \map \Pr {X = x}$
Then:
{{begin-eqn}}
{{eqn | l = \var X
      | r = \sum_x \paren {x^2 - 2 \mu x + \mu^2} \map \Pr {X = x}
      | c = 
}}
{{eqn | r = \sum_x x^2 \map \Pr {X = x} - 2 \mu \sum_x x \map \Pr {X = x} + \mu^2 \sum_x \map \Pr {X = x}
      | c = 
}}
{{eqn | r = \sum_x x^2 \map \Pr {X = x} - 2 \mu \sum_x x \map \Pr {X = x} + \mu^2
      | c = {{Defof|Probability Mass Function}}: $\ds \sum_x \map \Pr {X = x} = 1$
}}
{{eqn | r = \sum_x x^2 \map \Pr {X = x} - 2 \mu^2  + \mu^2
      | c = {{Defof|Expectation}}: $\ds \sum_x x \map \Pr {X = x} = \mu$
}}
{{eqn | r = \sum_x x^2 \map \Pr {X = x} - \mu^2
      | c = 
}}
{{end-eqn}}
Hence the result, from $\mu = \expect X$.
{{qed}}
Theorem: Reversion of Power Series

Let $\ds y = \sum_{n \mathop = 1}^\infty c_n x^n$ be a power series.
Then:
:$\ds x = \sum_{n \mathop = 1}^\infty C_n y^n$
is also a power series, where:
{{begin-eqn}}
{{eqn | l = c_1 C_1
      | r = 1
}}
{{eqn | l = {c_1}^3 C_2
      | r = -c_2
}}
{{eqn | l = {c_1}^5 C_3
      | r = 2 {c_2}^2 - c_1 c_3
}}
{{eqn | l = {c_1}^7 C_4
      | r = 5 c_1 c_2 c_3 - 5 {c_2}^2 - {c_1}^2 c_4
}}
{{eqn | l = {c_1}^9 C_5
      | r = 6 {c_1}^2 c_2 c_4 + 3 {c_1}^2 {c_3}^2 - {c_1}^3 c_5 + 14 {c_2}^4 - 21 c_1 {c_2}^2 c_3
}}
{{eqn | l = {c_1}^{11} C_6
      | r = 7 {c_1}^3 c_2 c_5 + 84 c_1 {c_2}^3 c_3 + 7 {c_1}^3 c_3 c_4 - 28 {c_1}^2 c_2 {c_3}^2 - {c_1}^4 c_6 - 28 {c_1}^2 {c_2}^2 c_4 - 42 {c_2}^5
}}
{{eqn | l = {c_1}^{13} C_7
      | r = 8 {c_1}^4 c_2 c_6 + 8 {c_1}^4 c_3 c_5 + 4 {c_1}^4 {c_4}^2 + 120 {c_1}^2 {c_2}^3 c_4 + 180 {c_1}^2 {c_2}^2 {c_3}^2 + 132 {c_2}^6 - {c_1}^5 c_7 - 36 {c_1}^3 {c_2}^2 c_5 - 72 {c_1}^3 c_2 c_3 c_4 - 12 {c_1}^3 {c_3}^3 - 330 c_1 {c_2}^4 c_3
}}
{{end-eqn}}
{{expand|How are $C_n$ defined for $n\ge 7$? I am even not able to predicate a general term.}}
A derivation of the explicit formula for the $n$th term is given by:
:$\ds C_n = \dfrac 1 {n {c_1}^n} \sum_{s, t, u, \cdots} \paren {-1}^{s + t + u + \cdots} \dfrac {n \paren {n + 1} \cdots \paren {n - 1 + s + t + u + \cdots} } {s! \, t! \, u! \ldots} \paren {\dfrac {c_2} {c_1} }^s \paren {\dfrac {c_3} {c_1} }^t \cdots$
where $ s + 2 t + 3 u + \cdots = n - 1$.

Proof:
{{ProofWanted}}
Plugging:
:$\ds x = \sum_{n \mathop = 1}^\infty C_n y^n$
into:
:$\ds y = \sum_{n \mathop = 1}^\infty c_n x^n$
the following equation is obtained
:$y = c_1 C_1 y + \paren {c_2 C_1^2 + c_1 C_2} y^2 + \paren {c_3 C_1^3 + 2 c_2 C_1 C_2 + c_1 C_3} y^3 + \paren {3 c_3 C_1^2 C_2 + c_2 C_2^2 + c_2 C_1 C_3} + \cdots$
Equating coefficients then gives the formula.
{{Handwaving}}
{{qed}}
Theorem: Expectation of Continuous Uniform Distribution

Let $a, b \in \R$ such that $a < b$.
Let $X \sim \ContinuousUniform a b$ be the continuous uniform distribution over $\closedint a b$. 
Then: 
:$\expect X = \dfrac {a + b} 2$

Proof:
From the definition of the continuous uniform distribution, $X$ has probability density function: 
:$\map {f_X} x = \begin {cases} \dfrac 1 {b - a} & : a \le x \le b \\ 0 & : \text {otherwise} \end {cases}$
From the definition of the expected value of a continuous random variable: 
:$\ds \expect X = \int_{-\infty}^\infty x \map {f_X} x \rd x$
So:
{{begin-eqn}}
{{eqn | l = \expect X
      | r = \int_{-\infty}^a 0 x \rd x + \int_a^b \frac x {b - a} \rd x + \int_b^\infty 0 x \rd x
}}
{{eqn | r = \intlimits {\frac {x^2} {2 \paren {b - a} } } a b
      | c = Primitive of Power, Fundamental Theorem of Calculus
}}
{{eqn | r = \frac {b^2 - a^2} {2 \paren {b - a} }
}}
{{eqn | r = \frac {\paren {b - a} \paren {b + a} } {2 \paren {b - a} }
      | c = Difference of Two Squares
}}
{{eqn | r = \frac {a + b} 2
}}
{{end-eqn}}
{{qed}}
Theorem: Variance of Continuous Uniform Distribution

Let $a, b \in \R$ such that $a < b$.
Let $X \sim \ContinuousUniform a b$ be the continuous uniform distribution over $\closedint a b$. 
Then: 
:$\var X = \dfrac {\paren {b - a}^2} {12}$

Proof:
From the definition of the continuous uniform distribution, $X$ has probability density function: 
:$\map {f_X} x = \begin{cases} \dfrac 1 {b - a} & a \le x \le b \\ 0 & \text{otherwise} \end{cases}$
From Variance as Expectation of Square minus Square of Expectation: 
:$\ds \var X = \int_{-\infty}^\infty x^2 \map {f_X} x \rd x - \paren {\expect X}^2$
So:
{{begin-eqn}}
{{eqn | l = \var X
      | r = \int_{-\infty}^a 0 x^2 \rd x + \int_a^b \frac {x^2} {b - a} \rd x + \int_b^\infty 0 x^2 \rd x - \frac {\paren {a + b}^2} 4
      | c = Expectation of Continuous Uniform Distribution
}}
{{eqn | r = \intlimits {\frac {x^3} {3 \paren {b - a} } } a b - \frac {\paren {a + b}^2} 4 
      | c = Primitive of Power, Fundamental Theorem of Calculus
}}
{{eqn | r = \frac {b^3 - a^3} {3 \paren {b - a} } - \frac {\paren {a + b}^2} 4 
}}
{{eqn | r = \frac {4 \paren {b - a} \paren {a^2 + a b + b^2} } {12 \paren {b - a} } - \frac {3 \paren {a + b}^2} {12}
      | c = Difference of Two Cubes
}}
{{eqn | r = \frac {4 a^2 + 4 a b + 4 b^2 - 3 a^2 - 6 a b - 3 b^2} {12}
      | c = Square of Sum
}}
{{eqn | r = \frac {b^2 - 2 a b + a^2} {12}
}}
{{eqn | r = \frac {\paren {b - a}^2} {12}
      | c = Square of Difference
}}
{{end-eqn}}
{{qed}}