avewright/proofwiki-math huggingface dataset:
Theorem: Integral over 2 pi of Sine of m x by Sine of n x

Let $m, n \in \Z$ be integers.
Let $\alpha \in \R$ be a real number.
Then:
:$\ds \int_\alpha^{\alpha + 2 \pi} \sin m x \sin n x \rd x = \begin {cases} 0 & : m \ne n \\ \pi & : m = n \end {cases}$
That is:
:$\ds \int_\alpha^{\alpha + 2 \pi} \sin m x \sin n x \rd x = \pi \delta_{m n}$
where $\delta_{m n}$ is the Kronecker delta.

Proof:
Let $m \ne n$.
{{begin-eqn}}
{{eqn | l = \int \sin m x \sin n x \rd x
      | r = \frac {\sin \paren {m - n} x} {2 \paren {m - n} } - \frac {\sin \paren {m + n} x} {2 \paren {m + n} } + C
      | c = Primitive of $\sin m x \sin n x$
}}
{{eqn | ll= \leadsto
      | l = \int_\alpha^{\alpha + 2 \pi} \sin m x \sin n x \rd x
      | r = \intlimits {\frac {\sin \paren {m - n} x} {2 \paren {m - n} } - \frac {\sin \paren {m + n} x} {2 \paren {m + n} } } \alpha {\alpha + 2 \pi}
      | c = 
}}
{{eqn | r = \paren {\frac {\sin \paren {\paren {m - n} \paren {\alpha + 2 \pi} } } {2 \paren {m - n} } - \frac {\sin \paren {\paren {m + n} \paren {\alpha + 2 \pi} } } {2 \paren {m + n} } }
      | c = 
}}
{{eqn | o = 
      | ro= -
      | r = \paren {\frac {\sin \paren {m - n} \alpha} {2 \paren {m - n} } - \frac {\sin \paren {m + n} \alpha} {2 \paren {m + n} } }
      | c = 
}}
{{eqn | r = \paren {\frac {\sin \paren {m - n} \alpha} {2 \paren {m - n} } - \frac {\sin \paren {m + n} \alpha} {2 \paren {m + n} } }
      | c = {{Corollary|Sine of Angle plus Full Angle}}
}}
{{eqn | o = 
      | ro= -
      | r = \paren {\frac {\sin \paren {m - n} \alpha} {2 \paren {m - n} } - \frac {\sin \paren {m + n} \alpha} {2 \paren {m + n} } }
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
When $m = n$ we have:
{{begin-eqn}}
{{eqn | l = \int \sin m x \sin m x \rd x
      | r = \int \sin^2 m x \rd x
      | c = 
}}
{{eqn | r = \frac x 2 - \frac {\sin 2 m x} {4 m} + C
      | c = Primitive of $\sin^2 m x$
}}
{{eqn | ll= \leadsto
      | l = \int_\alpha^{\alpha + 2 \pi} \sin m x \sin m x \rd x
      | r = \intlimits {\frac x 2 - \frac {\sin 2 m x} {4 m} } \alpha {\alpha + 2 \pi}
      | c = 
}}
{{eqn | r = \paren {\frac {\alpha + 2 \pi} 2 - \frac {\sin \paren {2 m \paren {\alpha + 2 \pi} } } {4 m} } - \paren {\frac \alpha 2 - \frac {\sin 2 m \alpha} {4 m} }
      | c = 
}}
{{eqn | r = \paren {\frac {\alpha + 2 \pi} 2 - \frac {\sin 2 m \alpha} {4 m} } - \paren {\frac \alpha 2 - \frac {\sin 2 m \alpha} {4 m} }
      | c = {{Corollary|Sine of Angle plus Full Angle}}
}}
{{eqn | r = \frac {\alpha + 2 \pi - \alpha} 2
      | c = 
}}
{{eqn | r = \pi
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Integral over 2 pi of Cosine of m x by Cosine of n x

Let $m, n \in \Z$ be integers.
Let $\alpha \in \R$ be a real number.
Then:
:$\ds \int_\alpha^{\alpha + 2 \pi} \cos m x \cos n x \rd x = \begin {cases} 0 & : m \ne n \\ \pi & : m = n \end {cases}$
That is:
:$\ds \int_\alpha^{\alpha + 2 \pi} \cos m x \cos n x \rd x = \pi \delta_{m n}$
where $\delta_{m n}$ is the Kronecker delta.

Proof:
Let $m \ne n$.
{{begin-eqn}}
{{eqn | l = \int \cos m x \cos n x \rd x
      | r = \frac {\sin \paren {m - n} x} {2 \paren {m - n} } + \frac {\sin \paren {m + n} x} {2 \paren {m + n} } + C
      | c = Primitive of $\cos m x \cos n x$
}}
{{eqn | ll= \leadsto
      | l = \int_\alpha^{\alpha + 2 \pi} \cos m x \cos n x \rd x
      | r = \intlimits {\frac {\sin \paren {m - n} x} {2 \paren {m - n} } + \frac {\sin \paren {m + n} x} {2 \paren {m + n} } } \alpha {\alpha + 2 \pi}
      | c = 
}}
{{eqn | r = \paren {\frac {\sin \paren {\paren {m - n} \paren {\alpha + 2 \pi} } } {2 \paren {m - n} } + \frac {\sin \paren {\paren {m + n} \paren {\alpha + 2 \pi} } } {2 \paren {m + n} } }
      | c = 
}}
{{eqn | o = 
      | ro= -
      | r = \paren {\frac {\sin \paren {m - n} \alpha} {2 \paren {m - n} } + \frac {\sin \paren {m + n} \alpha} {2 \paren {m + n} } }
      | c = 
}}
{{eqn | r = \paren {\frac {\sin \paren {m - n} \alpha} {2 \paren {m - n} } + \frac {\sin \paren {m + n} \alpha} {2 \paren {m + n} } }
      | c = {{Corollary|Sine of Angle plus Full Angle}}
}}
{{eqn | o = 
      | ro= -
      | r = \paren {\frac {\sin \paren {m - n} \alpha} {2 \paren {m - n} } + \frac {\sin \paren {m + n} \alpha} {2 \paren {m + n} } }
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
When $m = n$ we have:
{{begin-eqn}}
{{eqn | l = \int \cos m x \cos m x \rd x
      | r = \int \cos^2 m x \rd x
      | c = 
}}
{{eqn | r = \frac x 2 + \frac {\sin 2 m x} {4 m} + C
      | c = Primitive of $\cos^2 m x$
}}
{{eqn | ll= \leadsto
      | l = \int_\alpha^{\alpha + 2 \pi} \cos m x \cos m x \rd x
      | r = \intlimits {\frac x 2 + \frac {\sin 2 m x} {4 m} } \alpha {\alpha + 2 \pi}
      | c = 
}}
{{eqn | r = \paren {\frac {\alpha + 2 \pi} 2 + \frac {\map \sin {2 m \paren {\alpha + 2 \pi} } } {4 m} } - \paren {\frac \alpha 2 + \frac {\sin 2 m \alpha} {4 m} }
      | c = 
}}
{{eqn | r = \paren {\frac {\alpha + 2 \pi} 2 + \frac {\sin 2 m \alpha} {4 m} } - \paren {\frac \alpha 2 + \frac {\sin 2 m \alpha} {4 m} }
      | c = {{Corollary|Sine of Angle plus Full Angle}}
}}
{{eqn | r = \frac {\alpha + 2 \pi - \alpha} 2
      | c = 
}}
{{eqn | r = \pi
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Integral over 2 pi of Sine of m x by Cosine of n x

Let $m, n \in \Z$ be integers.
Let $\alpha \in \R$ be a real number.
Then:
:$\ds \int_\alpha^{\alpha + 2 \pi} \sin m x \cos n x \rd x = 0$

Proof:
Let $m \ne n$.
{{begin-eqn}}
{{eqn | l = \int \sin m x \cos n x \rd x
      | r = \frac {-\map \cos {m - n} x} {2 \paren {m - n} } - \frac {\map \cos {m + n} x} {2 \paren {m + n} } + C
      | c = Primitive of $\sin m x \cos n x$
}}
{{eqn | ll= \leadsto
      | l = \int_\alpha^{\alpha + 2 \pi} \sin m x \cos n x \rd x
      | r = \intlimits {\frac {-\map \cos {m - n} x} {2 \paren {m - n} } - \frac {\map \cos {m + n} x} {2 \paren {m + n} } } \alpha {\alpha + 2 \pi}
      | c = 
}}
{{eqn | r = \paren {\frac {-\map \cos {\paren {m - n} \paren {\alpha + 2 \pi} } } {2 \paren {m - n} } - \frac {\map \cos {\paren {m + n} \paren {\alpha + 2 \pi} } } {2 \paren {m + n} } }
      | c = 
}}
{{eqn | o = 
      | ro= -
      | r = \paren {\frac {-\map \cos {m - n} \alpha} {2 \paren {m - n} } - \frac {\map \cos {m + n} \alpha} {2 \paren {m + n} } }
      | c = 
}}
{{eqn | r = \paren {\frac {-\map \cos {m - n} \alpha} {2 \paren {m - n} } - \frac {\map \cos {m + n} \alpha} {2 \paren {m + n} } }
      | c = {{Corollary|Cosine of Angle plus Full Angle}}
}}
{{eqn | o = 
      | ro= -
      | r = \paren {\frac {-\map \cos {m - n} \alpha} {2 \paren {m - n} } - \frac {\map \cos {m + n} \alpha} {2 \paren {m + n} } }
      | c = 
}}
{{eqn | r = 0
      | c = after simplification
}}
{{end-eqn}}
When $m = n$ we have:
{{begin-eqn}}
{{eqn | l = \int \sin m x \cos m x \rd x
      | r = \frac {\sin^2 m x} {2 m} + C
      | c = Primitive of $\sin m x \cos m x$
}}
{{eqn | ll= \leadsto
      | l = \int_\alpha^{\alpha + 2 \pi} \sin m x \cos m x \rd x
      | r = \intlimits {\frac {\sin^2 m x} {2 m} } \alpha {\alpha + 2 \pi}
      | c = 
}}
{{eqn | r = \frac {\map {\sin^2} {m \paren {\alpha + 2 \pi} } } {2 m} - \frac {\sin^2 m \alpha} {2 m}
      | c = 
}}
{{eqn | r = \frac {\sin^2 m \alpha} {2 m} - \frac {\sin^2 m \alpha} {2 m}
      | c = {{Corollary|Cosine of Angle plus Full Angle}}
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Integral over 2 pi of Sine of n x

Let $m \in \Z$ be an integer.
Then:
:$\ds \int_\alpha^{\alpha + 2 \pi} \sin m x \rd x = 0$

Proof:
Let $m \ne n$.
{{begin-eqn}}
{{eqn | l = \int \sin m x \rd x
      | r = -\frac {\cos m x} m + C
      | c = Primitive of $\sin m x$
}}
{{eqn | ll= \leadsto
      | l = \int_\alpha^{\alpha + 2 \pi} \sin m x \rd x
      | r = \intlimits {-\frac {\cos m x} m} \alpha {\alpha + 2 \pi}
      | c = 
}}
{{eqn | r = \paren {-\frac {\map \cos {m \paren {\alpha + 2 \pi} } } m} - \paren {-\frac {\cos m \alpha} a}
      | c = 
}}
{{eqn | r = \paren {-\frac {\cos m \alpha} m} - \paren {-\frac {\cos m \alpha} a}
      | c = {{Corollary|Cosine of Angle plus Full Angle}}
}}
{{eqn | r = 0
      | c = after simplification
}}
{{end-eqn}}
{{qed|lemma}}
Let $m = 0$.
{{begin-eqn}}
{{eqn | l = \int \sin 0 x \rd x
      | r = \int 0 \rd x
      | c = Sine of Zero is Zero
}}
{{eqn | ll= \leadsto
      | l = \int_\alpha^{\alpha + 2 \pi} \sin 0 x \rd x
      | r = \bigintlimits 0 \alpha {\alpha + 2 \pi}
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Integral over 2 pi of Cosine of n x

Let $m \in \Z$ be an integer.
Then:
:$\ds \int_\alpha^{\alpha + 2 \pi} \cos m x \rd x = \begin {cases} 0 & : m \ne 0 \\ 2 \pi & : m = 0 \end {cases}$

Proof:
Let $m \ne 0$.
{{begin-eqn}}
{{eqn | l = \int \cos m x \rd x
      | r = \frac {\sin m x} m + C
      | c = Primitive of $\cos m x$
}}
{{eqn | ll= \leadsto
      | l = \int_\alpha^{\alpha + 2 \pi} \cos m x \rd x
      | r = \intlimits {\frac {\sin m x} m} \alpha {\alpha + 2 \pi}
      | c = 
}}
{{eqn | r = \paren {\frac {\map \sin {m \paren {\alpha + 2 \pi} } } m} - \paren {\frac {\sin m \alpha} m}
      | c = 
}}
{{eqn | r = \paren {\frac {\sin m \alpha} m} - \paren {\frac {\sin m \alpha} m}
      | c = {{Corollary|Sine of Angle plus Full Angle}}
}}
{{eqn | r = 0 - 0
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
Let $m = 0$.
{{begin-eqn}}
{{eqn | l = \int \cos 0 x \rd x
      | r = \int 1 \rd x
      | c = Cosine of Zero is One
}}
{{eqn | r = x + C
      | c = Primitive of Constant
}}
{{eqn | ll= \leadsto
      | l = \int_\alpha^{\alpha + 2 \pi} \cos 0 x \rd x
      | r = \bigintlimits x \alpha {\alpha + 2 \pi}
      | c = 
}}
{{eqn | r = \alpha + 2 \pi - \alpha
      | c = 
}}
{{eqn | r = 2 \pi
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Coefficients of Cosine Terms in Convergent Trigonometric Series

Let $\map S x$ be a trigonometric series which converges to $\map f x$ on the interval $\openint \alpha {\alpha + 2 \pi}$:
:$\map f x = \dfrac {a_0} 2 + \ds \sum_{m \mathop = 1}^\infty \paren {a_m \cos m x + b_m \sin m x}$
Then:
:$\forall n \in \Z_{\ge 0}: a_n = \dfrac 1 \pi \ds \int_\alpha^{\alpha + 2 \pi} \map f x \cos n x \rd x$

Proof:
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \dfrac {a_0} 2 + \sum_{m \mathop = 1}^\infty \paren {a_m \cos m x + b_m \sin m x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int_\alpha^{\alpha + 2 \pi} \map f x \cos n x \rd x
      | r = \int_\alpha^{\alpha + 2 \pi} \paren {\dfrac {a_0} 2 + \sum_{m \mathop = 1}^\infty \paren {a_m \cos m x + b_m \sin m x} } \cos n x \rd x
      | c = 
}}
{{eqn | r = \int_\alpha^{\alpha + 2 \pi} \dfrac {a_0} 2 \cos n x \rd x
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \sum_{m \mathop = 1}^\infty \paren {\int_\alpha^{\alpha + 2 \pi} \paren {a_m \cos m x + b_m \sin m x} \cos n x \rd x}
      | c = 
}}
{{eqn | r = \frac {a_0} 2 2 \pi \delta_{n 0} + \sum_{m \mathop = 1}^\infty \paren {\int_\alpha^{\alpha + 2 \pi} \paren {a_m \cos m x + b_m \sin m x} \cos n x \rd x}
      | c = $\ds \int_\alpha^{\alpha + 2 \pi} \cos n x \rd x = \begin {cases} 0 & : n \ne 0 \\ 2 \pi & : n = 0 \end {cases}$
}}
{{eqn | r = a_0 \pi \delta_{n 0} + \sum_{m \mathop = 1}^\infty \paren {\int_\alpha^{\alpha + 2 \pi} a_m \cos m x \cos n x \rd x}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \sum_{m \mathop = 1}^\infty \paren {\int_\alpha^{\alpha + 2 \pi} b_m \sin m x \cos n x \rd x}
      | c = 
}}
{{eqn | r = a_0 \pi \delta_{n 0} + \sum_{m \mathop = 1}^\infty \paren {\int_\alpha^{\alpha + 2 \pi} a_m \cos m x \cos n x \rd x}
      | c = $\ds \int_\alpha^{\alpha + 2 \pi} \sin m x \cos n x \rd x = 0$
}}
{{eqn | r = a_0 \pi \delta_{n 0} + \sum_{m \mathop = 1}^\infty a_m \pi \delta_{m n}
      | c = $\ds \int_\alpha^{\alpha + 2 \pi} \cos m x \cos n x \rd x = \begin {cases} 0 & : m \ne n \\ \pi & : m = n \end {cases}$
}}
{{end-eqn}}
Thus when $n = 0$ we have:
:$\ds \int_\alpha^{\alpha + 2 \pi} \map f x \rd x = \int_\alpha^{\alpha + 2 \pi} \map f x \cos 0 x \rd x = a_0 \pi$
and when $n \ne 0$ we have:
:$\ds \int_\alpha^{\alpha + 2 \pi} \map f x \cos n x \rd x = a_n \pi$
Hence the result.
{{qed}}
Theorem: Coefficients of Sine Terms in Convergent Trigonometric Series

Let $\map S x$ be a trigonometric series which converges to $\map f x$ on the interval $\openint \alpha {\alpha + 2 \pi}$:
:$\map f x = \dfrac {a_0} 2 + \ds \sum_{m \mathop = 1}^\infty \left({a_m \cos m x + b_m \sin m x}\right)$
Then:
:$\forall n \in \Z_{\ge 0}: b_n = \dfrac 1 \pi \ds \int_\alpha^{\alpha + 2 \pi} \map f x \sin n x \rd x$

Proof:
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \dfrac {a_0} 2 + \sum_{m \mathop = 1}^\infty \paren {a_m \cos m x + b_m \sin m x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int_\alpha^{\alpha + 2 \pi} \map f x \sin n x \rd x
      | r = \int_\alpha^{\alpha + 2 \pi} \paren {\dfrac {a_0} 2 + \sum_{m \mathop = 1}^\infty \paren {a_m \cos m x + b_m \sin m x} } \sin n x \rd x
      | c = 
}}
{{eqn | r = \int_\alpha^{\alpha + 2 \pi} \dfrac {a_0} 2 \sin n x \rd x + \sum_{m \mathop = 1}^\infty \paren {\int_\alpha^{\alpha + 2 \pi} \paren {a_m \cos m x + b_m \sin m x} \sin n x \rd x}
      | c = 
}}
{{eqn | r = 0 + \sum_{m \mathop = 1}^\infty \paren {\int_\alpha^{\alpha + 2 \pi} \paren {a_m \cos m x + b_m \sin m x} \sin n x \rd x}
      | c = $\ds \int_\alpha^{\alpha + 2 \pi} \sin n x \rd x = 0$
}}
{{eqn | r = \sum_{m \mathop = 1}^\infty \paren {\int_\alpha^{\alpha + 2 \pi} a_m \cos m x \sin n x \rd x} + \sum_{m \mathop = 1}^\infty \paren {\int_\alpha^{\alpha + 2 \pi} b_m \sin m x \sin n x \rd x}
      | c = 
}}
{{eqn | r = \sum_{m \mathop = 1}^\infty \paren {\int_\alpha^{\alpha + 2 \pi} b_m \sin m x \sin n x \rd x}
      | c = $\ds \int_\alpha^{\alpha + 2 \pi} \sin m x \cos n x \rd x = 0$
}}
{{eqn | r = \sum_{m \mathop = 1}^\infty b_m \pi \delta_{m n}
      | c = $\ds \int_\alpha^{\alpha + 2 \pi} \sin m x \sin n x \rd x = \begin{cases} 0 & : m \ne n \\ \pi & : m = n \end{cases}$
}}
{{eqn | r = b_n \pi 
      | c = {{Defof|Kronecker Delta}}
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Angle plus Full Angle/Corollary

Let $n \in \Z$ be an integer.
Then:
:$\map \sin {x + 2 n \pi} = \sin x$

Proof:
From Sine of Angle plus Full Angle:
:$\map \sin {x + 2 \pi} = \sin x$
The result follows from the General Periodicity Property:
If:
:$\forall x \in X: \map f x = \map f {x + L}$
then:
:$\forall n \in \Z: \forall x \in X: \map f x = \map f {x + n L}$
{{qed}}
Theorem: Fourier's Theorem

Let $\alpha \in \R$ be a real number.
Let $\map f x$ be a real function which is defined and bounded on the interval $\openint \alpha {\alpha + 2 \pi}$.
Let $f$ satisfy the Dirichlet conditions on $\openint \alpha {\alpha + 2 \pi}$:
{{:Definition:Dirichlet Conditions}}
Outside the interval $\openint \alpha {\alpha + 2 \pi}$, let $f$ be periodic and defined such that:
:$\map f x = \map f {x + 2 \pi}$
Let $f$ be defined by the Fourier series:
:$(1): \quad \ds \frac {a_0} 2 + \sum_{n \mathop = 1}^\infty \paren {a_n \cos n x + b_n \sin n x}$
such that:
:$\ds a_n = \dfrac 1 \pi \int_\alpha^{\alpha + 2 \pi} \map f x \cos n x \rd x$
:$\ds b_n = \dfrac 1 \pi \int_\alpha^{\alpha + 2 \pi} \map f x \sin n x \rd x$
Then for all $a \in \R$, $(1)$ converges to the sum:
:$\ds \frac 1 2 \paren {\lim_{x \mathop \to a^+} \map f x + \lim_{x \mathop \to a^-} \map f x}$
where the $\lim$ symbols denote the limit from the right and the limit from the left.

Proof:
=== Lemma 1 ===
{{:Fourier's Theorem/Lemma 1}}{{qed|lemma}}
Theorem: Definite Integral of Step Function

Let $\alpha, \beta \in \R$ be a real numbers such that $\alpha < \beta$.
Let $\map f x$ be a step function defined on the interval $\closedint \alpha \beta$:
:$\map f x = \lambda_1 \chi_{\mathbb I_1} + \lambda_2 \chi_{\mathbb I_2} + \cdots + \lambda_n \chi_{\mathbb I_n}$
where:
:$\lambda_1, \lambda_2, \ldots, \lambda_n$ are real constants
:$\mathbb I_1, \mathbb I_2, \ldots, \mathbb I_n$ are intervals, where these intervals partition $\closedint \alpha \beta$
:$\chi_{\mathbb I_1}, \chi_{\mathbb I_2}, \ldots, \chi_{\mathbb I_n}$ are characteristic functions of $\mathbb I_1, \mathbb I_2, \ldots, \mathbb I_n$.
Then the definite integral of $f$ {{WRT|Integration}} $x$ over $\closedint \alpha \beta$ is given by:
:$\ds \int_\alpha^\beta \map f x \rd x = \sum_{k \mathop = 1}^n \lambda_k \paren {\beta_k - \alpha_k}$
where $\alpha_k, \beta_k$ are the endpoints of $\mathbb I_k$ for $1 \le k \le n$.

Proof:
Each of the intervals $\mathbb I_k$ is such that $f \sqbrk {\mathbb I_k}$ is a constant function:
:$\forall x \in \mathbb I_k: \map f x = \lambda_k$
Thus:
{{begin-eqn}}
{{eqn | l = \int_{\mathbb I_k} \map f x \rd x
      | r = \int_{\alpha_k}^{\beta_k} \lambda_k \rd x
      | c = 
}}
{{eqn | r = \lambda_k \paren {\beta_k - \alpha_k}
      | c = Definite Integral of Constant
}}
{{end-eqn}}
From {{Corollary|Sum of Integrals on Adjacent Intervals for Integrable Functions}}:
{{begin-eqn}}
{{eqn | l = \int_\alpha^\beta \map f x \rd x
      | r = \sum_{k \mathop = 1}^n \int_{\mathbb I_k} \map f x \rd x
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^n \lambda_k \paren {\beta_k - \alpha_k}
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Step Functions
Category:Definite Integrals
3tt9r2dbj0qrfoxij8tpdxkn44jxvs3
Theorem: Step Function satisfies Dirichlet Conditions

Let $\alpha, \beta \in \R$ be a real numbers such that $\alpha < \beta$.
Let $\map f x$ be a step function defined on the interval $\openint \alpha \beta$.
Then $f$ satisfies the Dirichlet conditions.

Proof:
Recall the definition of step function:
:{{Definition:Step Function}}
Recall the Dirichlet conditions:
{{:Definition:Dirichlet Conditions}}
We inspect the Dirichlet conditions in turn.
Theorem: Parseval's Theorem/Formulation 2

Let $f$ be a real function which is square-integrable over the interval $\openint {-\pi} \pi$.
Let $f$ be expressed by the Fourier series:
:$\map f x = \ds \sum_{n \mathop = -\infty}^\infty c_n e^{i n x}$
where:
:$c_n = \ds \frac 1 {2 \pi} \int_{-\pi}^\pi \map f t e^{-i n t} \rd t$
Then:
:$\ds \frac 1 {2 \pi} \int_{-\pi}^\pi \size {\map f x}^2 \rd x = \sum_{n \mathop = -\infty}^\infty \size {c_n}^2$

Proof:
{{begin-eqn}}
{{eqn | l = \frac 1 {2 \pi} \int_{-\pi}^\pi \size {\map f x}^2 \rd x
      | r = \frac 1 {2 \pi} \int_{-\pi}^\pi \map f x \overline {\map f x} \rd x
      | c = Modulus in Terms of Conjugate
}}
{{eqn | r = \frac 1 {2 \pi} \int_{-\pi}^\pi \sum_{n \mathop = -\infty}^\infty c_n e^{i n x} \overline {\sum_{m \mathop = -\infty}^\infty c_m e^{i m x} } \rd x
}}
{{eqn | r = \frac 1 {2 \pi} \int_{-\pi}^\pi \sum_{n \mathop = -\infty}^\infty c_n e^{i n x} \sum_{m \mathop = -\infty}^\infty \overline {c_m} e^{-i m x} \rd x
      | c = Sum of Complex Conjugates
}}
{{eqn | r = \frac 1 {2 \pi} \int_{-\pi}^\pi \sum_{n \mathop = -\infty}^\infty \sum_{m \mathop = -\infty}^\infty c_n \overline {c_m} e^{i x \paren {n - m} } \rd x
}}
{{eqn | r = \frac 1 {2 \pi} \sum_{n \mathop = -\infty}^\infty \sum_{m \mathop = -\infty}^\infty c_n \overline {c_m} \int_{-\pi}^\pi e^{i x \paren {n - m} } \rd x
      | c = Fubini's Theorem
}}
{{eqn | r = \frac 1 {2 \pi} \sum_{n \mathop = -\infty}^\infty \sum_{m \mathop = -\infty}^\infty c_n \overline {c_m} 2 \pi \delta_{n m}
      | c = Integral over 2 pi of Exponential of i by n x
}}
{{eqn | r = \frac {2 \pi} {2 \pi} \sum_{n \mathop = -\infty}^\infty c_n \overline {c_n}
}}
{{eqn | r = \sum_{n \mathop = -\infty}^\infty \size {c_n}^2 
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Marc-Antoine Parseval}}
Category:Parseval's Theorem
01t1h36vn98xo4mf38np7uz51o9yr7x
Theorem: Parseval's Theorem/Formulation 1

Let $f$ be a real function which is square-integrable over the interval $\openint {-\pi} \pi$.
Let $f$ be expressed by the Fourier series: 
:$\map f x \sim \dfrac {a_0} 2 + \ds \sum_{n \mathop = 1}^\infty \paren {a_n \cos n x + b_n \sin n x}$
{{explain|What does $\sim$ mean?}}
Then:
:$\ds \frac 1 \pi \int_{-\pi}^\pi \size {\map {f^2} x} \rd x = \frac { {a_0}^2} 2 + \sum_{n \mathop = 1}^\infty \paren { {a_n}^2 + {b_n}^2}$
{{explain|Is this not $\size {\map f x}^2$? I know these are the same but the latter is more common.}}

Proof:
{{ProofWanted}}
{{Namedfor|Marc-Antoine Parseval}}
Category:Parseval's Theorem
9h5wuhgjgv3kv4f7zvpg9echh2xe9sf
Theorem: Dilogarithm of Square

:$\map {\Li_2} z + \map {\Li_2} {-z} = \dfrac 1 2 \map {\Li_2} {z^2}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\Li_2} z + \map {\Li_2} {-z}
      | r = -\paren {\int_0^z \frac {\map \ln {1 - t} } t \rd t + \int_0^z \frac {\map \ln {1 + t} } t \rd t}
      | c = {{Defof|Dilogarithm Function}}
}}
{{eqn | r = -\int_0^z \frac {\map \ln {\paren {1 - t} \paren {1 + t} } } t \rd t
      | c = Linear Combination of Definite Integrals, Sum of Logarithms
}}
{{eqn | r = -\int_0^z \frac {\map \ln {1 - t^2} } t \rd t
      | c = Difference of Two Squares
}}
{{eqn | r = -\int_0^{z^2} \frac {\map \ln {1 - t^2} } t \frac {\map \d {t^2} } {2 t}
      | c = substituting $t \to t^2$
}}
{{eqn | r = -\frac 1 2 \int_0^{z^2} \frac {\map \ln {1 - t^2} } {t^2} \map \rd {t^2}
}}
{{eqn | r = \frac 1 2 \map {\Li_2} {z^2}
      | c = {{Defof|Dilogarithm Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Dilogarithm of Square

:$\map {\Li_2} z + \map {\Li_2} {-z} = \dfrac 1 2 \map {\Li_2} {z^2}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\Li_2} z + \map {\Li_2} {-z}
      | r = \sum_{n \mathop = 1}^\infty \frac {z^n} {n^2} + \sum_{n \mathop = 1}^\infty \frac {\paren {-z}^n} {n^2}
      | c = Power Series Expansion for Spence's Function
}}
{{eqn | r = \paren {z + \frac {z^2} {2^2} + \frac {z^3} {3^2} + \frac {z^4} {4^2} + \frac {z^5} {5^2} + \frac {z^6} {6^2} + \cdots} + \paren {-z + \frac {z^2} {2^2} - \frac {z^3} {3^2} + \frac {z^4} {4^2} - \frac {z^5} {5^2} + \frac {z^6} {6^2} + \cdots}
      | c = 
}}
{{eqn | r = 2 \paren {\frac {z^2} {2^2} + \frac {z^4} {4^2} + \frac {z^6} {6^2} + \cdots}
      | c = odd terms cancel, even terms double
}}
{{eqn | r = \frac 2 {2^2} \paren {\frac {z^2} {1^2} + \frac {z^4} {2^2} + \frac {z^6} {3^2} + \cdots}
      | c = factoring out $2^2$
}}
{{eqn | r = \frac 1 2 \sum_{n \mathop = 1}^\infty \frac {\paren {z^2}^n} {n^2}
      | c = 
}}
{{eqn | r = \frac 1 2 \map {\Li_2} {z^2}
      | c = {{Defof|Dilogarithm Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Power Series Expansion for Spence's Function

Spence's function has a power series expansion: 
:$\ds \map {\Li_2} z = \sum_{n \mathop = 1}^\infty \frac {z^n} {n^2}$
for $z \in \C$.
This converges for $\size z \le 1$.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\Li_2} z
      | r = -\int_0^z \frac {\map \ln {1 - t} } t \rd t
      | c = {{Defof|Spence's Function}}
}}
{{eqn | r = -\int_0^z \frac 1 t \sum_{n \mathop = 1}^\infty \paren {-\frac {t^n} n} \rd t 
      | c = Power Series Expansion for $\map \ln {1 - x}$
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \int_0^z \frac {t^{n - 1} } n \rd t
      | c = Fubini's Theorem
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \frac {z^n} {n^2}
      | c = Primitive of Power
}}
{{end-eqn}}
{{qed}}
Category:Spence's Function
Category:Examples of Power Series
13ka3sww5blalnhrsefbmbaw91iz3hp
Theorem: Odd Function of Zero is Zero

Let $f: \R \to \R$ be an odd function.
Let $f$ be defined at the point $x = 0$.
Then:
:$\map f 0 = 0$

Proof:
By definition of odd function:
:$\map f {-x} = -\map f x$
and so:
{{begin-eqn}}
{{eqn | l = \map f {-0}
      | r = \map f 0
      | c = 
}}
{{eqn | r = -\map f 0
      | c = 
}}
{{end-eqn}}
The only real number $a$ for which $a = -a$ is $0$.
Hence the result.
{{qed}}