Theorem: Stirling's Formula/Refinement

A refinement of Stirling's Formula is:
:$n! = \sqrt {2 \pi n} \paren {\dfrac n e}^n \paren {1 + \dfrac 1 {12 n} + \map \OO  {\dfrac 1 {n^2} } }$

Proof:
Let $z\in \R_{>0}$ and $n \in \N_{\ge 0}$
Let $\ds c_n = \ln \map \Gamma {z + n}$
We begin by observing:
{{begin-eqn}}
{{eqn | l = \map \Gamma {z + n}
      | r = \map \Gamma {z + 1} \times \paren {z + 1} \times \paren {z + 2} \times \cdots \times \paren {z + n - 1}
      | c = Gamma Difference Equation
}}
{{eqn | ll = \leadsto
      | l = \ln \map \Gamma {z + n}
      | r = \ln \map \Gamma {z + 1} + \map \ln {z + 1} + \map \ln {z + 2} + \cdots + \map \ln {z + n - 1}
      | c = Sum of Logarithms
}}
{{eqn | ll = \leadsto
      | n = 1
      | l = \ln \map \Gamma {z + n}
      | r = \ln \map \Gamma {z + 1} + \sum_{k \mathop = 1}^{n - 1} \map \ln {z + k}
      | c = 
}}
{{end-eqn}}
Then from $\paren 1$ above, we have:
:$\ds c_n = \ln \map \Gamma {z + 1} + \sum_{k \mathop = 1}^{n - 1} \map \ln {z + k}$
Therefore:
{{begin-eqn}}
{{eqn | l = c_{n + 1} - c_n
      | r = \paren {\ln \map \Gamma {z + 1} + \sum_{k \mathop = 1}^{\paren {n + 1} - 1} \map \ln {z + k} } - \paren {\ln \map \Gamma {z + 1} + \sum_{k \mathop = 1}^{n - 1} \map \ln {z + k} }
      | c = 
}}
{{eqn | ll = \leadsto
      | l = c_{n + 1} - c_n
      | n = 2
      | r = \map \ln {z + n}
      | c = 
}}
{{end-eqn}}
By the analogy between the derivative and the finite difference, we consider $c_n$ to be '''approximately''' $\ds \int \map \ln {z + n} \rd z$.
With this in mind, based upon Primitive of Logarithm of x, we set:
:$\ds c_n = \paren {z + n} \map \ln {z + n} - \paren {z + n} + d_n$
Quick recap:
{{begin-eqn}}
{{eqn | l = c_n
      | r = \ln \map \Gamma {z + n}
      | c = 
}}
{{eqn | r = \ln \map \Gamma {z + 1} + \sum_{k \mathop = 1}^{n - 1} \map \ln {z + k}
      | c = 
}}
{{eqn | ll = \leadsto
      | l = c_n
      | o = \approx
      | r = \int \map \ln {z + n} \rd z
      | c = by the analogy between the derivative and the finite difference
}}
{{eqn | ll = \leadsto
      | n = 3
      | l = c_n
      | r = \paren {z + n} \map \ln {z + n} - \paren {z + n} + d_n
      | c = based upon Primitive of Logarithm of x
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = c_{n + 1} - c_n
      | r = \paren {\paren {z + n + 1} \map \ln {z + n + 1} - \paren {z + n + 1} + d_{n + 1} } - \paren {\paren {z + n} \map \ln {z + n} - \paren {z + n} + d_n }
      | c = from $\paren 3$
}}
{{eqn | ll = \leadsto
      | l = \map \ln {z + n}
      | r = \paren {\paren {z + n + 1} \map \ln {z + n + 1} - \paren {z + n + 1} + d_{n + 1} } - \paren {\paren {z + n} \map \ln {z + n} - \paren {z + n} + d_n }
      | c = from $\paren 2$
}}
{{eqn | r = \paren {z + n + 1} \map \ln {z + n + 1} - \paren {z + n} \map \ln {z + n} + d_{n + 1} - d_n - 1
      | c = 
}}
{{eqn | ll = \leadsto
      | l = d_{n + 1} - d_n
      | r = 1 + \map \ln {z + n} - \paren {\paren {z + n + 1} \map \ln {z + n + 1} - \paren {z + n} \map \ln {z + n} }
      | c = rearranging and moving $d_{n + 1} - d_n$ to the {{LHS}}
}}
{{eqn | r = 1 - \paren {\paren {z + n + 1} \map \ln {z + n + 1} - \paren {z + n + 1} \map \ln {z + n} }
      | c = 
}}
{{eqn | r = 1 - \paren {z + n + 1} \map \ln {\dfrac {z + n + 1} {z + n} }
      | c = Sum of Logarithms
}}
{{eqn | r = 1 - \paren {z + n + 1} \map \ln {1 + \dfrac 1 {z + n} }
      | c = 
}}
{{eqn | r = 1 - \paren {z + n + 1} \paren {\paren {\dfrac 1 {z + n} } - \dfrac {\paren {\dfrac 1 {z + n} }^2 } 2 + \dfrac {\paren {\dfrac 1 {z + n} }^3 } 3 - \cdots }
      | c = Power Series Expansion for Logarithm of 1 + x
}}
{{eqn | r = 1 - \paren {z + n} \paren {\paren {\dfrac 1 {z + n} } - \dfrac {\paren {\dfrac 1 {z + n} }^2 } 2 + \dfrac {\paren {\dfrac 1 {z + n} }^3 } 3 - \cdots } - \paren {\paren {\dfrac 1 {z + n} } - \dfrac {\paren {\dfrac 1 {z + n} }^2 } 2 + \dfrac {\paren {\dfrac 1 {z + n} }^3 } 3 - \cdots }
      | c = 
}}
{{eqn | r = 1 - \paren {\paren {1 } - \dfrac {\paren {\dfrac 1 {z + n} } } 2 + \dfrac {\paren {\dfrac 1 {z + n} }^2 } 3 -  \cdots } - \paren {\paren {\dfrac 1 {z + n} } - \dfrac {\paren {\dfrac 1 {z + n} }^2 } 2 + \dfrac {\paren {\dfrac 1 {z + n} }^3 } 3 - \cdots }
      | c = distributing $\paren {z + n}$
}}
{{eqn | r = \paren {\dfrac {\paren {\dfrac 1 {z + n} } } 2 - \dfrac {\paren {\dfrac 1 {z + n} }^2 } 3 - \cdots } - \paren {\paren {\dfrac 1 {z + n} } - \dfrac {\paren {\dfrac 1 {z + n} }^2 } 2 + \dfrac {\paren {\dfrac 1 {z + n} }^3 } 3 - \cdots }
      | c = 
}}
{{eqn | r = \paren {\paren {\frac 1 2 - 1} \dfrac 1 {z + n} + \paren {-\frac 1 3 + \frac 1 2} \dfrac 1 {\paren {z + n}^2 } + \cdots}
      | c = 
}}
{{eqn | ll = \leadsto
      | n = 4
      | l = d_{n + 1} - d_n
      | r = \paren {-\dfrac 1 {2 \paren {z + n} } + \dfrac 1 {6 \paren {z + n}^2 } - \cdots}
      | c = 
}}
{{end-eqn}}
Let $\ds d_n = e_n - \dfrac 1 2 \map \ln {z + n}$.
Then:
{{begin-eqn}}
{{eqn | l = d_{n + 1} - d_n
      | r = \paren {e_{n + 1} - \frac 1 2 \map \ln {z + n + 1} } - \paren {e_n - \frac 1 2 \map \ln {z + n} }
      | c = 
}}
{{eqn | r = e_{n + 1} - e_n - \frac 1 2 \map \ln {\dfrac {z + n + 1} {z + n} }
      | c = Sum of Logarithms
}}
{{eqn | r = e_{n + 1} - e_n - \frac 1 2 \map \ln {1 + \dfrac 1 {z + n} }
      | c = 
}}
{{eqn | ll = \leadsto
      | l = e_{n + 1} - e_n
      | r = d_{n + 1} - d_n + \frac 1 2 \map \ln {1 + \frac 1 {z + n} }
      | c = rearranging and moving $e_{n + 1} - e_n$ to the {{LHS}}
}}
{{eqn | r = \paren {-\dfrac 1 {2 \paren {z + n} } + \dfrac 1 {6 \paren {z + n}^2} - \cdots} + \frac 1 2 \paren {\paren {\dfrac 1 {z + n} } - \dfrac {\paren {\dfrac 1 {z + n} }^2 } 2 + \cdots}
      | c = from $\paren 4$ above and Power Series Expansion for Logarithm of 1 + x
}}
{{eqn | r = \paren { \paren {\frac 1 6 - \frac 1 4 } \dfrac 1 {\paren {z + n}^2} + \OO \paren {\frac 1 {\paren {z + n}^3} } } 
      | c = where $\OO$ is big-$\OO$ notation
}}
{{eqn | ll = \leadsto
      | n = 5
      | l = e_{n + 1} - e_n
      | r = \paren {-\dfrac 1 {12 \paren {z + n}^2} + \OO \paren {\frac 1 {\paren {z + n}^3} } } 
      | c = 
}}
{{end-eqn}}
We now observe that:
{{begin-eqn}}
{{eqn | l = e_n - e_0
      | r = \paren {e_1 - e_0} + \paren {e_2 - e_1} + \paren {e_3 - e_2} + \cdots + \paren {e_{n - 1} - e_{n - 2} } + \paren {e_n - e_{n - 1} }
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^{n - 1} \paren {e_{k + 1} - e_k }
      | c = {{Defof|Telescoping Series}}
}}
{{eqn | r = \sum_{k \mathop = 0}^{n - 1} \paren {-\dfrac 1 {12 \paren {z + k}^2 } + \OO \paren {\frac 1 {\paren {z + k}^3} } } 
      | c = from $\paren 5$ above
}}
{{end-eqn}}
Let $\ds \map {K_1} z = \lim_{n \mathop \to \infty} \paren {e_n - e_0}$.
Then:
{{begin-eqn}}
{{eqn | l = e_n - e_0
      | r = \sum_{k \mathop = 0}^{n - 1} \paren {e_{k + 1} - e_k}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^\infty \paren {e_{k + 1} - e_k} - \sum_{k \mathop = n}^\infty \paren {e_{k + 1} - e_k}
      | c = Indexed Summation over Adjacent Intervals
}}
{{eqn | ll = \leadsto
      | l = e_n
      | r = e_0 + \map {K_1} z - \sum_{k \mathop = n}^\infty \paren {e_{k + 1} - e_k}
      | c = adding $e_0$ to both sides and $\ds \map {K_1} z = \lim_{n \mathop \to \infty} \paren {e_n - e_0}$
}}
{{eqn | r = e_0 + \map {K_1} z - \sum_{k \mathop = n}^\infty \paren { -\dfrac 1 {12 \paren {z + k}^2 } + \OO \paren {\frac 1 {\paren {z + k}^3} } }
      | c = from $\paren 5$ above
}}
{{eqn | r = e_0 + \map {K_1} z - \int_n^\infty \paren { -\dfrac 1 {12 \paren {z + k}^2} + \OO \paren {\frac 1 {\paren {z + k}^3} } } \rd k
      | c = approximating the sum with an integral
}}
{{eqn | r = e_0 + \map {K_1} z - \intlimits {\dfrac 1 {12 \paren {z + k} } + \OO \paren {\frac 1 {\paren {z + k}^2} } } n \infty 
      | c = Primitive of Power
}}
{{eqn | r = e_0 + \map {K_1} z + \dfrac 1 {12 \paren {z + n} } + \OO \paren {\frac 1 {\paren {z + n}^2} } 
      | c = 
}}
{{eqn | ll = \leadsto
      | n = 6
      | l = e_n
      | r = \map \ln {\map C z} + \dfrac 1 {12 \paren {z + n} } + \OO \paren {\frac 1 {\paren {z + n}^2} } 
      | c = let $\map \ln {\map C z} = e_0 + \map {K_1} z$
}}
{{end-eqn}}
Therefore, we have:
{{begin-eqn}}
{{eqn | l = c_n
      | r = \paren {z + n} \map \ln {z + n} - \paren {z + n} + d_n
      | c = from $\paren 3$ above
}}
{{eqn | r = \paren {z + n} \map \ln {z + n} - \paren {z + n} + \paren {e_n - \frac 1 2 \map \ln {z + n} }
      | c = substituting $\ds d_n = e_n - \dfrac 1 2 \map \ln {z + n}$
}}
{{eqn | r = \paren {z + n - \frac 1 2} \map \ln {z + n} - \paren {z + n} + \paren {\map \ln {\map C z} + \dfrac 1 {12 \paren {z + n} } + \OO \paren {\frac 1 {\paren {z + n}^2 } } }
      | c = from $\paren 6$ above
}}
{{end-eqn}}
Exponentiating both sides, we obtain:
{{begin-eqn}}
{{eqn | l = \map \Gamma {z + n}
      | r = \map \exp {\paren {z + n - \frac 1 2} \map \ln {z + n} - \paren {z + n} + \paren {\map \ln {\map C z} + \frac 1 {12 \paren {z + n} } + \OO \paren {\frac 1 {\paren {z + n}^2 } } } }
      | c = Exponential of Natural Logarithm
}}
{{eqn | r = \map C z \paren {z + n}^{z + n - \frac 1 2} \map \exp {-\paren {z + n} } \map \exp {\frac 1 {12 \paren {z + n} } + \OO \paren {\frac 1 {\paren {z + n}^2 } } }
      | c = Product of Powers
}}
{{eqn | ll = \leadsto
      | l = \map \Gamma {z + n}
      | n = 7
      | r = \map C z \paren {z + n}^{z + n - \frac 1 2} \map \exp {-\paren {z + n} } \paren {1 + \frac 1 {12 \paren {z + n} } + \OO \paren {\frac 1 {\paren {z + n}^2 } } }
      | c = Power Series Expansion for Exponential Function
}}
{{end-eqn}}
We claim $\map C z$ is independent of $z$.
{{begin-eqn}}
{{eqn | l = 1
      | r = \lim_{n \mathop \to \infty} n^{-z} \frac {\map \Gamma {n + z} } {\map \Gamma n}
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} n^{-z} \frac {\map C z \paren {z + n}^{z + n - \frac 1 2} \map \exp {-\paren {z + n} } } {\map C 0 n^{n - \frac 1 2} \map \exp {-n} }
      | c = 
}}
{{eqn | r = \frac {\map C z} {\map C 0} \lim_{n \mathop \to \infty} \frac { \paren {z + n}^{z + n - \frac 1 2} \map \exp {-\paren {z + n} } } { n^{z + n - \frac 1 2} \map \exp {-n} }
      | c = 
}}
{{eqn | r = \frac {\map C z} {\map C 0} \lim_{n \mathop \to \infty} \paren {1 + \frac z n}^{z + n - \frac 1 2} e^{-z}
      | c = 
}}
{{eqn | r = \frac {\map C z} {\map C 0} e^z e^{-z}
      | c = Real Exponential Function as Limit of Sequence
}}
{{eqn | r = \frac {\map C z} {\map C 0 }
      | c = 
}}
{{end-eqn}}
Therefore, $\map C z$ is a constant, and:
:$\map \Gamma z \sim C z^{z - \frac 1 2} e^{-z}$ as $z \to \infty$
Therefore:
{{begin-eqn}}
{{eqn | l = \map \Gamma z
      | o = \sim
      | r = C z^{z - \frac 1 2} e^{-z}
      | c = 
}}
{{eqn | ll = \leadsto
      | l = z \map \Gamma z
      | o = \sim
      | r = z C z^{z - \frac 1 2} e^{-z}
      | c = multiplying both sides by z
}}
{{eqn | ll = \leadsto
      | l = \map \Gamma {z + 1}
      | o = \sim
      | r = C z^{z + \frac 1 2} e^{-z}
      | c = Gamma Difference Equation
}}
{{eqn | ll = \leadsto
      | l = z!
      | o = \sim
      | r = C z^{z + \frac 1 2} e^{-z}
      | c = Gamma Function Extends Factorial
}}
{{end-eqn}}
To determine $C$, we use Wallis's Product:
{{begin-eqn}}
{{eqn | l = \pi
      | r = 2 \prod_{k \mathop = 1}^\infty \frac {2 k} {2 k - 1} \cdot \frac {2 k} {2 k + 1}
      | c = 
}}
{{eqn | r = 2 \prod \paren {\frac 2 1 \cdot \frac 2 3} \paren {\frac 4 3 \cdot \frac 4 5} \paren {\frac 6 5 \cdot \frac 6 7} \cdots
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \dfrac 2 {2 n + 1} \prod_{k \mathop = 1}^n \frac {\paren {2 k}^2} {\paren {2 k - 1}^2}
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \dfrac 1 {n + \frac 1 2} \prod_{k \mathop = 1}^n \frac {\paren {2 k}^2} {\paren {2 k - 1}^2} \dfrac {\paren {2 k}^2} {\paren {2 k}^2}
      | c = multiplying by $1$
}}
{{eqn | r = \lim_{n \mathop \to \infty} \dfrac 1 {n + \frac 1 2} \prod_{k \mathop = 1}^n \frac {2^4 k^4} {\paren {\paren {2 k - 1} \paren {2 k} }^2}
      | c = 
}}
{{eqn | ll = \leadsto
      | l = \pi
      | r = \lim_{n \mathop \to \infty} \frac {2^{4 n} \paren {n!}^4} {\paren {\paren {2 n}!}^2 \paren {n + \frac 1 2} }
      | c = 
}}
{{eqn | ll = \leadsto
      | l = \sqrt {\pi}
      | r = \lim_{n \mathop \to \infty} \sqrt {\frac {2^{4 n} \paren {n!}^4} {\paren {\paren {2 n}!}^2 \paren {n + \frac 1 2} } }
      | c = taking the Square Root of both sides
}}
{{eqn | ll = \leadsto
      | l = \sqrt {\pi}
      | n = 8
      | r = \lim_{n \mathop \to \infty} \frac {2^{2 n} \paren {n!}^2} {\paren {2 n}! \sqrt {n + \frac 1 2} }
      | c = 
}}
{{end-eqn}}
Substituting for $n!$ in $(8)$ yields:
{{begin-eqn}}
{{eqn | l = \sqrt {\pi}
      | r = \lim_{n \mathop \to \infty} \frac {2^{2 n} \paren {C n^{n + \frac 1 2} e^{-n} }^2} {C \paren {2 n}^{2 n + \frac 1 2} e^{- 2 n} \sqrt {n + \frac 1 2} }
      | c = $n! = C n^{n + \frac 1 2} e^{-n}$
}}
{{eqn | ll = \leadsto
      | l = \sqrt {\pi}
      | r = C \lim_{n \mathop \to \infty} \frac {2^{2 n} n^{2 n + 1} e^{-2 n} } {\paren {2 n}^{2 n + \frac 1 2} e^{- 2 n} \sqrt {n + \frac 1 2} }
      | c = Power of Product
}}
{{eqn | ll = \leadsto
      | l = \sqrt {\pi}
      | r = C \lim_{n \mathop \to \infty} \frac n {\paren {2 n}^{\frac 1 2} \sqrt {n + \frac 1 2} }
      | c = 
}}
{{eqn | ll = \leadsto
      | l = C
      | r = \sqrt {2 \pi}
      | c = 
}}
{{end-eqn}}
Putting all of the pieces together, we have:
{{begin-eqn}}
{{eqn | l = \map \Gamma {z + n}
      | r = \map C z \paren {z + n}^{z + n - \frac 1 2} \map \exp {-\paren {z + n} } \paren {1 + \frac 1 {12 \paren {z + n} } + \OO \paren {\frac 1 {\paren {z + n}^2 } } }
      | c = from $\paren 7$ above
}}
{{eqn | ll = \leadsto
      | l = \map \Gamma {z + n}
      | r = \sqrt {2 \pi} \paren {z + n}^{z + n - \frac 1 2} \map \exp {-\paren {z + n} } \paren {1 + \frac 1 {12 \paren {z + n} } + \OO \paren {\frac 1 {\paren {z + n}^2 } } }
      | c = $C = \sqrt {2 \pi}$
}}
{{eqn | ll = \leadsto
      | l = \map \Gamma z
      | r = \sqrt {2 \pi} z^{z - \frac 1 2} e^{-z} \paren {1 + \frac 1 {12 z } + \OO \paren {\frac 1 {z^2 } } }
      | c = setting $n = 0$
}}
{{eqn | ll = \leadsto
      | l = z \map \Gamma z
      | r = z \sqrt {2 \pi} z^{z - \frac 1 2} e^{-z} \paren {1 + \frac 1 {12 z } + \OO \paren {\frac 1 {z^2 } } }
      | c = multiplying both sides by z
}}
{{eqn | ll = \leadsto
      | l = \map \Gamma {z + 1}
      | r = \sqrt {2 \pi} z^{z + \frac 1 2} e^{-z} \paren {1 + \frac 1 {12 z } + \OO \paren {\frac 1 {z^2 } } }
      | c = Gamma Difference Equation
}}
{{eqn | ll = \leadsto
      | l = z!
      | r = \sqrt {2 \pi z} \paren {\dfrac z e}^z \paren {1 + \dfrac 1 {12 z} + \map \OO  {\dfrac 1 {z^2} } }
      | c = Gamma Function Extends Factorial
}}
{{end-eqn}}
{{qed}}