avewright/proofwiki-math huggingface dataset:
Theorem: Hyperbolic Cosine of Zero is One

:$\map \cosh 0 = 1$
where $\cosh$ denotes the hyperbolic cosine.

Proof:
{{begin-eqn}}
{{eqn | l = \map \cosh 0
      | r = \dfrac {e^0 + e^{-0} } 2
      | c = {{Defof|Hyperbolic Cosine}}
}}
{{eqn | r = \dfrac {1 + 1} 2
      | c = {{Defof|Integer Power}}
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Binomial Theorem/Approximations/1st Order

When $x$ is sufficiently small that $x^2$ can be neglected then:
:$\paren {1 + x}^\alpha \approx 1 + \alpha x$
and the error is of the order of $\dfrac {\alpha \paren {\alpha - 1} } 2 x^2$

Proof:
{{ProofWanted|Not sure how this is formulated yet, I need a more precise definition and source work}}
Theorem: Binomial Theorem/Approximations/2nd Order

When $x$ is sufficiently small that $x^3$ can be neglected, then:
:$\paren {1 + x}^\alpha \approx 1 + \alpha x + \dfrac {\alpha \paren {\alpha - 1} } 2 x^2$
and the error is of the order of:
:$\dfrac {\alpha \paren {\alpha - 1} \paren {\alpha - 2} } 6 x^3$

Proof:
{{ProofWanted|Not sure how this is formulated yet, I need a more precise definition and source work}}
Theorem: Normed Vector Space with Schauder Basis is Separable

Let $\struct {X, \norm {\, \cdot \,}}$ be a normed vector space over $\R$.
Suppose $X$ admits a Schauder basis.
Then $X$ is separable.

Proof:
Let $\set {\mathbf E_i : i \in \N}$ be a Schauder basis.
Then:
:$\ds \forall x \in X : \exists \sequence {x_i'}_{i \mathop \in \N} \in \R : x = \sum_{i \mathop = 0}^\infty x_i' \mathbf E_i$
Let $\ds \mathbf e_i = \frac {\mathbf E_i}{\norm {\mathbf E_i}}$ and $\ds x_i=x_i' \norm{\mathbf E_i}$.
Then $\ds x = \sum_{i \mathop = 0}^\infty x_i \mathbf e_i$ where $\forall i \in \N : \norm {\mathbf e_i} = 1$.
Let $\ds Y = \set {\sum_{i \mathop = 0}^n q_i \mathbf e_i : q_i \in \Q, n \in \N}$ be a countable set.
$Y$ is spanned by $\set {\mathbf e_i : i \in \N}$.
Also, Rational Numbers form Subset of Real Numbers.
Hence, $Y \subseteq X$.
We have that rationals are everywhere dense in reals.
Then for any $i \in \N$:
:$\forall x_i \in \R: \forall \epsilon_i \in \R_{>0}: \exists q_i \in \Q: \size {x_i - q_i} < \epsilon_i$
Hence:
{{begin-eqn}}
{{eqn | l = \norm {\sum_{i \mathop = 0}^n x_i \mathbf e_i - \sum_{i \mathop = 0}^n q_i \mathbf e_i}
      | r = \norm {\sum_{i \mathop = 0}^n \paren {x_i - q_i} \mathbf e_i}
}}
{{eqn | o = \le
      | r = \sum_{i \mathop = 0}^n \norm {\paren {x_i - q_i} \mathbf e_i}
      | c = {{NormAxiomVector|3}}
}}
{{eqn | r = \sum_{i \mathop = 0}^n \size {x_i - q_i} \norm {\mathbf e_i}
      | c = {{NormAxiomVector|2}}
}}
{{eqn | r = \sum_{i \mathop = 0}^n \size {x_i - q_i}
}}
{{eqn | o = <
      | r = \sum_{i \mathop = 0}^n \epsilon_i
}}
{{end-eqn}}
By the existence of Schauder basis, the limit $\ds x = \sum_{i \mathop = 0}^\infty x_i \mathbf e_i$ exists.
Thus:
:$\ds \forall \epsilon' \in \R_{>0}: \exists N \in \R_{>0}: \forall n \in \N: n > N \implies \norm {\sum_{i \mathop = 0}^\infty x_i \mathbf e_i - \sum_{i \mathop = 0}^n x_i \mathbf e_i} < \epsilon'$
Therefore:
{{begin-eqn}}
{{eqn | l = \norm {x - \sum_{i \mathop = 0}^n q_i \mathbf e_i}
      | r = \norm {x - \sum_{i \mathop = 0}^n x_i \mathbf e_i + \sum_{i \mathop = 0}^n x_i \mathbf e_i - \sum_{i \mathop = 0}^n q_i \mathbf e_i}
}}
{{eqn | o = \le
      | r = \norm {x - \sum_{i \mathop = 0}^n x_i \mathbf e_i} + \norm{\sum_{i \mathop = 0}^n x_i \mathbf e_i - \sum_{i \mathop = 0}^n q_i \mathbf e_i}
      | c = {{NormAxiomVector|3}}
}}
{{eqn | o = <
      | r = \epsilon' + \sum_{i \mathop = 0}^n \epsilon_i
}}
{{end-eqn}}
Let $\epsilon \in \R_{> 0}$. 
Let $\epsilon'$ and $\sequence {\epsilon_i}_{0 \mathop \le i \le n}$ be such that:
:$\ds \epsilon > \epsilon' + \sum_{i \mathop = 0}^n \epsilon_i$.
Let $n > N$.
Then:
:$\ds \norm {x - \sum_{i \mathop = 0}^n q_i \mathbf e_i} < \epsilon$
$\epsilon$ was arbitrary.
Altogether:
:$\ds \forall x \in X : \forall \epsilon \in \R_{> 0} : \exists y_{i \mathop \in \N} \in Y : \norm {x - y_i} < \epsilon$
By definition, $X$ is separable.
{{qed}}
Theorem: Greatest Term of Binomial Expansion/Examples/Arbitrary Example 1

Consider the expression:
:$E = \paren {1 + 2 x}^{10 \frac 1 2}$
Let $x = \dfrac 3 7$.
Then the greatest term in the power series expansion of $E$ by means of the General Binomial Theorem is:
{{begin-eqn}}
{{eqn | o = 
      | r = \dfrac {21 \times 19 \times 17 \times 15 \times 13} {5!} \paren {\dfrac 3 7}^5
}}
{{eqn | o = \approx
      | r = 159 \cdotp 36
      | c = 
}}
{{end-eqn}}

Proof:
Let us perform the expansion:
:$\paren {1 + 2 x}^{\frac {21} 2} = 1 + \dfrac {21} 2 \paren {2 x} + \dfrac {\paren {\frac {21} 2} \paren {\frac {19} 2} } {2!} \paren {2 x}^2 + \dfrac {\paren {\frac {21} 2} \paren {\frac {19} 2} \paren {\frac {17} 2} } {3!} \paren {2 x}^3 + \cdots$
Consider the $\paren {r + 1}$th term:
:$u_{r + 1} = \dfrac {\paren {\frac {21} 2} \paren {\frac {19} 2} \cdots \paren {\frac {23} 2 - r} } {r!} \paren {2 x}^r$
Hence $u_{r + 1} > u_r$ if:
{{begin-eqn}}
{{eqn | q = 
      | l = u_{r + 1}
      | o = >
      | r = u_r
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\paren {\frac {21} 2} \paren {\frac {19} 2} \cdots \paren {\frac {23} 2 - r} } {r!} \paren {2 x}^r
      | o = >
      | r = \dfrac {\paren {\frac {21} 2} \paren {\frac {19} 2} \cdots \paren {\frac {25} 2 - r} } {\paren {r - 1}!} \paren {2 x}^{r - 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\paren {\frac {23} 2 - r} } r \paren {2 x}
      | o = >
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {\frac {23} 2 - r} \paren {\dfrac 6 7}
      | o = >
      | r = r
      | c = setting $x = \dfrac 3 7$
}}
{{eqn | ll= \leadsto
      | l = 69 - 6 r
      | o = >
      | r = 7 r
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 13 r
      | o = <
      | r = 69
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r
      | o = <
      | r = 5 \tfrac 4 {13}
      | c = 
}}
{{end-eqn}}
So:
:if $r < 5 \tfrac 4 {13}$ then $u_{r + 1} > u_r$
but conversely:
:if $r > 5 \tfrac 4 {13}$ then $u_{r + 1} < u_r$
Hence the greatest value of $r$ for which $u_{r + 1} > u_r$ is $5$.
Then we have that:
:$u_6 > u_5$
but then:
:$u_7 < u_6$
Hence the $6$th term is greatest:
{{begin-eqn}}
{{eqn | l = u_6
      | r = \dfrac {\paren {\frac {21} 2} \paren {\frac {19} 2} \paren {\frac {17} 2} \paren {\frac {15} 2} \paren {\frac {13} 2} } {5!} \paren {2 x}^5
      | c = 
}}
{{eqn | r = \dfrac {21 \times 19 \times 17 \times 15 \times 13} {2^5 \times 5!} \paren {\dfrac 6 7}^5
      | c = 
}}
{{eqn | r = \dfrac {21 \times 19 \times 17 \times 15 \times 13} {5!} \paren {\dfrac 3 7}^5
      | c = 
}}
{{eqn | o = \approx
      | r = 159 \cdotp 36
      | c = performing the arithmetic
}}
{{end-eqn}}
{{qed}}
Theorem: Weierstrass Approximation Theorem/Complex Case

Let $\Bbb I = \closedint a b$ be a closed real interval.
Let $f: \Bbb I \to \C$ be a continuous complex function. 
Let $\epsilon \in \R_{>0}$.
Then there exists a complex polynomial function $p : \Bbb I \to \C$ such that:
:$\norm {p - f}_\infty < \epsilon$
where $\norm f_\infty$ denotes the supremum norm of $f$ on $\Bbb I$.

Proof:
Let $\Re f : \Bbb \to \R$ be the real function defined by:
:$\map {\Re f} x = \map \Re {\map f x}$
where $\map \Re z$ denotes the real part of a complex number $z \in \C$.
Let $\Im f : \Bbb \to \R$ be the real function defined by:
:$\map {\Im f} x = \map \Im {\map f x}$
where $\map \Im z$ denotes the imaginary part of $z \in \C$.
From Real and Imaginary Part Projections are Continuous and Composite of Continuous Mappings is Continuous, it follows that $\Re f$ and $\Im f$ are continuous functions.
By the Weierstrass Approximation Theorem, there exist two real polynomial functions $u, v: \Bbb I \to \R$ such that:
:$\norm {u - \Re f}_\infty < \dfrac \epsilon 2$
:$\norm {v - \Im f}_\infty < \dfrac \epsilon 2$
Set $p := u + iv$, so $p$ becomes a complex polynomial function.
Then:
{{begin-eqn}}
{{eqn | l = \norm {p - f}_\infty
      | r = \sup_{x \mathop \in \Bbb I} \size {\map p x - \map f x}
      | c = {{Defof|Supremum Norm}}
}}
{{eqn | r = \sup_{x \mathop \in \Bbb I} \size {\map u x + i \map v x - \map \Re {\map f x} - i \map \Im {\map f x} }
      | c = {{Defof|Complex Number}}
}}
{{eqn | o = \le
      | r = \sup_{x \mathop \in \Bbb I} \size {\map u x - \map \Re {\map f x} } + \sup_{x \mathop \in \Bbb I} \size i \size {\map v x - \map \Im {\map f x} }
      | c = Triangle Inequality for Complex Numbers
}}
{{eqn | r = \norm {u - \Re f}_\infty + \norm {v - \Im f}_\infty
      | c = {{Defof|Supremum Norm}}, and complex modulus of $i$
}}
{{eqn | o = <
      | r = \dfrac \epsilon 2 + \dfrac \epsilon 2
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
{{qed}}
Category:Weierstrass Approximation Theorem
fa5f7lfasqvpyyvk7qm7gptwd4i5vre
Theorem: Complex Numbers with Complex Modulus form Normed Vector Space

Let $\C$ be the set of complex numbers.
Let $\size {\, \cdot \,}$ be the complex modulus.
Then $\struct {\C, \size {\, \cdot \,}}$ is a normed vector space.

Proof:
We have that:
:Complex Numbers form Vector Space over Themselves
:Complex Modulus is Norm
By definition, $\struct {\C, \size {\, \cdot \,}}$ is a normed vector space.
{{qed}}
Theorem: Gaussian Rationals are Everywhere Dense in Complex Numbers

Let $\struct {\C, \cmod {\, \cdot \,}}$ be the normed vector space of complex numbers.
Let $\Q \sqbrk i = \set {a + i b: a, b \in \Q}$ be the set of Gaussian rational numbers.
Then $\Q \sqbrk i$ is everywhere dense in $\struct {\C, \cmod {\, \cdot \,}}$.

Proof:
Let $z = x + i y \in \C$ be a complex number.
Let $q = a + i b \in \Q \sqbrk i$ be a Gaussian rational number.
Then:
{{begin-eqn}}
{{eqn | l = \cmod {z - q}
      | r = \cmod {\paren {x + i y} - \paren {a + i b} }
}}
{{eqn | r = \cmod {x - a + i \paren {y - b} }
}}
{{eqn | o = \le
      | r = \cmod {x - a} + \cmod {i \paren {y - b} }
      | c = {{NormAxiomVector|3}}
}}
{{eqn | r = \size {x - a} + \size {y - b}
}}
{{end-eqn}}
We have that rationals are everywhere dense in reals.
Then:
:$\forall x \in \R: \forall \epsilon_x \in \R_{> 0}: \exists a \in \Q: \size {x - a} < \epsilon_x$
:$\forall y \in \R: \forall \epsilon_y \in \R_{> 0}: \exists b \in \Q: \size {y - b} < \epsilon_y$
Let $\epsilon \in \R_{> 0}$.
Let $\epsilon_x, \epsilon_y \in \R_{> 0}$ be such that $\epsilon_x + \epsilon_y < \epsilon$.
Then:
:$\exists q \in \Q \sqbrk i: \cmod {z - q} < \epsilon$
$z$ and $\epsilon$ were arbitary.
Therefore:
:$\forall z \in \C: \forall \epsilon \in \R_{> 0}: \exists q \in \Q \sqbrk i: \cmod {z - q} < \epsilon$
By definition, $\Q \sqbrk i$ is everywhere dense in $\C$.
{{qed}}
Category:Denseness
Category:Complex Numbers
Category:Gaussian Rationals
pscb60hrunu7ds7xixqka7etp824zsz
Theorem: Square Root of Function under Derivative

:$\ds \int \dfrac {\map {f'} x} {\sqrt {\map f x} } \rd x = 2 \sqrt {\map f x} + C$

Proof:
Let $u = \map f x$.
Then:
:$\dfrac {\d u} {\d x} = \map {f'} x$
Hence:
{{begin-eqn}}
{{eqn | l = \int \dfrac {\d u} {\d x} \dfrac 1 {\sqrt {\map f x} } \rd x
      | r = \int \dfrac {\d u} {\sqrt u}
      | c = Integration by Substitution
}}
{{eqn | r = 2 \sqrt u + C
      | c = Primitive of Power
}}
{{eqn | r = 2 \sqrt {\map f x} + C
      | c = Primitive of Power
}}
{{end-eqn}}
{{qed}}
Theorem: Normed Vector Space over Complex Numbers with Schauder Basis is Separable

Let $\struct {X, \norm {\, \cdot \,}}$ be a normed vector space over $\C$.
Suppose $X$ admits a Schauder basis.
Then $X$ is separable.

Proof:
Let $\set {\mathbf E_i : i \in \N}$ be a Schauder basis.
Then:
:$\ds \forall x \in X : \exists \sequence {x_i'}_{i \mathop \in \N} \in \C : x = \sum_{i \mathop = 0}^\infty x_i' \mathbf E_i$
Let $\ds \mathbf e_i = \frac {\mathbf E_i}{\norm {\mathbf E_i}}$ and $\ds x_i=x_i' \norm{\mathbf E_i}$.
Then $\ds x = \sum_{i \mathop = 0}^\infty x_i \mathbf e_i$ where $\forall i \in \N : \norm {\mathbf e_i} = 1$.
Let $\ds Y = \set {\sum_{i \mathop = 0}^n q_i \mathbf e_i : q_i \in \Q \sqbrk i, n \in \N}$ be a countable set.
$Y$ is spanned by $\set {\mathbf e_i : i \in \N}$.
Also, Gaussian Rational Numbers form Subset of Complex Numbers.
Hence, $Y \subseteq X$.
We have that Gaussian Rationals are Everywhere Dense in Complex Numbers.
Then for any $i \in \N$:
:$\forall x_i \in \C: \forall \epsilon_i \in \R_{>0}: \exists q_i \in \Q \sqbrk i: \size {x_i - q_i} < \epsilon_i$
Hence:
{{begin-eqn}}
{{eqn | l = \norm {\sum_{i \mathop = 0}^n x_i \mathbf e_i - \sum_{i \mathop = 0}^n q_i \mathbf e_i}
      | r = \norm {\sum_{i \mathop = 0}^n \paren {x_i - q_i} \mathbf e_i}
}}
{{eqn | o = \le
      | r = \sum_{i \mathop = 0}^n \norm {\paren {x_i - q_i} \mathbf e_i}
      | c = {{NormAxiomVector|3}}
}}
{{eqn | r = \sum_{i \mathop = 0}^n \size {x_i - q_i} \norm {\mathbf e_i}
      | c = {{NormAxiomVector|2}}
}}
{{eqn | r = \sum_{i \mathop = 0}^n \size {x_i - q_i}
}}
{{eqn | o = <
      | r = \sum_{i \mathop = 0}^n \epsilon_i
}}
{{end-eqn}}
By the existence of Schauder basis, the limit $\ds x = \sum_{i \mathop = 0}^\infty x_i \mathbf e_i$ exists.
Thus:
:$\ds \forall \epsilon' \in \R_{>0}: \exists N \in \R_{>0}: \forall n \in \N: n > N \implies \norm {\sum_{i \mathop = 0}^\infty x_i \mathbf e_i - \sum_{i \mathop = 0}^n x_i \mathbf e_i} < \epsilon'$
Therefore:
{{begin-eqn}}
{{eqn | l = \norm {x - \sum_{i \mathop = 0}^n q_i \mathbf e_i}
      | r = \norm {x - \sum_{i \mathop = 0}^n x_i \mathbf e_i + \sum_{i \mathop = 0}^n x_i \mathbf e_i - \sum_{i \mathop = 0}^n q_i \mathbf e_i}
}}
{{eqn | o = \le
      | r = \norm {x - \sum_{i \mathop = 0}^n x_i \mathbf e_i} + \norm{\sum_{i \mathop = 0}^n x_i \mathbf e_i - \sum_{i \mathop = 0}^n q_i \mathbf e_i}
      | c = {{NormAxiomVector|3}}
}}
{{eqn | o = <
      | r = \epsilon' + \sum_{i \mathop = 0}^n \epsilon_i
}}
{{end-eqn}}
Let $\epsilon \in \R_{> 0}$. 
Let $\epsilon'$ and $\sequence {\epsilon_i}_{0 \mathop \le i \le n}$ be such that:
:$\ds \epsilon > \epsilon' + \sum_{i \mathop = 0}^n \epsilon_i$.
Let $n > N$.
Then:
:$\ds \norm {x - \sum_{i \mathop = 0}^n q_i \mathbf e_i} < \epsilon$
$\epsilon$ was arbitrary.
Altogether:
:$\ds \forall x \in X : \forall \epsilon \in \R_{> 0} : \exists y_{i \mathop \in \N} \in Y : \norm {x - y_i} < \epsilon$
By definition, $X$ is separable.
{{qed}}
Category:Schauder Bases
Category:Normed Vector Spaces
Category:Separable Spaces
dmweszk3aar0xr4a2nv3uskht9z47s4
Theorem: Orthogonal Projection is Mapping

Let $H$ be a Hilbert space.
Let $K$ be a closed linear subspace of $H$.
Let $P_K: H \to H$ be the orthogonal projection on $K$.
Then $P_K$ is a mapping.

Proof:
For $P_K$ to be a mapping we need to show that:
:$\forall h \in H: \map{P_K} h$ exists and is unique
By definition of $\map{P_K} h$, this amounts to:
:There is a unique $k \in K$ such that $\norm{ h - k } = \map d {h, K}$
This is precisely the statement of Unique Point of Minimal Distance to Closed Convex Subset of Hilbert Space.
{{qed}}
Theorem: Fourier Transform of 1-Lebesgue Space Function is Bounded

Let $n \in \N_{>0}$.
Let $\map {L^1} {\R^n}$ be the complex-valued Lebesgue $1$-space with respect to the Lebesgue measure.
Let $f \in \map {L^1} {\R^n}$.
Let $\hat f$ be the Fourier transform of $f$.
Then:
:$\ds \sup_{\mathbf s \mathop \in \R^n} \cmod {\map {\hat f} {\mathbf s} } \le \norm f_{\map {L^1} {\R^n} }$

Proof:
For each $\mathbf s \in \R^n$:
{{begin-eqn}}
{{eqn | l = \cmod { \map {\hat f} {\mathbf s} }
      | r = \cmod { \int_{\R^n} \map f {\mathbf x} e^{-2 \pi i \mathbf x \cdot \mathbf s} \rd \mathbf x }
      | c = {{Defof|Fourier Transform}}
}}
{{eqn | o = \le
      | r = \int_{\R^n} \cmod { \map f {\mathbf x} e^{-2 \pi i \mathbf x \cdot \mathbf s} } \rd \mathbf x
      | c = Triangle Inequality for Integrals
}}
{{eqn | r = \int_{\R^n} \cmod { \map f {\mathbf x} } \rd \mathbf x
      | c = Modulus and Argument of Complex Exponential
}}
{{eqn | r = \norm f_{\map {L^1} {\R^n} }
      | c = {{Defof|Lp Norm|$L^1$ Norm}}
}}
{{end-eqn}}
{{qed}}
Category:Fourier Transforms
oitram70uvtdmsx0u06yz3m120bv9ah
Theorem: Primitive of p x + q over a x squared plus 2 b x plus c

:$\ds \int \dfrac {p x + q} {a x^2 + 2 b x + c} \rd x = \dfrac p {2 a} \ln \size {a x^2 + 2 b x + c} + \paren {q - \dfrac {p b} a} \int \dfrac {\d x} {a^2 + 2 b x + c} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \dfrac {p x + q} {a x^2 + 2 b x + c} \rd x
      | r = p \int \dfrac x {a x^2 + 2 b x + c} \rd x + q \int \dfrac {\rd x} {a x^2 + 2 b x + c} 
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac p {2 a} \ln \size {a x^2 + 2 b x + c} - \frac {p b} a \int \frac {\d x} {a x^2 + 2 b x + c} + q \int \dfrac {\rd x} {a x^2 + 2 b x + c}  + C
      | c = Primitive of $\dfrac x {a x^2 + b x + c}$
}}
{{eqn | r = \dfrac p {2 a} \ln \size {a x^2 + 2 b x + c} + \paren {q - \dfrac {p b} a} \int \dfrac {\d x} {a^2 + 2 b x + c} + C 
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Orthogonal Projection onto Orthocomplement

Let $H$ be a Hilbert space.
Let $A$ be a closed linear subspace of $H$.
Let $P_A: H \to H$ be the orthogonal projection onto $A$.
Let $P_{A^\perp}: H \to H$ be the orthogonal projection onto $A^\perp$, the orthocomplement of $A$.
Let $I: H \to H$ be the identity operator on $H$.
Then:
:$P_{A^\perp} = I - P_A$

Proof:
Let $h \in H$.
By definition of orthogonal projection, $P_A h = a \in A$ such that $h - a \in A^\perp$.
Then the claim is that for all $h \in H$:
:$\paren {I - P_A } h = h - P_A h$
is in $A^\perp$, and:
:$h - \paren {h - P_A h} \in \paren {A^\perp}^\perp$
That $h - P_A h \in A^\perp$ is part of the definition of $P_A$.
For the other criterion, note:
:$h - \paren {h - P_A h} = P_A h \in A$
By {{Corollary|Double Orthocomplement is Closed Linear Span}}:
:$\paren{ A^\perp }^\perp = A$
{{qed}}
Theorem: Cesàro Summation Operator is Continuous Linear Transformation

Let $\ell^\infty$ be the space of bounded sequences.
Let $A : \ell^\infty \to \ell^\infty$ be the Cesàro summation operator.
Then $A$ is a continuous linear transformation.

Proof:
=== Well-Definedness ===
Let $\mathbf x = \sequence {x_n}_{n \mathop \in \N} \in \ell^\infty$.
Then:
{{begin-eqn}}
{{eqn | q = \forall n \in \N 
      | l = \size {x_n} 
      | o = \le 
      | r = \sup_{n \mathop \in \N} \size {x_n}
}}
{{eqn | r = \norm {\mathbf x}_\infty
      | c = {{Defof|Supremum Norm}}
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \size {\sum_{i \mathop = 1}^n\frac{x_i} n }
      | o = \le
      | r = \frac 1 n \sum_{i \mathop = 1}^n \size {x_i}
      | c = General Triangle Inequality for Complex Numbers
}}
{{eqn | o = \le
      | r = \frac 1 n \sum_{i \mathop = 1}^n \sup_{n \mathop \in \N} \size {x_i}
}}
{{eqn | r = \frac 1 n n \norm {\mathbf x}_\infty
      | c = {{Defof|Supremum Norm}}
}}
{{eqn | r = \norm {\mathbf x}_\infty
}}
{{end-eqn}}
Hence:
:$A \mathbf x \in \ell^\infty$
{{Research|Clarify connection to the {{Defof|Well-Defined Mapping}} }}
{{qed|lemma}}
Theorem: Primitive of p x + q over Root of a x squared plus 2 b x plus c

:$\ds \int \dfrac {p x + q} {\sqrt {a x^2 + 2 b x + c} } \rd x = \dfrac p a \sqrt {a x^2 + 2 b x + c} + \paren {q - \dfrac {p b} a} \int \dfrac {\d x} {\sqrt {a x^2 + 2 b x + c} }$

Proof:
{{begin-eqn}}
{{eqn | l = \int \dfrac {p x + q} {\sqrt {a x^2 + 2 b x + c} } \rd x
      | r = \dfrac p {2 a} \int \dfrac {2 a x + \frac {2 a q} p} {\sqrt {a x^2 + 2 b x + c} } \rd x
      | c = 
}}
{{eqn | r = \dfrac p {2 a} \int \dfrac {2 a x + 2 b - 2 b + \frac {2 a q} p} {\sqrt {a x^2 + 2 b x + c} } \rd x
      | c = 
}}
{{eqn | r = \dfrac p {2 a} \int \dfrac {2 a x + 2 b} {\sqrt {a x^2 + 2 b x + c} } \rd x + \dfrac p {2 a} \paren {\dfrac {2 a q} p - 2 b} \int \dfrac {\d x} {\sqrt {a x^2 + 2 b x + c} }
      | c = Linear Combination of Primitives
}}
{{eqn | r = \dfrac p {2 a} \int \dfrac {2 a x + 2 b} {\sqrt {a x^2 + 2 b x + c} } \rd x + \paren {q - \dfrac {p b} a} \int \dfrac {\d x} {\sqrt {a x^2 + 2 b x + c} }
      | c = simplifying
}}
{{eqn-intertext|We have from Power Rule for Derivatives that $\map {\dfrac \d {\d x} } {a x^2 + b x + c} {{=}} 2 a x + 2 b$, so:}}
{{eqn | r = \dfrac p {2 a} \paren {2 \sqrt {a x^2 + 2 b x + c} } + \paren {q - \dfrac {p b} a} \int \dfrac {\d x} {\sqrt {a x^2 + 2 b x + c} }
      | c = Square Root of Function under Derivative
}}
{{eqn | r = \dfrac p a \sqrt {a x^2 + 2 b x + c} + \paren {q - \dfrac {p b} a} \int \dfrac {\d x} {\sqrt {a x^2 + 2 b x + c} }
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: All Normal Vectors of Simple Closed Contour Cannot Point into Interior

Let $C$ be a simple closed contour in the complex plane $\C$ with parameterization $\gamma: \closedint a b \to \C$.
Let $t \in \openint a b$ such that $\gamma$ is complex-differentiable at $t$.
Let $S \in \set {-1,1}$.
Let $\Int C$ denote the interior of $C$.
Then there exists $r_0 \in \R_{>0}$ such that:
:for all $\epsilon \in \openint 0 {r_0}$, we have $\map \gamma {t} + \epsilon i S \map {\gamma '}{ t } \in \Int C$
{{iff}} there exists $r_1 \in \R_{>0}$ such that:
:for all $\epsilon \in \openint 0 {r_1}$, we have $\map \gamma {t} - \epsilon i S \map {\gamma '}{ t } \notin \Int C$.

Proof:
From Normal Vectors Form Space around Simple Complex Contour, it follows that there exists $\tilde r, \tilde R \in \R_{>0}$ such that:
:for all $s \in \openint { t - \tilde R }{ t + \tilde R }$ and for all $\epsilon \in \openint 0 {\tilde r}$: $\map \gamma s + \epsilon i \map {\gamma'} s \notin \Img C$, and $\map \gamma s - \epsilon i \map {\gamma'} s \notin \Img C$
where $\Img C$ denotes the image of $C$.
From the Lemma, we find an open set $V_{r,R} \subseteq \C$ with $r \le \tilde r, R \le \tilde R$.
Let $z_1, z_2 \in V_{r,R}$.
Then there exist $s_1 , s_2 \in \openint { t-R }{ t+R }$ and $\epsilon_1 , \epsilon_2 \in \openint 0 r$ with $S_0 \in \set {-1,1}$ such that:
:$z_1 = \map \gamma {s_1} + \epsilon_1 i S_0 \map {\gamma'}{ s_1 } \in V_{r,R}, z_2 = \map \gamma {s_2} + \epsilon_2 i S_0 \map {\gamma'}{ s_2 } \in V_{r,R}$.
We now define a path $f: \closedint 0 1 \to V_{r,R}$  with endpoints $z_1$ and $z_2$ by:
:$\map f {\hat t} =  \map \gamma { s_1 + \paren{ s_2 - s_1} \hat t } + \paren{ \epsilon_1 + \paren{ \epsilon_2 - \epsilon_1 } \hat t } i S_0 \map {\gamma'}{ s_1 + \paren{ s_2 - s_1} \hat t  }$
As $\paren{ \epsilon_1 + \paren{ \epsilon_2 - \epsilon_1 } \hat t } \in \openint 0 r$, it follows that $\map f {\hat t} \notin \Img C$ for all $\hat t \in \closedint 0 1$.
Complex Plane is Homeomorphic to Real Plane shows that we can identify the complex plane $\C$ with the real plane $\R^2$ by the homeomorphism $\map \phi {x, y} = x + i y$.
Interior of Simple Closed Contour is Well-Defined shows that $\Img C$ can be identified with the image of a Jordan curve $g: \R^2 \to \R^2$.
From the same theorem, it follows that $\Int C$ can be identified with the interior of $g$.
From the Jordan Curve Theorem, it follows that $\C \setminus \Img C$ is a union of two open connected components, which are $\Int C$ and the exterior of $g$, which we denote $\Ext C$.
From Connected Open Subset of Euclidean Space is Path-Connected, it follows that $\Int C$ and $\Ext C$ are path components of $\C \setminus \Img C$.