avewright/proofwiki-math huggingface dataset:
Theorem: Subspace of Product Space is Homeomorphic to Factor Space/Proof 2/Continuous Mapping

Let $\family {\struct {X_i, \tau_i} }_{i \mathop \in I}$ be a family of topological spaces where $I$ is an arbitrary index set.
Let $\ds \struct {X, \tau} = \prod_{i \mathop \in I} \struct {X_i, \tau_i}$ be the product space of $\family {\struct {X_i, \tau_i} }_{i \mathop \in I}$.
Let $z \in X$.
Let $i \in I$. 
Let $Y_i = \set {x \in X: \forall j \in I \setminus \set i: x_j = z_j}$.
Let $\upsilon_i$ be the subspace topology of $Y_i$ relative to $\tau$. 
Let $p_i = \pr_i {\restriction_{Y_i}}$, where $\pr_i$ is the projection from $X$ to $X_i$.
Then:
:$p_i$ is continuous.

Proof:
Let $V \in \tau_i$.
Let $\ds U = \prod_{i \mathop \in I} U_i$ where:
:$U_j = \begin{cases} X_j & j \ne i \\ V & j = i \end{cases}$
From Natural Basis of Product Topology, $U$ is an element of the the natural basis.
By definition of the product topology $\tau$ on the product space $\struct {X, \tau}$ the natural basis is a basis for the product topology.
It follows that:
:$U$ is open in $\struct {X, \tau}$
Let $x \in Y_i$.
Now:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \map {p_i^\gets} V
}}
{{eqn | ll= \leadstoandfrom
      | l = \map {p_i} x
      | o = \in
      | r = V
      | c = {{Defof|Inverse Image Mapping of Mapping}}: $p_i^\gets$
}}
{{eqn | ll= \leadstoandfrom
      | l = \map {\pr_i} x
      | o = \in
      | r = V
      | c = {{Defof|Restriction of Mapping}} $p_i$
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = U
      | c = Definition of $U$
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = U \cap Y_i
      | c = as $x \in Y_i$
}}
{{end-eqn}}
By set equality:
:$\map {p_i^\gets} V = U \cap Y_i$
By definition of the subspace topology on $Y_i$:
:$\map {p_i^\gets} V \in \upsilon_i$
It follows that $p_i$ is continuous by definition.
Theorem: Subspace of Product Space is Homeomorphic to Factor Space/Proof 2/Open Mapping

Let $\family {\struct {X_i, \tau_i} }_{i \mathop \in I}$ be a family of topological spaces where $I$ is an arbitrary index set.
Let $\ds \struct {X, \tau} = \prod_{i \mathop \in I} \struct {X_i, \tau_i}$ be the product space of $\family {\struct {X_i, \tau_i} }_{i \mathop \in I}$.
Let $z \in X$.
Let $i \in I$. 
Let $Y_i = \set {x \in X: \forall j \in I \setminus \set i: x_j = z_j}$.
Let $\upsilon_i$ be the subspace topology of $Y_i$ relative to $\tau$. 
Let $p_i = \pr_i {\restriction_{Y_i} }$, where $\pr_i$ is the projection from $X$ to $X_i$.
Then:
:$p_i$ is an open mapping.

Proof:
Let $U \in \upsilon_i$.
Let $x \in \map {p_i^\to} U$.
Then by definition of the direct image mapping:
:$\exists y \in U : x = \map {p_i} y$
By the definition of the subspace topology:
:$\exists U' \in \tau: U = U' \cap Y_i$
For all $k \in I$ let $\pr_k$ denote the projection from $X$ to $X_k$.
By definition of the natural basis of the product topology $\tau$:
:there exists a finite subset $J$ of $I$
and:
:for each $k \in J$, there exists a $V_k \in \tau_k$
such that:
:$\ds y \in \bigcap_{k \mathop \in J} \map {\pr_k^\gets} {V_k} \subseteq U'$
Then:
:$\ds y \in \paren {\bigcap_{k \mathop \in J} \map{\pr_k^\gets} {V_k} } \cap Y_i \subseteq U' \cap Y_i = U$
By definition of direct image mapping:
:$\ds x = \map {p_i} y \in \map {p_i^\to} {\paren {\bigcap_{k \mathop \in J} \map {\pr_k^\gets} {V_k} } \cap Y_i} \subseteq \map {p_i^\to} U$
Recall that $p_i$ is an injection.
Then:
{{begin-eqn}}
{{eqn | l = \map {p_i^\to} {\paren {\bigcap_{k \mathop \in J} \map {\pr_k^\gets} {V_k} } \cap Y_i}
      | r = \map {p_i^\to} {\bigcap_{k \mathop \in J} \paren {\map {\pr_k^\gets} {V_k} \cap Y_i} }
      | c = Set Intersection is Self-Distributive
}}
{{eqn | r = \bigcap_{k \mathop \in J} \map {p_i^\to} {\map {\pr_k^\gets } {V_k} \cap Y_i}
      | c = Image of Intersection under Injection
}}
{{end-eqn}}
Let $k \in J$.
==== Lemma ====
{{:Subspace of Product Space is Homeomorphic to Factor Space/Proof 2/Lemma 1}}{{qed|lemma}}
By {{Open-set-axiom|1}}:
:$\ds \bigcap_{k \mathop \in J} \map {p_i^\to} {\map{\pr_k^\gets} {V_k} \cap Y_i}$ is open in $\struct {X_i, \tau_i}$
Since $x \in \map {p_i^\to} U$ was arbitrary then it has been shown that:
:$\forall x \in \map {p_i^\to} U : \exists V \in \tau_i : x \in V \subseteq \map {p_i^\to} U$
Then by definition:
$\forall x \in \map {p_i^\to} U: \map {p_i^\to} U$ is a neighborhood of $x$.
From Set is Open iff Neighborhood of all its Points:
:$\map {p_i^\to} U$ is open in $\tau_i$.
Since $U \in \upsilon_i$ was arbitrary, $p_i$ is an open mapping.
Theorem: Exponential Distribution in terms of Continuous Uniform Distribution

Let $X \sim \mathrm U \hointl 0 1$ where $\mathrm U \hointl 0 1$ is the continuous uniform distribution on $\hointl 0 1$.
Let $\beta$ be a positive real number.
Then: 
:$-\beta \ln X \sim \Exponential \lambda$
where $\Exponential \cdot$ is the exponential distribution.

Proof:
Let $Y \sim \Exponential \lambda$.
We aim to show that:
:$\map \Pr {Y < -\beta \ln x} = \map \Pr {X > x}$
for all $x \in \hointl 0 1$.
We have:
{{begin-eqn}}
{{eqn	| l = \map \Pr {Y < -\beta \ln x}
	| r = \frac 1 \beta \int_0^{-\beta \ln x} \map \exp {-\frac u \beta} \rd u
	| c = {{Defof|Exponential Distribution}}
}}
{{eqn	| r = \intlimits {-\map \exp {-\frac u \beta} } 0 {-\beta \ln x}
	| c = Primitive of $\exp a x$
}}
{{eqn	| r = -\map \exp {-\frac {-\beta \ln x} {\beta} } + \map \exp 0
}}
{{eqn	| r = 1 - x
	| c = {{Defof|Natural Logarithm}}, Exponential of Zero
}}
{{eqn	| r = \frac 1 {1 - 0} \int_x^1 \rd u
	| c = Primitive of Constant
}}
{{eqn	| r = \map \Pr {X > x}
	| c = {{Defof|Continuous Uniform Distribution}}
}}
{{end-eqn}}
{{qed}}
Category:Exponential Distribution
Category:Continuous Uniform Distribution
kmc471ssl8f0t85nfiq8zj8j3y4eakz
Theorem: Power of Random Variable with Continuous Uniform Distribution has Beta Distribution

Let $X \sim \ContinuousUniform 0 1$ where $\ContinuousUniform 0 1$ is the continuous uniform distribution on $\closedint 0 1$.
Let $n$ be a positive real number. 
Then:
:$X^n \sim \BetaDist {\dfrac 1 n} 1$
where $\operatorname {Beta}$ is the beta distribution.

Proof:
Let:
:$Y \sim \BetaDist {\dfrac 1 n} 1$
We aim to show that: 
:$\map \Pr {Y < x^n} = \map \Pr {X < x}$
for all $x \in \closedint 0 1$. 
We have:
{{begin-eqn}}
{{eqn	| l = \map \Pr {Y < x^n}
	| r = \int_0^{x^n} \frac 1 {\map \Beta {\frac 1 n, 1} } u^{\frac 1 n - 1} \paren {1 - u}^{1 - 1} \rd u
	| c = {{Defof|Beta Distribution}}
}}
{{eqn	| r = \frac {\map \Gamma {\frac 1 n + 1} } {\map \Gamma {\frac 1 n} \map \Gamma 1} \intlimits {n u^{\frac 1 n} } 0 {x^n}
	| c = {{Defof|Gamma Function}}, Primitive of Power
}}
{{eqn	| r = \frac n n x
	| c = Gamma Difference Equation
}}
{{eqn	| r = x
}}
{{eqn	| r = \frac 1 {1 - 0} \int_0^x \rd u
	| c = Primitive of Constant
}}
{{eqn	| r = \map \Pr {X < x}
	| c = {{Defof|Continuous Uniform Distribution}}
}}
{{end-eqn}}
{{qed}}
Category:Continuous Uniform Distribution
Category:Beta Distribution
qohnmnficfpp575bvekyr81helo7pqy
Theorem: Expectation of Non-Negative Random Variable is Non-Negative

Let $X$ be a random variable. 
Let $\map \Pr {X \ge 0} = 1$. 
Then:
:$\expect X \ge 0$
where $\expect X$ denotes the expectation of $X$.

Proof:
=== Discrete Random Variable ===
{{:Expectation of Non-Negative Random Variable is Non-Negative/Discrete}}
Theorem: Expectation of Non-Negative Random Variable is Non-Negative/Discrete

Let $X$ be a discrete random variable. 
Let $\map \Pr {X \ge 0} = 1$. 
Then:
:$\expect X \ge 0$
where $\expect X$ denotes the expectation of $X$.

Proof:
Let $\map \supp X$ be the support of $X$. 
Note that since $X$ is discrete, its sample space and hence support is countable. 
Therefore, there exists some sequence $\sequence {x_i}_{i \mathop \in I}$ such that: 
:$\map \supp X = \set {x_i \mid i \in I}$
for some $I \subseteq \N$. 
By the definition of a sample space, we have: 
:$\map \Pr {X = x_i} \ge 0$
for all $i \in I$. 
Note that since $\map \Pr {X \ge 0} = 1$, we have $\map \Pr {X < 0} = 0$. 
So, for any $x < 0$ we necessarily have $\map \Pr {X = x} = 0$, meaning that $x \notin \map \supp X$. 
We therefore have that any elements of $\map \supp X$ are non-negative.
That is: 
:$x_i \ge 0$
for all $i \in I$.
Therefore: 
:$x_i \map \Pr {X = x_i} \ge 0$
for all $i \in I$. 
Summing over all $i \in I$, we have: 
:$\ds \sum_{i \mathop \in I} x_i \map \Pr {X = x_i} \ge 0$
Hence, by the definition of expectation:
:$\expect X \ge 0$
{{qed}}
Theorem: Expectation of Almost Surely Constant Random Variable

Let $X$ be an almost surely constant random variable.
That is, there exists some $c \in \R$ such that: 
:$\map \Pr {X = c} = 1$
Then: 
:$\expect X = c$

Proof:
Note that since $\map \Pr {X = c} = 1$, we have $\map \Pr {X \ne c} = 0$ from Probability of Event not Occurring.
Therefore: 
:$\map {\mathrm {supp} } X = \set c$
{{MissingLinks|supp}}
We therefore have:
{{begin-eqn}}
{{eqn	| l = \expect X
	| r = \sum_{x \mathop \in \map {\mathrm {supp} } X} x \map \Pr {X = x}
	| c = {{Defof|Expectation of Discrete Random Variable}}
}}
{{eqn	| r = c \map \Pr {X = c}
}}
{{eqn	| r = c
}}
{{end-eqn}}
{{qed}}
Category:Expectation
cqhoc6pyg2z5hpd3qb4dksyh7h9s6dq
Theorem: Expectation Preserves Inequality

Let $X$, $Y$ be random variables.
Let $\map \Pr {X \ge Y} = 1$.
Then: 
:$\expect X \ge \expect Y$

Proof:
Note that we have: 
:$\map \Pr {X - Y \ge 0} = 1$
From Expectation of Non-Negative Random Variable is Non-Negative, we then have: 
:$\expect {X - Y} \ge 0$
From Sum of Expectations of Independent Trials, we have: 
:$\expect X + \expect {-Y} \ge 0$
From Expectation of Linear Transformation of Random Variable, we have:
:$\expect X - \expect Y \ge 0$
That is: 
:$\expect X \ge \expect Y$
{{qed}}
Category:Expectation
1lj57fi74c5hffhuwnorm00zc1dydog
Theorem: Random Variable has Zero Variance iff Almost Surely Constant

Let $X$ be a random variable such that $\expect {X^2}$ exists.
Then $\var X = 0$ {{iff}} there exists $c \in \R$ with $\map \Pr {X = c} = 1$.
That is, $X$ is almost surely constant.

Proof:
=== Sufficient Condition ===
Suppose that there exists some $c \in \R$ with $\map \Pr {X = c} = 1$.
From Expectation of Almost Surely Constant Random Variable: 
:$\expect X = c$
Let $\map \supp X$ be the support of $X$. 
Since $\map \Pr {X = c} = 1$, we have: 
:$\map \supp X = \set c$
We therefore have: 
{{begin-eqn}}
{{eqn	| l = \expect {X^2}
	| r = \sum_{x \mathop \in \map \supp X} x^2 \map \Pr {X = x}
}}
{{eqn	| r = c^2 \map \Pr {X = c}
}}
{{eqn	| r = c^2
}}
{{end-eqn}}
Hence, from Variance as Expectation of Square minus Square of Expectation:
{{begin-eqn}}
{{eqn	| l = \var X
	| r = \expect {X^2} - \paren {\expect X}^2
}}
{{eqn	| r = c^2 - c^2
}}
{{eqn	| r = 0
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Covariance of Random Variable with Itself

Let $X$ be a random variable.
Then $\cov {X, X} = \var X$.

Proof:
We have: 
{{begin-eqn}}
{{eqn	| l = \cov {X, X}
	| r = \expect {\paren {X - \expect X} \paren {X - \expect X} }
	| c = {{Defof|Covariance}}
}}
{{eqn	| r = \expect {\paren {X - \expect X}^2}
}}
{{eqn	| r = \var X
	| c = {{Defof|Variance}}
}}
{{end-eqn}}
{{qed}}
Category:Covariance
Category:Variance
ir6l7arixypl4c30xq378s6a8rrkt9e
Theorem: Covariance is Symmetric

Let $X$ and $Y$ be random variables.
Suppose the covariance $\cov {X, Y}$ exists.
Then $\cov {X, Y} = \cov {Y, X}$.

Proof:
{{begin-eqn}}
{{eqn	| l = \cov {X, Y}
	| r = \expect {\paren {X - \expect X} \paren {Y - \expect Y} }
	| c = {{Defof|Covariance}}
}}
{{eqn	| r = \expect {\paren {Y - \expect Y} \paren {X - \expect X} }
	| c = Real Multiplication is Commutative
}}
{{eqn	| r = \cov {Y, X}
	| c = {{Defof|Covariance}}
}}
{{end-eqn}}
{{qed}}
Category:Covariance
2yrsm5swavo21axqe6u9pf1gphquuob
Theorem: Covariance of Linear Combination of Random Variables with Another

Let $X, Y, Z$ be random variables. 
Let $a, b$ be real numbers.
Then: 
:$\cov {a X + b Y, Z} = a \cov {X, Z} + b \cov {Y, Z}$

Proof:
{{begin-eqn}}
{{eqn | l = \cov {a X + b Y, Z}
      | r = \expect {\paren {a X + b Y} Z} - \expect {a X + b Y} \expect Z
      | c = Covariance as Expectation of Product minus Product of Expectations
}}
{{eqn | r = a \expect {X Z} + b \expect {Y Z} - \paren {a \expect X + b \expect Y} \expect Z
      | c = Expectation is Linear
}}
{{eqn | r = a \paren {\expect {X Z} - \expect X \expect Z} + b \paren {\expect {Y Z} - \expect Y \expect Z}
}}
{{eqn | r = a \cov {X, Z} + b \cov {Y, Z}
      | c = Covariance as Expectation of Product minus Product of Expectations
}}
{{end-eqn}}
{{qed}}
Category:Covariance
tkdg7jezusm8awbxleae2zskkphwyr4
Theorem: Covariance of Sums of Random Variables

Let $n$ be a strictly positive integer.
Let $\sequence {X_i}_{1 \mathop \le i \mathop \le n}$, $\sequence {Y_j}_{1 \mathop \le j \mathop \le n}$ be sequences of random variables.
Then: 
:$\ds \cov {\sum_{i \mathop = 1}^n X_i, \sum_{j \mathop = 1}^n Y_j} = \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^n \cov {X_i, Y_j}$

Proof:
{{begin-eqn}}
{{eqn	| l = \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^n \cov {X_i, Y_j}
	| r = \sum_{i \mathop = 1}^n \paren {\sum_{j \mathop = 1}^n \cov {Y_j, X_i} }
	| c = Covariance is Symmetric
}}
{{eqn	| r = \sum_{i \mathop = 1}^n \cov {\sum_{j \mathop = 1}^n Y_j, X_i}
	| c = Covariance of Sums of Random Variables: Lemma
}}
{{eqn	| r = \sum_{i \mathop = 1}^n \cov {X_i, \sum_{j \mathop = 1}^n Y_j}
	| c = Covariance is Symmetric
}}
{{eqn	| r = \cov {\sum_{i \mathop = 1}^n X_i, \sum_{j \mathop = 1}^n Y_j}
	| c = Covariance of Sums of Random Variables: Lemma
}}
{{end-eqn}}
{{qed}}
Category:Covariance
Category:Covariance of Sums of Random Variables
er2m9ghp676g42c5ckucyyaaj0prx2o
Theorem: Covariance of Sums of Random Variables/Lemma

Let $n$ be a strictly positive integer.
Let $\sequence {X_i}_{1 \mathop \le i \mathop \le n}$ be a sequence of random variables.
Let $Y$ be a random variable.
Then: 
:$\ds \cov {\sum_{i \mathop = 1}^n X_i, Y} = \sum_{i \mathop = 1}^n \cov {X_i, Y}$

Proof:
Proof by induction:
For all $n \in \N$, let $\map P n$ be the proposition: 
:$\ds \cov {\sum_{i \mathop = 1}^n X_i, Y} = \sum_{i \mathop = 1}^n \cov {X_i, Y}$
Theorem: Expectation of Linear Transformation of Random Variable

Let $X$ be a random variable. 
Let $a, b$ be real numbers. 
Let $\expect X$ denote the expectation of $X$. 
Then we have: 
:$\expect {a X + b} = a \expect X + b$
if that expectation exists.

Proof:
=== Discrete Random Variable ===
{{:Expectation of Linear Transformation of Random Variable/Discrete}}
Theorem: Expectation of Linear Transformation of Random Variable/Discrete

Let $X$ be a discrete random variable. 
Let $a, b$ be real numbers. 
Then we have: 
:$\expect {a X + b} = a \expect X + b$
where $\expect X$ denotes the expectation of $X$.

Proof:
We have: 
{{begin-eqn}}
{{eqn	| l = \expect {a X + b}
	| r = \sum_{x \mathop \in \Img X} \paren {a x + b} \map \Pr {X = x}
	| c = Expectation of Function of Discrete Random Variable
}}
{{eqn	| r = a \sum_{x \mathop \in \Img X} x \map \Pr {X = x} + b \sum_{x \mathop \in \Img X} \map \Pr {X = x}
}}
{{eqn	| r = a \expect X + b \times 1
	| c = {{Defof|Expectation of Discrete Random Variable}}, {{Defof|Probability Mass Function}}
}}
{{eqn	| r = a \expect X + b
}}
{{end-eqn}}
{{qed}}
Theorem: Expectation of Linear Transformation of Random Variable/Continuous

Let $X$ be a continuous random variable. 
Let $a, b$ be real numbers. 
Then we have: 
:$\expect {a X + b} = a \expect X + b$
where $\expect X$ denotes the expectation of $X$.

Proof:
Let $\map \supp X$ be the support of $X$. 
Let $f_X : \map \supp X \to \R$ be the probability density function of $X$.
{{questionable|What if the density $f_X$ does not exist?}}
Then:
{{begin-eqn}}
{{eqn	| l = \expect {a X + b}
	| r = \int_{x \mathop \in \map \supp X} \paren {a x + b} \map {f_X} x \rd x
	| c = Expectation of Function of Continuous Random Variable
}}
{{eqn	| r = a \int_{x \mathop \in \map \supp X} x \map {f_X} x \rd x + b \int_{x \mathop \in \map \supp X} \map {f_X} x \rd x
	| c = Linear Combination of Definite Integrals
}}
{{eqn	| r = a \expect X + b \times 1
	| c = {{Defof|Expectation of Continuous Random Variable}}
}}
{{eqn	| r = a \expect X + b
}}
{{end-eqn}}
{{qed}}
Theorem: Variance of Linear Transformation of Random Variable

Let $X$ be a random variable. 
Let $a, b$ be real numbers. 
Then we have: 
:$\var {a X + b} = a^2 \var X$
where $\var X$ denotes the variance of $X$.

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = \var {a X + b}
	| r = \expect {\paren {a X + b - \expect {a X + b} }^2}
	| c = {{Defof|Variance}}
}}
{{eqn	| r = \expect {\paren {a X + b - a \expect X - b}^2}
	| c = Expectation of Linear Transformation of Random Variable
}}
{{eqn	| r = \expect {a^2 \paren {X - \expect X}^2}
}}
{{eqn	| r = a^2 \expect {\paren {X - \expect X}^2}
	| c = Expectation of Linear Transformation of Random Variable
}}
{{eqn	| r = a^2 \var X
	| c = {{Defof|Variance}}
}}
{{end-eqn}}
{{qed}}
Category:Variance
2wnjot8um78hb1la52xi5uluf0gf3mw
Theorem: Fourier Series/Square Wave

600pxthumbrightSquare Wave and $9$th Approximation
Let $\map S x$ be the square wave defined on the real numbers $\R$ as:
:$\forall x \in \R: \map S x = \begin {cases}
1 & : x \in \openint 0 l \\
-1 & : x \in \openint {-l} 0 \\
\map S {x + 2 l} & : x < -l \\
\map S {x - 2 l} & : x > +l \end {cases}$
Then its Fourier series can be expressed as:
{{begin-eqn}}
{{eqn | l = \map S x
      | o = \sim
      | r = \frac 4 \pi \sum_{r \mathop = 0}^\infty \frac 1 {2 r + 1} {\sin \frac {\pi x} l}
      | c = 
}}
{{eqn | r = \frac 4 \pi \paren {\sin \frac {\pi x} l + \dfrac 1 3 \sin \frac {3 \pi x} l + \dfrac 1 5 \sin \frac {5 \pi x} l + \dotsb}
      | c = 
}}
{{end-eqn}}

Proof:
Let $\map f x$ be the function defined as:
:$\forall x \in \openint {-l} l: \begin{cases} -1 & : -l < x < 0 \\ 1 & : 0 < x < l \end {cases}$
By inspection we see that $\map f x$ is an odd function.
Hence from Fourier Series for Odd Function over Symmetric Range we can express $f$ by a half-range Fourier sine series:
:$\ds \map f x \sim \sum_{n \mathop = 1}^\infty b_n \sin \dfrac {n \pi x} l$
where for all $n \in \Z_{> 0}$:
:$\ds b_n = \frac 2 l \int_0^l \map f x \sin \dfrac {n \pi x} l \rd x$
over the interval $\openint 0 l$.
In that interval $\openint 0 l$, we have:
:$\map S x = 1$
Hence:
{{begin-eqn}}
{{eqn | l = b_n
      | r = \frac 2 l \int_0^l \sin \dfrac {n \pi x} l \rd x
      | c = 
}}
{{eqn | r = \frac 2 l \intlimits {\frac l {n \pi} \paren {-\cos \dfrac {n \pi x} l} } 0 c
      | c = Primitive of $\sin a x$
}}
{{eqn | r = \frac 2 {n \pi} \paren {-\cos n \pi - \paren {-\cos 0} }
      | c = 
}}
{{eqn | r = \frac 2 {n \pi} \paren {1 - \cos n \pi}
      | c = Cosine of Zero is One and simplifying
}}
{{eqn | r = \frac 2 {n \pi} \paren {1 - \paren {-1}^n}
      | c = Cosine of Multiple of Pi
}}
{{eqn | r = \begin {cases} 0 & : \text {$n$ even} \\ \dfrac 4 {n \pi}  & : \text {$n$ odd} \end {cases}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = b_{2 r + 1}
      | r = \dfrac 4 {\paren {2 r + 1} \pi}
      | c = for $r \in \Z_{\ge 0}$: substituting $n = 2 r + 1$
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Fourier Series/Triangle Wave

600pxthumbrightTriangle Wave and $9$th Approximation
<onlyinclude>
Let $\map T x$ be the triangle wave defined on the real numbers $\R$ as:
:<nowiki>$\forall x \in \R: \map T x = \begin {cases}
\size x & : x \in \closedint {-l} l \\
\map T {x + 2 l} & : x < -l \\
\map T {x - 2 l} & : x > +l \end {cases}$</nowiki>
where:
:$l$ is a given real constant
:$\size x$ denotes the absolute value of $x$.
Then its Fourier series can be expressed as:
{{begin-eqn}}
{{eqn | l = \map T x
      | o = \sim
      | r = \frac l 2 - \frac {4 l} {\pi^2} \sum_{n \mathop = 0}^\infty \frac 1 {\paren {2 n + 1}^2} \cos \dfrac {\paren {2 n + 1} \pi x} l
      | c = 
}}
{{eqn | r = \frac l 2 - \frac {4 l} {\pi^2} \paren {\cos \dfrac {\pi x} l + \frac 1 {3^2} \cos \dfrac {3 \pi x} l + \frac 1 {5^2} \cos \dfrac {5 \pi x} l + \dotsb}
      | c = 
}}
{{end-eqn}}

Proof:
Let $\map f x: \openint {-l} l \to \R$ denote the absolute value function on the open interval $\openint {-l} l$:
:<nowiki>$\map f x = \size x = \begin{cases}
x & : x > 0 \\
0 & : x = 0 \\
-x & : x < 0
\end{cases}$</nowiki>
From Fourier Series for Absolute Value Function over Symmetric Range, $\map f x$ can immediately be expressed as:
:$\ds \map f x \sim \frac \lambda 2 - \frac {4 \lambda} {\pi^2} \sum_{n \mathop = 0}^\infty \frac 1 {\paren {2 n + 1}^2} \cos \dfrac {\paren {2 n + 1} \pi x} \lambda$
{{finish|We need a result that the Fourier series over an interval is the restriction of the resulting periodic function.}}
Theorem: Fourier Series/Sawtooth Wave

600pxthumbrightSawtooth Wave and $6$th Approximation
Let $\map S x$ be the sawtooth wave defined on the real numbers $\R$ as:
:$\forall x \in \R: \map S x = \begin {cases} x & : x \in \openint {-l} l \\ \map S {x + 2 l} & : x < -l \\ \map S {x - 2 l} & : x > +l \end {cases}$
where $l$ is a given real constant.
Then its Fourier series can be expressed as:
{{begin-eqn}}
{{eqn | l = \map S x
      | o = \sim
      | r = \frac {2 l} \pi \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} } n \sin \dfrac {n \pi x} l
      | c = 
}}
{{eqn | r = \frac {2 l} \pi \paren {\sin \dfrac {\pi x} l - \frac 1 2 \sin \dfrac {2 \pi x} l + \frac 1 3 \sin \dfrac {3 \pi x} l + \dotsb}
      | c = 
}}
{{end-eqn}}

Proof:
Let $\map f x: \openint {-l} l \to \R$ denote the identity function on the open interval $\openint {-l} l$:
:$\map f x = x$
From Fourier Series for Identity Function over Symmetric Range, $\map f x$ can immediately be expressed as:
:$\ds \map f x \sim \frac {2 l} \pi \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} } n \sin \dfrac {n \pi x} l$
{{finish|We need a result that the Fourier series over an interval is the restriction of the resulting periodic function.}}
Theorem: Subspace of Product Space is Homeomorphic to Factor Space/Product with Singleton/Lemma

:$f$ is a bijection.

Proof:
=== $f$ is an Injection ===
Let $x, y \in T_1$.
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \map f y
}}
{{eqn | ll = \leadstoandfrom
      | l = \tuple {x, b}
      | r = \tuple {y, b}
      | c = Definition of $f$
}}
{{eqn | ll = \leadstoandfrom
      | l = x
      | r = y
      | c = Equality of ordered pairs
}}
{{end-eqn}}
Then $f$ is an injection by definition.
{{qed|lemma}}