avewright/proofwiki-math huggingface dataset:
Theorem: Zero Complement is Not Empty

Let $\struct {S, \circ, \preceq}$ be a naturally ordered semigroup.
Let $S^*$ be the zero complement of $S$.
Then $S^*$ is not empty.

Proof:
From {{NOSAxiom|4}}, we have:
:$\exists m, n \in S: m \ne n$
That is, there are at least two distinct elements in $S$.
Therefore, there must be at least one element in $S^* = S \setminus \set 0$.
So:
:$S^* = S \setminus \set 0 \ne \O$
{{qed}}
Theorem: Stirling's Formula/Proof 2/Lemma 5

:$\dfrac {n!} {n^n \sqrt n e^{-n} } \to \sqrt {2 \pi}$ as $n \to \infty$

Proof:
By previous work done in Stirling's Formula: Proof 2 it is noted that $\sequence {\dfrac {n!} {n^n \sqrt n e^{-n} } }_{n \mathop \in \N}$ is a convergent sequence.
Let $\dfrac {n!} {n^n \sqrt n e^{-n} } \to C$ as $n \to \infty$.
Let $\ds I_n = \int_0^{\frac \pi 2} \sin^n x \rd x$.
Then:
{{begin-eqn}}
{{eqn | l = \frac {I_{2 n} } {I_{2 n + 1} }
      | r = \frac {\paren {2 n}!} {\paren {2^n n!}^2} \frac \pi 2 \cdot \frac {\paren {2 n + 1}!} {\paren {2^n n!}^2}
      | c = Definite Integral from $0$ to $\dfrac \pi 2$ of Even Power of $\sin x$ and Corollary 2
}}
{{eqn | r = \frac \pi 2 \paren {2 n + 1} \frac {\paren {\paren {2 n}!}^2} {\paren {2^n n!}^4}
      | c = extracting $\paren {2 n + 1}$ as a factor and rearranging
}}
{{eqn | o = \sim
      | r = \frac \pi 2 \paren {2 n + 1} \frac {\paren {C \paren {2 n}^{2 n + 1/2} e^{-2 n} }^2} {\paren {2^n C n^{n + 1/2} e^{-n} }^4}
      | c = entering $C$ into top and bottom
}}
{{eqn | r = \frac \pi 2 \frac {\paren {2 n + 1} } {C^2} \frac {2^{4 n} 2 \paren {n^{4 n + 1} } e^{-4 n} } {2^{4 n} \paren {n^{4 n + 2} } e^{-4 n} }
      | c = rearranging
}}
{{eqn | r = \frac {\pi \paren {2 n + 1} } {n C^2}
      | c = much simplification
}}
{{eqn | o = \to
      | r = \frac {2 \pi} {C^2}
      | rr= \text {as $n \to \infty$}
}}
{{end-eqn}}
From Lemma 4:
:$\ds \lim_{n \mathop \to \infty} \frac {I_{2 n} } {I_{2 n + 1} } = 1$
from which:
{{begin-eqn}}
{{eqn | l = \frac {2 \pi} {C^2}
      | r = 1
}}
{{eqn | ll= \leadsto
      | l = C^2
      | r = 2 \pi
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Zero Strictly Precedes One

Let $\struct {S, \circ, \preceq}$ be a naturally ordered semigroup.
Let $0$ be the zero of $S$.
Let $1$ be the one of $S$.
Then:
:$0 \prec 1$

Proof:
This follows directly from the definition of $\prec$.
First note that:
:$\forall n \in S: 0 \preceq n$
from the definition of zero.
Next, from the definition of one:
:$0 \ne 1$
Thus:
{{begin-eqn}}
{{eqn | o = 
      | r = 0 \preceq 1 \land 0 \ne 1
}}
{{eqn | o = \leadsto
      | r = 0 \prec 1
      | c = {{Defof|Strictly Precede}}
}}
{{end-eqn}}
{{Qed}}
Theorem: Stirling's Formula/Proof 2/Lemma 2

The sequence $\sequence {d_n}$ defined as:
:$d_n = \map \ln {n!} - \paren {n + \dfrac 1 2} \ln n + n$
is decreasing.

Proof:
The proof strategy is to demonstrate that the sign of $d_n - d_{n + 1}$ is positive.
{{begin-eqn}}
{{eqn | l = d_n - d_{n + 1}
      | r = \map \ln {n!} - \paren {n + \frac 1 2} \ln n + n
      | c = 
}}
{{eqn | o = 
      | ro= -
      | r = \paren {\map \ln {\paren {n + 1}!} - \paren {n + 1 + \frac 1 2} \map \ln {n + 1} + n + 1}
      | c = 
}}
{{eqn | r = -\map \ln {n + 1} - \paren {n + \frac 1 2} \ln n + \paren {n + \frac 3 2} \map \ln {n + 1} - 1
      | c = (as $\map \ln {\paren {n + 1}!} = \map \ln {n + 1} + \map \ln {n!}$)
}}
{{eqn | r = \paren {n + \frac 1 2} \map \ln {\frac {n + 1} n} - 1
      | c =
}}
{{eqn | n = 1
      | r = \frac {2 n + 1} 2 \map \ln {\frac {1 + \paren {2 n + 1}^{-1} } {1 - \paren {2 n + 1}^{-1} } } - 1
      | c =
}}
{{end-eqn}}
Let:
:$\map f x := \dfrac 1 {2 x} \map \ln {\dfrac {1 + x} {1 - x} } - 1$
for $\size x < 1$.
Then from Lemma 1:
:$(2): \quad \ds \map f x = \sum_{k \mathop = 1}^\infty \frac {x^{2 n} } {2 n + 1}$
Thus $\map f x > 0$ for $\size x < 1$.
Putting $x = \dfrac 1 {2 n + 1}$ it can be seen that $(1)$ is $\map f {\dfrac 1 {2 n + 1} }$.
As $-1 < \dfrac 1 {2 n + 1} < 1$ it can be seen that $(2)$ can be applied and so:
:$\forall n \in \N: d_n - d_{n + 1} \ge 0$
Thus $\sequence {d_n}$ is a decreasing sequence.
{{qed}}
Theorem: Power Series Expansion for Real Arctangent Function

The arctangent function has a Taylor series expansion:
:<nowiki>$\arctan x = \begin {cases} \ds \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {2 n + 1} & : -1 \le x \le 1 \\ \\
\ds \frac \pi 2 - \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac 1 {\paren {2 n + 1} x^{2 n + 1} } & : x \ge 1 \\ \\
\ds -\frac \pi 2 - \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac 1 {\paren {2 n + 1} x^{2 n + 1} } & : x \le -1
\end {cases}$</nowiki>
That is:
:<nowiki>$\arctan x = \begin {cases} x - \dfrac {x^3} 3 + \dfrac {x^5} 5 - \dfrac {x^7} 7 + \dfrac {x^9} 9 - \cdots & : -1 \le x \le 1 \\ \\
\dfrac \pi 2 - \dfrac 1 x + \dfrac 1 {3 x^3} - \dfrac 1 {5 x^5} + \cdots & : x \ge 1 \\ \\
-\dfrac \pi 2 - \dfrac 1 x + \dfrac 1 {3 x^3} - \dfrac 1 {5 x^5} + \cdots & : x \le -1
\end {cases}$</nowiki>

Proof:
From Sum of Infinite Geometric Sequence:
:$(1): \quad \ds \sum_{n \mathop = 0}^\infty \paren {-x^2}^n = \frac 1 {1 + x^2}$
for $-1 < x < 1$.
From Power Series is Termwise Integrable within Radius of Convergence, $(1)$ can be integrated term by term:
{{begin-eqn}}
{{eqn | l = \int_0^x \frac 1 {1 + t^2} \rd t
      | r = \sum_{n \mathop = 0}^\infty \int_0^x \paren {-t^2}^n \rd t
      | c = 
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \arctan x 
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {2 n + 1}
      | c = Primitive of Reciprocal of $\dfrac 1 {1 + t^2}$, Integral of Power
}}
{{end-eqn}}
For $-1 \le x \le 1$, the sequence $\sequence {\dfrac {x^{2 n + 1}} {2 n + 1} }$ is decreasing and converges to zero.
Therefore the series converges in the given range by the Alternating Series Test.
{{qed|lemma}}
Now consider the case $x \ge 1$:
{{begin-eqn}}
{{eqn | l = \arctan x 
      | r = \frac \pi 2 - \map \arccot x
      | c = Sum of Arctangent and Arccotangent
}}
{{eqn | r = \frac \pi 2 - \map \arctan {\frac 1 x}
      | c = Arctangent of Reciprocal equals Arccotangent
}}
{{eqn | r = \frac \pi 2 - \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac 1 {2 n + 1} \paren {\frac 1 x}^{2 n + 1}
      | c = as $x \ge 1$, $0 < \dfrac 1 x \le 1$, so $(2)$ may be applied
}}
{{eqn | n = 3
      | r = \frac \pi 2 - \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac 1 {\paren {2 n + 1} x^{2 n + 1} }
}}
{{end-eqn}}
{{qed|lemma}}
We also have: 
{{begin-eqn}}
{{eqn | l = \map \arctan {-x}
      | r = -\arctan x
      | c = Arctangent Function is Odd
}}
{{eqn | r = -\frac \pi 2 - \sum_{n \mathop = 0}^\infty \paren {-1}^{n + 1} \frac 1 {\paren {2 n + 1} x^{2 n + 1} }
      | c = from $(3)$
}}
{{end-eqn}}
Substituting $x$ for $-x$ gives us the expansion for $x \le -1$: 
{{begin-eqn}}
{{eqn | l = \arctan x
      | r = -\frac \pi 2 - \sum_{n \mathop = 0}^\infty \paren {-1}^{n + 1} \frac 1 {\paren {2 n + 1} \paren {-x}^{2 n + 1} }
}}
{{eqn | r = -\frac \pi 2 - \sum_{n \mathop = 0}^\infty \paren {-1}^{n + 1} \frac 1 {-\paren {2 n + 1} x^{2 n + 1} }
}}
{{eqn | r = -\frac \pi 2 - \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac 1 {\paren {2 n + 1} x^{2 n + 1} }
}}
{{end-eqn}}
{{qed}}
Theorem: Ordering in terms of Addition

Let $\struct {S, \circ, \preceq}$ be a naturally ordered semigroup.
Then $\forall m, n \in S$: 
:$m \preceq n \iff \exists p \in S: m \circ p = n$

Proof:
=== Necessary Condition ===
From {{NOSAxiom|3}}, we have:
:$\forall m, n \in S: m \preceq n \implies \exists p \in S: m \circ p = n$
{{qed|lemma}}
Theorem: Difference in Naturally Ordered Semigroup is Unique

Let $\struct {S, \circ, \preceq}$ be a naturally ordered semigroup.
Let $n, m \in S$ such that $m \preceq n$.
Then there exists a unique difference $n - m$ of $m$ and $n$.

Proof:
Since $m \preceq n$, by {{NOSAxiom|3}}:
:$\exists p \in S: m \circ p = n$
Now suppose that $p, q \in S$ are such that:
:$m \circ p = m \circ q = n$
Then it follows from {{NOSAxiom|2}} that:
:$p = q$
Hence the result.
{{qed}}
Theorem: Equivalence of Definitions of Beta Function

{{TFAE|def = Beta Function}}
For $\map \Re x, \map \Re y > 0$:

Proof:
=== Definition 1 is equivalent to Definition 2 ===
{{begin-eqn}}
{{eqn | l = \map \Beta {x, y}
      | r = \int_0^1 t^{x - 1} \paren {1 - t}^{y - 1} \rd t
      | c = {{Defof|Beta Function|index = 1}}
}}
{{eqn | r = \int_0^{\pi / 2} \paren {\sin \theta}^{2 x - 2} \paren {\cos \theta}^{2 y - 2} 2 \sin \theta \cos \theta \rd \theta
      | c = Substitute $t = \sin^2 \theta$
}}
{{eqn | r = 2 \int_0^{\pi / 2} \paren {\sin \theta}^{2 x - 1} \paren {\cos \theta}^{2 y - 1} \rd \theta
      | c = {{Defof|Beta Function|index = 2}}
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Ordering of Naturally Ordered Semigroup is Strongly Compatible

:$\forall m, n, p \in S: m \preceq n \iff m \circ p \preceq n \circ p$

Proof:
The forward implication is immediate from $\preceq$ being compatible with $\circ$:
:$\forall m, n, p \in S: m \preceq n \implies m \circ p \preceq n \circ p$
Conversely, suppose that $m \circ p \preceq n \circ p$.
Suppose that $n \prec m$.
Then as $\preceq$ is compatible with $\circ$:
:$n \circ p \preceq m \circ p$
Since $\preceq$ is an ordering, this implies:
:$n \circ p = m \circ p$
By {{NOSAxiom|2}}, it follows that:
:$n = m$
contradicting our assumption that $n \prec m$.
Hence, since $\preceq$ is a total ordering:
:$m \preceq n$
as desired.
{{qed}}
Theorem: Strict Ordering of Naturally Ordered Semigroup is Strongly Compatible

:$\forall m, n, p \in S: m \prec n \iff m \circ p \prec n \circ p$

Proof:
By {{NOSAxiom|2}}, all $n \in S$ are cancellable.
Hence from Strict Ordering Preserved under Product with Cancellable Element:
:$\forall m, n, p \in S: m \prec n \implies m \circ p \prec n \circ p$
By {{NOSAxiom|1}}, $\preceq$ is a total ordering.
Therefore, the contrapositive of:
:$\forall m, n, p \in S: m \circ p \prec n \circ p \implies m \prec n$
is:
:$\forall m, n, p \in S: m \preceq n \implies m \circ p \preceq n \circ p$
which we know to be true by virtue of {{NOSAxiom|2}}.
The result follows.
{{qed}}
Theorem: Sum with One is Immediate Successor in Naturally Ordered Semigroup

Let $\struct {S, \circ, \preceq}$ be a naturally ordered semigroup.
Let $1$ be the one of $S$.
Let $n \in S$.
Then $n \circ 1$ is the immediate successor of $n$.
That is, for all $m \in S$:
:$n \prec m \iff n \circ 1 \preceq m$

Proof:
By Zero Strictly Precedes One, $0 \prec 1$, where $0$ is the zero of $S$.
Hence from Strict Ordering of Naturally Ordered Semigroup is Strongly Compatible:
:$n \circ 0 \prec n \circ 1$
and by Zero is Identity in Naturally Ordered Semigroup, $n \circ 0 = n$.
Now suppose that $n \prec m$.
Then by {{NOSAxiom|3}}, there exists $p \in S$ such that:
:$n \circ p = m$
Moreover, since $n \ne m$, it follows that $p \ne 0$.
Hence $0 \prec p$ by definition of zero.
Therefore, by definition of one:
:$1 \preceq p$
Now by compatibility of $\preceq$ with $\circ$:
:$n \circ 1 \preceq n \circ p = m$
as desired.
Conversely, if $n \circ 1 \preceq m$, it is immediate from:
:$n \prec n \circ 1$
that $n \prec m$.
{{qed}}
Theorem: Riemann Zeta Function at Even Integers

The Riemann $\zeta$ function can be calculated for even integers as follows:
{{begin-eqn}}
{{eqn | l = \map \zeta {2 n}
      | r = \paren {-1}^{n + 1} \dfrac {B_{2 n} 2^{2 n - 1} \pi^{2 n} } {\paren {2 n}!}
      | c = 
}}
{{eqn | r = \frac 1 {1^{2 n} } + \frac 1 {2^{2 n} } + \frac 1 {3^{2 n} } + \frac 1 {4^{2 n} } + \cdots
      | c = 
}}
{{end-eqn}}
where:
:$B_n$ are the Bernoulli numbers
:$n$ is a positive integer.

Proof:
{{begin-eqn}}
{{eqn | l = \frac {\sin \pi x} {\pi x}
      | r = \prod_{k \mathop = 1}^\infty \paren {1 - \frac {x^2} {k^2} }
      | c = Euler Formula for Sine Function
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\frac {\sin \pi x} {\pi x} }
      | r = \ln \prod_{k \mathop = 1}^\infty \paren {1 - \frac {x^2} {k^2} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\sin {\pi x} }
      | r = \map \ln {\pi x} + \sum_{k \mathop = 1}^\infty \map \ln {1 - \frac {x^2} {k^2} }
      | c = Laws of Logarithms
}}
{{eqn | ll= \leadsto
      | l = \pi \frac {\cos {\pi x} } {\sin {\pi x} }
      | r = \frac 1 x + \sum_{k \mathop = 1}^\infty \frac 1 {\paren {1 - \frac {x^2} {k^2} } } \paren {-\frac {2 x} {k^2} }
      | c = differentiating {{WRT|Differentiation}} $x$
}}
{{eqn | ll= \leadsto
      | l = \pi x \cot {\pi x}
      | r = 1 + \sum_{k \mathop = 1}^\infty \frac 1 {\paren {1 - \frac {x^2} {k^2} } } \paren {-\frac {2 x^2} {k^2} }
      | c = 
}}
{{eqn | r = 1 + \sum_{k \mathop = 1}^\infty \sum_{n \mathop = 0}^\infty \paren {\frac {x^2} {k^2} }^n \paren {-\frac {2 x^2} {k^2} }
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | r = 1 - 2 \sum_{k \mathop = 1}^\infty \sum_{n \mathop = 1}^\infty \paren {\frac {x^2} {k^2} }^n
      | c = 
}}
{{eqn | r = 1 - 2  \sum_{n \mathop = 1}^\infty \paren {\sum_{k \mathop = 1}^\infty \frac 1 {k^{2 n} } } x^{2 n}
      | c = interchanging order of summation is valid by Tonelli's Theorem
}}
{{eqn | r = 1 - 2 \sum_{n \mathop = 1}^\infty \map \zeta {2 n} x^{2 n}
      | c =
}}
{{end-eqn}}
{{qed}}
Theorem: Riemann Zeta Function at Even Integers

The Riemann $\zeta$ function can be calculated for even integers as follows:
{{begin-eqn}}
{{eqn | l = \map \zeta {2 n}
      | r = \paren {-1}^{n + 1} \dfrac {B_{2 n} 2^{2 n - 1} \pi^{2 n} } {\paren {2 n}!}
      | c = 
}}
{{eqn | r = \frac 1 {1^{2 n} } + \frac 1 {2^{2 n} } + \frac 1 {3^{2 n} } + \frac 1 {4^{2 n} } + \cdots
      | c = 
}}
{{end-eqn}}
where:
:$B_n$ are the Bernoulli numbers
:$n$ is a positive integer.

Proof:
From Laurent Series Expansion for Cotangent Function:
:$\ds \pi \cot \pi z = \frac 1 z - 2 \sum_{n \mathop = 1}^\infty \map \zeta {2 n} z^{2 n - 1}$
where:
:$z \in \C$ such that $\cmod z < 1$
:$\zeta$ is the Riemann Zeta function.
Letting $x \in \R$ replace $z$, and multiplying through by $x$:
{{begin-eqn}}
{{eqn | l = \pi x \cot \pi x
      | r = x \paren {\frac 1 x - 2 \sum_{n \mathop = 1}^\infty \map \zeta {2 n} x^{2 n - 1} }
}}
{{eqn | r = 1 - 2 x \sum_{n \mathop = 1}^\infty \map \zeta {2 n} x^{2 n - 1}
}}
{{eqn | r = 1 - 2 \sum_{n \mathop = 1}^\infty \map \zeta {2 n} x^{2 n} 
}}
{{end-eqn}}
{{qed}}
Theorem: Riemann Zeta Function at Even Integers

The Riemann $\zeta$ function can be calculated for even integers as follows:
{{begin-eqn}}
{{eqn | l = \map \zeta {2 n}
      | r = \paren {-1}^{n + 1} \dfrac {B_{2 n} 2^{2 n - 1} \pi^{2 n} } {\paren {2 n}!}
      | c = 
}}
{{eqn | r = \frac 1 {1^{2 n} } + \frac 1 {2^{2 n} } + \frac 1 {3^{2 n} } + \frac 1 {4^{2 n} } + \cdots
      | c = 
}}
{{end-eqn}}
where:
:$B_n$ are the Bernoulli numbers
:$n$ is a positive integer.

Proof:
=== Lemma ===
{{:Riemann Zeta Function at Even Integers/Lemma}}
We also have:
{{begin-eqn}}
{{eqn | l = \pi x \cot {\pi x}
      | r = i \pi x \frac {e^{i \pi x} + e^{- i \pi x} } {e^{i \pi x} - e^{- i \pi x} }
      | c = Euler's Cotangent Identity
}}
{{eqn | r = i \pi x \frac {e^{2 i \pi x} + 1} {e^{2 i \pi x} - 1}
      | c = 
}}
{{eqn | r = i \pi x \paren {1 + \frac 2 {e^{2 i \pi x} - 1} }
      | c = 
}}
{{eqn | r = i \pi x  + \frac {2 i \pi x} {e^{2 i \pi x} - 1}
      | c = 
}}
{{eqn | r = i \pi x + \sum_{n \mathop = 0}^\infty \frac {B_n \paren {2 i \pi x}^n} {n!}
      | c = {{Defof|Bernoulli Numbers}}
}}
{{eqn | r = 1 + \sum_{n \mathop = 2}^\infty \frac {B_n \paren {2 i \pi x}^n} {n!}
      | c = as $B_0 = 1$ and $B_1 = - \dfrac 1 2$
}}
{{eqn | r = 1 - 2 \sum_{n \mathop = 2}^\infty \paren {-\frac 1 2} \frac {B_n \paren {2 i \pi x}^n} {n!}
      | c = 
}}
{{eqn | n = 1
      | r = 1 - 2 \sum_{n \mathop = 1}^\infty \paren {-\frac 1 2} \frac {B_{2 n} \paren {2 i \pi x}^{2 n} } {\paren {2 n}!}
      | c = Odd Bernoulli Numbers Vanish
}}
{{end-eqn}}
Equating the coefficients of $(1)$ with the expression given in the {{Lemma|Riemann Zeta Function at Even Integers}}:
:$\map \zeta {2 n} = \paren {-1}^{n + 1} \dfrac {B_{2 n} 2^{2 n - 1} \pi^{2 n} } {\paren {2 n}!}$
{{qed}}
Theorem: Tangent Inequality

:$x < \tan x$
for all $x$ in the interval $\openint 0 {\dfrac \pi 2}$.

Proof:
Let $\map f x = \tan x - x$.
By Derivative of Tangent Function, $\map {f'} x = \sec^2 x - 1$.
By Shape of Secant Function, $\sec^2 x > 1$ for $x \in \openint 0 {\dfrac \pi 2}$.
Hence $\map {f'} x > 0$.
From Derivative of Monotone Function, $\map f x$ is strictly increasing in this interval.
Since $\map f 0 = 0$, it follows that $\map f x > 0$ for all $x \in \openint 0 {\dfrac \pi 2}$.
{{qed}}
Category:Tangent Function
Category:Inequalities
o5e3yh1xmu1ns1gx4co1vzbf70d11l0
Theorem: Integral Representation of Riemann Zeta Function in terms of Gamma Function

For $\Re \paren s > 1$, the Riemann Zeta function is given by:
:$\ds \map \zeta s = \frac 1 {\map \Gamma s} \int_0^\infty \frac {t^{s - 1}} {e^t - 1} \rd t$
where $\Gamma$ is the Gamma function.

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^\infty \frac {t^{s - 1} } {e^t - 1} \rd t
      | r = \int_0^\infty \frac {t^{s - 1} } {e^t - 1} \times \dfrac {e^{-t} } {e^{-t} }\rd t
      | c = multiplying by 1
}}
{{eqn | r = \int_0^\infty \frac {t^{s - 1} e^{-t} } {1 - e^{-t} } \rd t
      | c = 
}}
{{eqn | r = \int_0^\infty t^{s - 1} e^{-t} \sum_{n \mathop = 0}^\infty e^{-n t} \rd t
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | r = \int_0^\infty t^{s - 1} \sum_{n \mathop = 0}^\infty e^{-\paren {n + 1} t} \rd t
      | c = Product of Powers
}}
{{eqn | r = \int_0^\infty t^{s - 1} \sum_{n \mathop = 1}^\infty e^{-n t} \rd t
      | c = reindexing the sum
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \int_0^\infty t^{s - 1} e^{-n t} \rd t
      | c = interchange of sum and integral is valid by Fubini's Theorem
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \int_0^\infty \paren {\dfrac u n}^{s - 1} e^{-u} \dfrac 1 n \rd u
      | c = substituting $n t \to u$; $t \to \dfrac u n$ and $\rd t \to \dfrac 1 n \rd u$
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \frac 1 {n^s} \int_0^\infty u^{s - 1} e^{-u} \rd u
      | c = 
}}
{{eqn | r = \map \zeta s \map \Gamma s
      | c = {{Defof|Riemann Zeta Function}} and {{Defof|Integral Form of Gamma Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Power Series Expansion for Real Arcsine Function

The (real) arcsine function has a Taylor series expansion:
{{begin-eqn}}
{{eqn | l = \arcsin x
      | r = \sum_{n \mathop = 0}^\infty \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2} \frac {x^{2 n + 1} } {2 n + 1}
      | c = 
}}
{{eqn | r = x + \frac {x^3} {2 \times 3} + \frac {\paren {1 \times 3} x^5} {2 \times 4 \times 5} + \frac {\paren {1 \times 3 \times 5} x^7} {2 \times 4 \times 6 \times 7} + \cdots
      | c = 
}}
{{end-eqn}}
which converges for $-1 \le x \le 1$.

Proof:
From the General Binomial Theorem:
{{begin-eqn}}
{{eqn | l = \paren {1 - x^2}^{-1/2} 
      | r = 1 + \frac 1 2 x^2 + \frac {1 \times 3} {2 \times 4} x^4 + \frac {1 \times 3 \times 5} {2 \times 4 \times 6} x^6 + \cdots
      | c =
}}      
{{eqn | n = 1
      | r = \sum_{n \mathop = 0}^\infty \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2} x^{2 n}
      | c = 
}}
{{end-eqn}}
for $-1 < x < 1$.
From Power Series is Termwise Integrable within Radius of Convergence, $(1)$ can be integrated term by term:
{{begin-eqn}}
{{eqn | l = \int_0^x \frac 1 {\sqrt{1 - t^2} } \rd t
      | r = \sum_{n \mathop = 0}^\infty \int_0^x \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2} t^{2 n} \rd t
      | c =
}}
{{eqn | ll= \leadsto
      | l = \arcsin x
      | r = \sum_{n \mathop = 0}^\infty \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2} \frac {x^{2 n + 1} } {2 n + 1}
      | c = Derivative of Arcsine Function
}}
{{end-eqn}}
We will now prove that the series converges for $-1 \le x \le 1$.
By Stirling's Formula:
{{begin-eqn}}
{{eqn | l = \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2} \frac {x^{2 n + 1} } {2 n + 1} 
      | o = \sim
      | r = \frac {\paren {2 n}^{2 n} e^{-2 n} \sqrt {4 \pi n} } {2^{2 n} n^{2 n} e^{-2 n} 2 \pi n} \frac {x^{2 n + 1} } {2 n + 1}
      | c =
}}
{{eqn | r = \frac 1 {\sqrt {\pi n} } \frac {x^{2 n + 1} } {2 n + 1}
      | c =
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \size {\frac 1 {\sqrt {\pi n} } \frac {x^{2 n + 1} } {2 n + 1} }
      | o = <
      | r = \size {\frac {x^{2 n + 1} } {n^{3/2} } }
      | c = 
}}
{{eqn | o = \le
      | r = \frac 1 {n^{3/2} }
      | c = 
}}
{{end-eqn}}
Hence by Convergence of P-Series:
:$\ds \sum_{n \mathop = 1}^\infty \frac 1 {n^{3/2} }$
is convergent.
So by the Comparison Test, the Taylor series is convergent for $-1 \le x \le 1$.
{{qed}}
Theorem: Power Series Expansion for Real Arccosine Function

The arccosine function has a Taylor Series expansion:
{{begin-eqn}}
{{eqn | l = \arccos x
      | r = \frac \pi 2 - \sum_{n \mathop = 0}^\infty \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2} \frac {x^{2 n + 1} } {2 n + 1}
      | c = 
}}
{{eqn | r = \frac \pi 2 - \paren {x + \frac {x^3} {2 \times 3} + \frac {\paren {1 \times 3} x^5} {2 \times 4 \times 5} + \frac {\paren {1 \times 3 \times 5} x^7} {2 \times 4 \times 6 \times 7} + \cdots}
      | c = 
}}
{{end-eqn}}
which converges for $-1 \le x \le 1$.

Proof:
{{begin-eqn}}
{{eqn | l = \arccos x 
      | r = \frac {\pi} 2 - \arcsin x
      | c = Sum of Arcsine and Arccosine
}}
{{eqn | r = \frac {\pi} 2 - \sum_{n \mathop = 0}^\infty \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2} \frac {x^{2 n + 1} } {2 n + 1}
      | c = Power Series Expansion for Real Arcsine Function
}}
{{end-eqn}}
It follows from Power Series Expansion for Real Arcsine Function that the series is convergent for $-1 \le x \le 1$.
{{qed}}
Theorem: Real Function is Concave iff its Negative is Convex

Let $f$ be a real function.
Let $I \subseteq \R$ be an interval of $\R$.
Then $f$ is concave on $I$ {{iff}} $-f$ is convex on $\R$.

Proof:
=== Necessary Condition ===
Let $f$ be concave on $I$.
Let $\alpha, \beta \in \R_{>0}$ such that $\alpha + \beta = 1$.
Then:
{{begin-eqn}}
{{eqn | l = \map f {\alpha x + \beta y}
      | o = \ge
      | r = \alpha \map f x + \beta \map f y
      | c = {{Defof|Concave Real Function}}
}}
{{eqn | ll= \leadsto
      | l = -\map f {\alpha x + \beta y}
      | o = \le
      | r = -\paren {\alpha \map f x + \beta \map f y}
      | c = 
}}
{{eqn | r = \alpha \paren {-\map f x} + \beta \paren {-\map f y}
      | c = 
}}
{{end-eqn}}
and so $-f$ is convex by definition.
{{qed|lemma}}
Theorem: Concave Real Function is Left-Hand and Right-Hand Differentiable

Let $f$ be a real function which is concave on the open interval $\openint a b$.
Then the left-hand derivative $\map {f'_-} x$ and right-hand derivative $\map {f'_+} x$ both exist for all $x \in \openint a b$.

Proof:
Let $f$ be concave on $\openint a b$.
Then by definition of concavity:
:$\forall x_1, x_2, x_3 \in \openint a b: x_1 < x_2 < x_3: \dfrac {\map f {x_2} - \map f {x_1} } {x_2 - x_1} \ge \dfrac {\map f {x_3} - \map f {x_1} } {x_3 - x_1}$
Let $0 < h_1 < h_2$.
Substitute $x_1 = x$, $x_2 = x + h_1$, $x_3 = x + h_2$. Then:
:$\dfrac {\map f {x + h_1} - \map f x} {h_1} \ge \dfrac {\map f {x + h_2} - \map f x} {h_2}$
Hence the function $\map F h = \dfrac {\map f {x + h} - \map f x} h$ decreases in some $\closedint 0 \delta$.
Thus from Limit of Decreasing Function it follows that both $\ds \lim_{h \mathop \to 0^+} \map F h = \map {f'_+} x$ and $\ds \lim_{h \mathop \to 0^-} \map F h = \map {f'_-} x$ exist.
{{qed}}
Theorem: Concave Real Function is Continuous

Let $f$ be a real function which is concave on the open interval $\openint a b$.
Then $f$ is continuous on $\openint a b$.

Proof:
From Concave Real Function is Left-Hand and Right-Hand Differentiable, $f$ is left-hand and right-hand differentiable on $\openint a b$.
From Left-Hand and Right-Hand Differentiable Function is Continuous, $f$ is continuous on $\openint a b$.
{{qed}}