avewright/proofwiki-math huggingface dataset:
Theorem: Absolute Value Function is Convex

Let $f: \R \to \R$ be the absolute value function on the real numbers.
Then $f$ is convex.

Proof:
Let $x, y \in \R$.
Let $\alpha, \beta \in \R_{\ge 0}$ where $\alpha + \beta = 1$.
{{begin-eqn}}
{{eqn | l = \map f {\alpha x + \beta y}
      | r = \size {\alpha x + \beta y}
      | c = Definition of $f$
}}
{{eqn | o = \le
      | r = \size {\alpha x} + \size {\beta y}
      | c = Triangle Inequality for Real Numbers
}}
{{eqn | r = \size \alpha \size x + \size \beta \size y
      | c = Absolute Value Function is Completely Multiplicative
}}
{{eqn | r = \alpha \size x + \beta \size y
      | c = {{Defof|Absolute Value}}
}}
{{eqn | r = \alpha \, \map f x + \beta \, \map f y
      | c = Definition of $f$
}}
{{end-eqn}}
Hence the result by definition of convex real function.
{{qed}}
Theorem: Real Function is Concave iff Derivative is Decreasing

Let $f$ be a real function which is differentiable on the open interval $\openint a b$.
Then $f$ is concave on $\openint a b$ {{iff}} its derivative $f'$ is decreasing on $\openint a b$.
Thus the intuitive result that a concave function "gets less steep".

Proof:
=== Necessary Condition ===
Let $f$ be concave on $\openint a b$.
Let $x_1, x_2, x_3, x_4 \in \openint a b$ such that:
:$x_1 < x_2 < x_3 < x_4$
By the definition of concave:
:$\dfrac {\map f {x_2} - \map f {x_1} } {x_2 - x_1} \ge \dfrac {\map f {x_3} - \map f {x_2} } {x_3 - x_2} \ge \dfrac {\map f {x_4} - \map f {x_3} } {x_4 - x_3}$
Ignore the middle term and let $x_2 \to x_1^+$ and $x_3 \to x_4^-$.
Thus:
:$\map {f'} {x_1} \ge \map {f'} {x_4}$
Hence $f'$ is decreasing on $\openint a b$.
{{qed|lemma}}
Theorem: Real Function is Strictly Convex iff Derivative is Strictly Increasing

Let $f$ be a real function which is differentiable on the open interval $\openint a b$.
Then $f$ is strictly convex on $\openint a b$ {{iff}} its derivative $f'$ is strictly increasing on $\openint a b$.

Proof:
=== Necessary Condition ===
Let $f$ be strictly convex on $\openint a b$.
Let $r, s \in \openint a b$ be arbitrarily selected such that $r < s$.
We are to show that:
:$\map {f'} r < \map {f'} s$
Let $x_1, x_2, x_3 \in \openint a b$ be chosen such that:
:$r < x_1 < x_2 < x_3 < s$
By the definition of strictly convex:
:$(1): \quad \dfrac {\map f {x_1} - \map f r} {x_1 - r} < \dfrac {\map f {x_2} - \map f {x_1} } {x_2 - x_1} < \dfrac {\map f {x_3} - \map f {x_2} } {x_3 - x_2} < \dfrac {\map f s - \map f {x_3} } {s - x_3}$
and:
:$(2): \quad \dfrac {\map f {x_2} - \map f r} {x_2 - r} < \dfrac {\map f s - \map f {x_2} } {s - x_2}$
Let $x_1 \to r^+$.
Then:
{{begin-eqn}}
{{eqn | l = \dfrac {\map f {x_1} - \map f r} {x_1 - r}
      | o = <
      | r = \dfrac {\map f {x_2} - \map f {x_1} } {x_2 - x_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \lim_{x_1 \mathop \to r^+} \dfrac {\map f {x_1} - \map f r} {x_1 - r}
      | o = \le
      | r = \lim_{x_1 \mathop \to r^+} \dfrac {\map f {x_2} - \map f {x_1} } {x_2 - x_1}
      | c = Limits Preserve Inequalities
}}
{{eqn | n = 3
      | ll= \leadsto
      | l = \map {f'} r
      | o = \le
      | r = \dfrac {\map f {x_2} - \map f r} {x_2 - r}
      | c = {{Defof|Derivative of Real Function at Point}}
}}
{{end-eqn}}
Similarly, let $x_3 \to s^-$.
We have:
{{begin-eqn}}
{{eqn | l = \dfrac {\map f {x_3} - \map f {x_2} } {x_3 - x_2}
      | o = <
      | r = \dfrac {\map f s - \map f {x_3} } {s - x_3}
      | c = from $(1)$
}}
{{eqn | ll= \leadsto
      | l = \lim_{x_3 \mathop \to s^-} \dfrac {\map f {x_3} - \map f {x_2} } {x_3 - x_2}
      | o = \le
      | r = \lim_{x_3 \mathop \to s^-} \dfrac {\map f s - \map f {x_3} } {s - x_3}
      | c = Limits Preserve Inequalities
}}
{{eqn | n = 4
      | ll= \leadsto
      | l = \dfrac {\map f s - \map f {x_2} } {s - x_2}
      | o = \le
      | r = \map {f'} s
      | c = {{Defof|Derivative of Real Function at Point}}
}}
{{end-eqn}}
Thus we have:
{{begin-eqn}}
{{eqn | l = \map {f'} r
      | o = \le
      | r = \dfrac {\map f {x_2} - \map f r} {x_2 - r}
      | c = from $(3)$
}}
{{eqn | o = <
      | r = \dfrac {\map f s - \map f {x_2} } {s - x_2}
      | c = from $(2)$
}}
{{eqn | o = \le
      | r = \map {f'} s
      | c = from $(4)$
}}
{{end-eqn}}
Thus:
:$\map {f'} r < \map {f'} s$
Hence $f'$ is strictly decreasing on $\openint a b$.
{{Proofread}}
{{qed|lemma}}
Theorem: Real Function is Strictly Concave iff Derivative is Strictly Decreasing

Let $f$ be a real function which is differentiable on the open interval $\openint a b$.
Then $f$ is strictly concave on $\openint a b$ {{iff}} its derivative $f'$ is strictly decreasing on $\openint a b$.

Proof:
=== Necessary Condition ===
Let $f$ be strictly concave on $\openint a b$.
Let $r, s \in \openint a b$ be arbitrarily selected such that $r < s$.
We are to show that:
:$\map {f'} r > \map {f'} s$
Let $x_1, x_2, x_3 \in \openint a b$ be chosen such that:
:$r < x_1 < x_2 < x_3 < s$
By the definition of strictly concave:
:$(1): \quad \dfrac {\map f {x_1} - \map f r} {x_1 - r} > \dfrac {\map f {x_2} - \map f {x_1} } {x_2 - x_1} > \dfrac {\map f {x_3} - \map f {x_2} } {x_3 - x_2} > \dfrac {\map f s - \map f {x_3} } {s - x_3}$
and:
:$(2): \quad \dfrac {\map f {x_2} - \map f r} {x_2 - r} > \dfrac {\map f s - \map f {x_2} } {s - x_2}$
Let $x_1 \to r^+$.
Then:
{{begin-eqn}}
{{eqn | l = \dfrac {\map f {x_1} - \map f r} {x_1 - r}
      | o = >
      | r = \dfrac {\map f {x_2} - \map f {x_1} } {x_2 - x_1}
      | c = from $(1)$
}}
{{eqn | ll= \leadsto
      | l = \lim_{x_1 \mathop \to r^+} \dfrac {\map f {x_1} - \map f r} {x_1 - r}
      | o = \ge
      | r = \lim_{x_1 \mathop \to r^+} \dfrac {\map f {x_2} - \map f {x_1} } {x_2 - x_1}
      | c = Limits Preserve Inequalities
}}
{{eqn | n = 3
      | ll= \leadsto
      | l = \map {f'} r
      | o = \ge
      | r = \dfrac {\map f {x_2} - \map f r} {x_2 - r}
      | c = {{Defof|Derivative of Real Function at Point}}
}}
{{end-eqn}}
Similarly, let $x_3 \to s^-$.
We have:
{{begin-eqn}}
{{eqn | l = \dfrac {\map f {x_3} - \map f {x_2} } {x_3 - x_2}
      | o = >
      | r = \dfrac {\map f s - \map f {x_3} } {s - x_3}
      | c = from $(1)$
}}
{{eqn | ll= \leadsto
      | l = \lim_{x_3 \mathop \to s^-} \dfrac {\map f {x_3} - \map f {x_2} } {x_3 - x_2}
      | o = \ge
      | r = \lim_{x_3 \mathop \to s^-} \dfrac {\map f s - \map f {x_3} } {s - x_3}
      | c = Limits Preserve Inequalities
}}
{{eqn | n = 4
      | ll= \leadsto
      | l = \dfrac {\map f s - \map f {x_2} } {s - x_2}
      | o = \ge
      | r = \map {f'} s
      | c = {{Defof|Derivative of Real Function at Point}}
}}
{{end-eqn}}
Thus we have:
{{begin-eqn}}
{{eqn | l = \map {f'} r
      | o = \ge
      | r = \dfrac {\map f {x_2} - \map f r} {x_2 - r}
      | c = from $(3)$
}}
{{eqn | o = >
      | r = \dfrac {\map f s - \map f {x_2} } {s - x_2}
      | c = from $(2)$
}}
{{eqn | o = \ge
      | r = \map {f'} s
      | c = from $(4)$
}}
{{end-eqn}}
Thus:
:$\map {f'} r > \map {f'} s$
Hence $f'$ is strictly decreasing on $\openint a b$.
{{Proofread}}
{{qed|lemma}}
Theorem: Inverse of Strictly Decreasing Convex Real Function is Convex

Let $f$ be a real function which is convex on the open interval $I$.
Let $J = f \left[{I}\right]$.
If $f$ be strictly decreasing on $I$, then $f^{-1}$ is convex on $J$.

Proof:
Let:
:$X = f \left({x}\right) \in J$
:$Y = f \left({y}\right) \in J$.
From the definition of convex:
: $\forall \alpha, \beta \in \R_{>0}, \alpha + \beta = 1: f \left({\alpha x + \beta y}\right) \le \alpha f \left({x}\right) + \beta f \left({y}\right)$
Let $f$ be strictly decreasing on $I$.
Then from Inverse of Strictly Monotone Function it follows that $f^{-1}$ is strictly decreasing on $J$.
Thus:
: $\alpha f^{-1} \left({X}\right) + \beta f^{-1} \left({Y}\right) = \alpha x + \beta y \le f^{-1} \left({\alpha X + \beta Y}\right)$
Hence $f^{-1}$ is convex on $J$.
{{qed}}
Theorem: Inverse of Strictly Increasing Concave Real Function is Convex

Let $f$ be a real function which is concave on the open interval $I$.
Let $J = f \sqbrk I$.
If $f$ is strictly increasing on $I$, then $f^{-1}$ is convex on $J$.

Proof:
Let $X = \map f x \in J, Y = \map f y \in J$.
From the definition of concave:
:$\forall \alpha, \beta \in \R_{>0}, \alpha + \beta = 1: \map f {\alpha x + \beta y} \ge \alpha \map f x + \beta \map f y$
Let $f$ be strictly increasing on $I$.
From Inverse of Strictly Monotone Function, it follows that $f^{-1}$ is strictly increasing on $J$.
Thus:
:$\alpha \map {f^{-1} } X + \beta \map {f^{-1} } Y = \alpha x + \beta y \ge \map {f^{-1} } {\alpha X + \beta Y}$
Hence $f^{-1}$ is convex on $J$.
{{qed}}
Theorem: Inverse of Strictly Decreasing Concave Real Function is Concave

Let $f$ be a real function which is concave on the open interval $I$.
Let $J = f \left[{I}\right]$.
If $f$ be strictly decreasing on $I$, then $f^{-1}$ is concave on $J$.

Proof:
Let:
:$X = f \left({x}\right) \in J$
:$Y = f \left({y}\right) \in J$.
From the definition of concave:
: $\forall \alpha, \beta \in \R_{>0}, \alpha + \beta = 1: f \left({\alpha x + \beta y}\right) \ge \alpha f \left({x}\right) + \beta f \left({y}\right)$
Let $f$ be strictly decreasing on $I$.
From Inverse of Strictly Monotone Function, it follows that $f^{-1}$ is strictly decreasing on $J$.
Thus:
: $\alpha f^{-1} \left({X}\right) + \beta f^{-1} \left({Y}\right) = \alpha x + \beta y \ge f^{-1} \left({\alpha X + \beta Y}\right)$
Hence $f^{-1}$ is concave on $J$.
{{qed}}
Theorem: Mean Value of Concave Real Function

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$ and differentiable on the open interval $\openint a b$.
Let $f$ be concave on $\openint a b$.
Then:
:$\forall \xi \in \openint a b: \map f x - \map f \xi \le \map {f'} \xi \paren {x - \xi}$

Proof:
By the Mean Value Theorem:
:$\exists \eta \in \openint x \xi: \map {f'} \eta = \dfrac {\map f x - \map f \xi} {x - \xi}$
From Real Function is Concave iff Derivative is Decreasing, the derivative of $f$ is decreasing.
Thus:
:$x > \xi \implies \map {f'} \eta \le \map {f'} \xi$
:$x < \xi \implies \map {f'} \eta \ge \map {f'} \xi$
Hence:
:$\map f x - \map f \xi \le \map {f'} \xi \paren {x - \xi}$
{{qed}}
Theorem: Differentiable Bounded Concave Real Function is Constant

Let $f$ be a real function which is:
:$(1): \quad$ differentiable on $\R$
:$(2): \quad$ bounded on $\R$
:$(3): \quad$ concave on $\R$.
Then $f$ is constant.

Proof:
Let $f$ be differentiable and bounded on $\R$.
Let $f$ be concave on $\R$.
Let $\xi \in \R$.
{{AimForCont}} $\map {f'} \xi > 0$.
Then by Mean Value of Concave Real Function it follows that:
:$\map f x \le \map f \xi + \map {f'} \xi \paren {x - \xi} \to -\infty$ as $x \to -\infty$
and therefore is not bounded.
Similarly, suppose $\map {f'} \xi < 0$.
Then by Mean Value of Concave Real Function it follows that:
:$\map f x \le \map f \xi + \map {f'} \xi \paren {x - \xi} \to -\infty$ as $x \to +\infty$
and therefore is likewise not bounded.
Hence $\map {f'} \xi = 0$.
From Zero Derivative implies Constant Function, it follows that $f$ is constant.
{{qed}}
Theorem: Real Function with Strictly Negative Second Derivative is Strictly Concave

Let $f$ be a real function which is twice differentiable on the open interval $\openint a b$ such that: 
:$\map {f' '} x < 0$ for each $x \in \openint a b$. 
Then $f$ is strictly concave on $\openint a b$.

Proof:
From Real Function is Strictly Concave iff Derivative is Strictly Decreasing, $f$ is strictly concave {{iff}} $f'$ is strictly decreasing.
Since $f' ' < 0$, we have that $f'$ is strictly decreasing from Real Function with Strictly Negative Derivative is Strictly Decreasing.
{{qed}}
Theorem: Real Function with Strictly Positive Second Derivative is Strictly Convex

Let $f$ be a real function which is twice differentiable on the open interval $\openint a b$ such that: 
:$\map {f' '} x > 0$ for each $x \in \openint a b$.
Then $f$ is strictly convex on $\openint a b$.

Proof:
From Real Function is Strictly Convex iff Derivative is Strictly Increasing, $f$ is strictly convex {{iff}} $f'$ is strictly increasing.
Since $f' ' > 0$, we have that $f'$ is strictly increasing from Real Function with Strictly Positive Derivative is Strictly Increasing.
{{qed}}
Theorem: Inverse of Strictly Decreasing Strictly Convex Real Function is Strictly Convex

Let $f$ be a real function which is strictly convex on the open interval $I$.
Let $J = f \sqbrk I$.
If $f$ be strictly decreasing on $I$, then $f^{-1}$ is strictly convex on $J$.

Proof:
Let:
:$X = \map f x \in J$
:$Y = \map f y \in J$.
From the definition of strictly convex:
:$\forall \alpha, \beta \in \R_{>0}, \alpha + \beta = 1: \map f {\alpha x + \beta y} < \alpha \map f x + \beta \map f y$
Let $f$ be strictly decreasing on $I$.
Then from Inverse of Strictly Monotone Function it follows that $f^{-1}$ is strictly decreasing on $J$.
Thus:
:$\alpha \map {f^{-1} } X + \beta \map {f^{-1} } Y = \alpha x + \beta y < \map {f^{-1} } {\alpha X + \beta Y}$
Hence $f^{-1}$ is strictly convex on $J$.
{{qed}}
Theorem: Inverse of Strictly Decreasing Strictly Concave Real Function is Strictly Concave

Let $f$ be a real function which is strictly concave on the open interval $I$.
Let $J = f \sqbrk I$.
If $f$ be strictly decreasing on $I$, then $f^{-1}$ is strictly concave on $J$.

Proof:
Let:
:$X = \map f x \in J$
:$Y = \map f y \in J$.
From the definition of strictly concave:
:$\forall \alpha, \beta \in \R_{>0}, \alpha + \beta = 1: \map f {\alpha x + \beta y} > \alpha \map f x + \beta \map f y$
Let $f$ be strictly decreasing on $I$.
From Inverse of Strictly Monotone Function, it follows that $f^{-1}$ is strictly decreasing on $J$.
Thus:
:$\alpha \map {f^{-1} } X + \beta \map {f^{-1} } Y = \alpha x + \beta y > \map {f^{-1} } {\alpha X + \beta Y}$
Hence $f^{-1}$ is strictly concave on $J$.
{{qed}}
Theorem: Inverse of Strictly Increasing Strictly Convex Real Function is Strictly Concave

Let $f$ be a real function which is strictly convex on the open interval $I$.
Let $J = f \sqbrk I$.
If $f$ be strictly increasing on $I$, then $f^{-1}$ is strictly concave on $J$.

Proof:
Let:
:$X = \map f x \in J$
:$Y = \map f y \in J$
From the definition of strictly convex:
:$\forall \alpha, \beta \in \R_{>0}, \alpha + \beta = 1: \map f {\alpha x + \beta y} < \alpha \, \map f x + \beta \, \map f y$
Let $f$ be strictly increasing on $I$.
From Inverse of Strictly Monotone Function it follows that, $f^{-1}$ is strictly increasing on $J$.
Thus:
:$\alpha \, \map {f^{-1} } X + \beta \, \map {f^{-1} } Y = \alpha x + \beta y < \map {f^{-1} } {\alpha X + \beta Y}$
Hence $f^{-1}$ is strictly concave on $J$.
{{qed}}
Theorem: Inverse of Strictly Increasing Strictly Concave Real Function is Strictly Convex

Let $f$ be a real function which is strictly concave on the open interval $I$.
Let $J = f \sqbrk I$.
If $f$ be strictly increasing on $I$, then $f^{-1}$ is strictly convex on $J$.

Proof:
Let $X = \map f x \in J, Y = \map f y \in J$.
From the definition of Strictly concave:
:$\forall \alpha, \beta \in \R_{>0}, \alpha + \beta = 1: \map f {\alpha x + \beta y} > \alpha \map f x + \beta \map f y$
Let $f$ be strictly increasing on $I$.
From Inverse of Strictly Monotone Function, it follows that $f^{-1}$ is strictly increasing on $J$.
Thus:
:$\alpha \map {f^{-1} } X  + \beta \map {f^{-1} } Y = \alpha x + \beta y > \map {f^{-1} } {\alpha X + \beta Y}$
Hence $f^{-1}$ is strictly convex on $J$.
{{qed}}
Theorem: Gamma Function as Integral of Natural Logarithm

Let $x \in \R_{>0}$ be a strictly positive real number.
Then:
:$\ds \map \Gamma x = \int_{\to 0}^1 \paren {\ln \frac 1 t}^{x - 1} \rd t$
where $\Gamma$ denotes the Gamma function.

Proof:
By definition of the Gamma function:
:$\ds \map \Gamma x = \int_0^{\to \infty} t^{x - 1} e^{-t} \rd t$
In order to allow the limits to be evaluated, this is to be expressed as:
:$\ds \map \Gamma x = \lim_{\delta \mathop \to 0^+, \ \Delta \mathop \to +\infty} \int_\delta^\Delta t^{x - 1} e^{-t} \rd t$
where $0 < \delta < \Delta$.
Let $-t = \ln u$.
Then by Derivative of Logarithm Function and the Chain Rule for Derivatives:
:$-1 = \dfrac 1 u \dfrac {\rd u} {\rd t}$
Also:
{{begin-eqn}}
{{eqn | l = -t
      | r = \ln u
}}
{{eqn | ll= \leadsto
      | l = e^{-t}
      | r = u
      | c = Exponential of Natural Logarithm
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \int_\delta^\Delta t^{x - 1} e^{-t} \rd t
      | r = \int_{e^{-\delta} }^{e^{-\Delta} } \paren {-\ln u}^{x - 1} e^{\ln u} \paren {-\frac 1 u \frac {\rd u} {\rd t} } \rd t
      | c = Integration by Substitution
}}
{{eqn | r = \int_{e^{-\Delta} }^{e^{-\delta} } \paren {-\ln u}^{x - 1} e^{\ln u} \paren {\frac 1 u \frac {\rd u} {\rd t} } \rd t
      | c = Reversal of Limits of Definite Integral
}}
{{eqn | r = \int_{e^{-\Delta} }^{e^{-\delta} } \paren {\ln \frac 1 u}^{x - 1} u \frac 1 u \rd u
      | c = Exponential of Natural Logarithm
}}
{{eqn | n = 1
      | r = \int_{e^{-\Delta} }^{e^{-\delta} } \paren {\ln \frac 1 u}^{x - 1} \rd u
      | c = simplification
}}
{{end-eqn}}
Next:
{{begin-eqn}}
{{eqn | l = \lim_{\delta \mathop \to 0^+} e^{-\delta}
      | r = 1
      | c = Exponential of Zero
}}
{{eqn | l = \lim_{\Delta \mathop \to +\infty} e^{-\Delta}
      | r = 0
      | c = Exponential Tends to Zero and Infinity
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \lim_{\delta \mathop \to 0^+, \ \Delta \mathop \to +\infty} \int_{e^{-\Delta} }^{e^{-\delta} } \paren {\ln \frac 1 u}^{x - 1} \rd u
      | r = \int_{e^{-\Delta} }^1 \paren {\ln \frac 1 u}^{x - 1} \rd u
      | c = substituting for the top limit
}}
{{eqn | r = \int_{\to 0}^1 \paren {\ln \frac 1 u}^{x - 1} \rd u
      | c = as $\ln 0$ is undefined
}}
{{end-eqn}}
The result follows by renaming the bound variable $u$ to $t$.
{{qed}}
Theorem: Reversal of Limits of Definite Integral

Let $a \le b$.
Then:
:$\ds \int_a^b \map f x \rd x = -\int_b^a \map f x \rd x$

Proof:
{{begin-eqn}}
{{eqn | l = \int_a^b \map f x \rd x + \int_b^a \map f x \rd x
      | r = \int_a^a \map f x \rd x
      | c = Sum of Integrals on Adjacent Intervals for Integrable Functions
}}
{{eqn | r = 0
      | c = Definite Integral on Zero Interval
}}
{{eqn | ll= \leadsto
      | l = \int_a^b \map f x \rd x
      | r = -\int_b^a \map f x \rd x
}}
{{end-eqn}}
{{CircularStructure|Careful with the above. Down at the bottom of Sum of Integrals on Adjacent Intervals for Integrable Functions use is made of this result. There has been a lot of activity on this area of mathematics, and several people have contributed, possibly without having completely followed through all the chains of implications. </br> My bad. Either way this has to be proven independently since the case $a {{=}} b$ was not considered in that theorem.}}
Theorem: Beta Function is Defined for Positive Reals

Let $x, y \in \R$ be real numbers.
Let $\map \Beta {x, y}$ be the Beta function:
:$\ds \map \Beta {x, y} := \int_{\mathop \to 0}^{\mathop \to 1} t^{x - 1} \paren {1 - t}^{y - 1} \rd t$
Then $\map \Beta {x, y}$ exists provided that $x, y > 0$.

Proof:
Consider the following inequalities, valid for $0 < t < 1$:
{{begin-eqn}}
{{eqn | l = t^{x - 1} \paren {1 - t}^{y - 1}
      | o = <
      | r = t^{x - 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = t^{x - 1} \paren {1 - t}^{y - 1}
      | o = <
      | r = \paren {1 - t}^{y - 1}
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int_{\mathop \to 0}^{\mathop \to 1} t^{x - 1} \rd t
      | r = \intlimits {\frac {t^x} x} {\mathop \to 0} {\mathop \to 1}
      | c = 
}}
{{eqn | r = x - 0
      | c = 
}}
{{end-eqn}}
and similarly:
{{begin-eqn}}
{{eqn | l = \int_{\mathop \to 0}^{\mathop \to 1} \paren {1 - t}^{y - 1} \rd t
      | r = -\intlimits {\frac {\paren {1 - t}^y} y} {\mathop \to 0} {\mathop \to 1}
      | c = 
}}
{{eqn | r = y - 0
      | c = 
}}
{{end-eqn}}
The result follows from the Comparison Test for Improper Integral.
{{qed}}
Theorem: Comparison Test for Improper Integral

Let $I = \openint a b$ be an open real interval.
Let $\phi$ be a real function which is continuous on $I$ and also non-negative on $I$.
Let $f$ be a real function which is continuous on $I$.
Let $f$ satisfy:
:$\forall x \in I: \size {\map f x} \le \map \phi x$
If the improper integral of $\phi$ over $I$ exists, then so does that of $f$.

Proof:
{{WLOG}}, we consider the case $I = \openint 0 \to$ such that $\ds l = \int_0^{\mathop \to +\infty} \map \phi x \rd x$ exists.
Let:
:$\ds a_n = \int_{n - 1}^n \map f x \rd x$
:$\ds b_n = \int_{n - 1}^n \map \phi x \rd x$
for $n = 1, 2, \ldots$
Then the series:
:$\ds \sum_{n \mathop = 1}^\infty b_n$
is a convergent series of positive terms whose sum is $l$.
Also:
$\size {a_n} \le b_n$
for $n = 1, 2, \ldots$
Hence $\ds \sum_{n \mathop = 1}^\infty a_n$ a convergent series by the Comparison Test.
That is:
:$\ds m = \lim_{N \mathop \to \infty} \int_0^N \map f x \rd x$
exists.
Given any $X > 0$, $N$ can be taken to be the smallest natural number which satisfies $N > X$.
Then:
{{begin-eqn}}
{{eqn | l = \size {\int_1^X \map f x \rd x - \int_1^{N - 1} \map f x \rd x}
      | o = \le
      | r = \int_{N - 1}^X \size {\map f x} \rd x
      | c = 
}}
{{eqn | o = \le
      | r = b_N
      | c = 
}}
{{eqn | o = \to
      | r = 0 
      | c = as $N \to \infty$
}}
{{end-eqn}}
It follows that:
:$\ds \lim_{X \mathop \to \infty} \int_1^X \map f x \rd x = m$
as required.
The other cases are treated similarly.
{{qed}}
Theorem: Beta Function is Continuous and Positive on Positive Reals

Let $x, y \in \R$ be real numbers.
Let $\map \Beta {x, y}$ be the Beta function:
:$\ds \map \Beta {x, y} := \int_{\mathop \to 0}^{\mathop \to 1} t^{x - 1} \paren {1 - t}^{y - 1} \rd t$
Let $y \in \R_{>0}$ be given.
Then $\map \Beta {x, y}$ is a positive and continuous function of $x$ on $\R_{>0}$.

Proof:
For each $x > 0$, we have for all $t$ with $0 < t < 1$ that:
:$t^{x - 1} \paren {1 - t}^{y - 1} > 0$
from which it is immediate that $\map \Beta {x, y} > 0$.
{{ProofWanted|Continuity to be established.}}
Theorem: Gamma Function of One Half

:$\map \Gamma {\dfrac 1 2} = \sqrt \pi$

Proof:
From the definition of the Beta function:
:$\map \Beta {x, y} := \dfrac {\map \Gamma x \map \Gamma y} {\map \Gamma {x + y} }$
Setting $x = y = \dfrac 1 2$:
{{begin-eqn}}
{{eqn | l = \map \Beta {\dfrac 1 2, \dfrac 1 2}
      | r = \frac {\map \Gamma {\dfrac 1 2} \map \Gamma {\dfrac 1 2} } {\map \Gamma {\dfrac 1 2 + \dfrac 1 2} }
      | c = 
}}
{{eqn | r = \paren {\map \Gamma {\dfrac 1 2} }^2
      | c = 
}}
{{end-eqn}}
Then from Beta Function of Half with Half:
:$\map \Beta {\dfrac 1 2, \dfrac 1 2} = \pi$
Hence the result.
{{qed}}
Theorem: Gamma Function of One Half

:$\map \Gamma {\dfrac 1 2} = \sqrt \pi$

Proof:
From Euler's Reflection Formula:
:$\forall z \notin \Z: \map \Gamma z \map \Gamma {1 - z} = \dfrac \pi {\map \sin {\pi z} }$
Setting $z = \dfrac 1 2$:
{{begin-eqn}}
{{eqn | l = \map \Gamma {\frac 1 2} \map \Gamma {\frac 1 2}
      | r = \frac \pi {\map \sin {\frac \pi 2} }
      | c = 
}}
{{eqn | r = \frac \pi 1
      | c = Sine of Right Angle
}}
{{eqn | ll= \leadsto
      | l = \map \Gamma {\frac 1 2}
      | r = \pm \sqrt \pi
      | c = 
}}
{{end-eqn}}
By definition of the gamma function:
:$\forall z \in \R_{\ge 0}: \map \Gamma z > 0$
and so the negative square root can be discarded.
Hence:
:$\map \Gamma {\dfrac 1 2} = \sqrt \pi$
as required.
{{qed}}
Theorem: Gamma Function of One Half

:$\map \Gamma {\dfrac 1 2} = \sqrt \pi$

Proof:
{{begin-eqn}}
{{eqn | l = \map \Gamma {\dfrac 1 2}
      | r = \int_0^{\to \infty} t^{-\frac 1 2} e^{-t} \rd t
      | c = {{Defof|Integral Form of Gamma Function|Gamma Function}}
}}
{{eqn | r = \int_0^{\to \infty} u^{-1} e^{-u^2} 2 u \rd u
      | c = Integration by Substitution, $\map \phi u = u^2$
}}
{{eqn | r = 2 \int_0^{\to \infty} e^{-u^2} \rd u
      | c = Linear Combination of Definite Integrals
}}
{{eqn | r = \int_{\to -\infty}^{\to \infty} e^{-u^2} \rd u
      | c = Definite Integral of Even Function
}}
{{eqn | r = \sqrt \pi
      | c = Gaussian Integral
}}
{{end-eqn}}
{{qed}}
Theorem: Gamma Function of One Half

:$\map \Gamma {\dfrac 1 2} = \sqrt \pi$

Proof:
{{begin-eqn}}
{{eqn | l = \map \Gamma {\frac 1 2} 
      | r = \frac {0!} {2^0 0!} \sqrt \pi
      | c = Gamma Function of Positive Half-Integer
}}
{{eqn | r = \sqrt \pi
      | c = Factorial of Zero
}}
{{end-eqn}}
{{qed}}