The proof assumes basic properties of
continued fractions. Let T : x \mapsto 1/x \mod 1 be the
Gauss map. Let \rho(t) = \frac{1}{(1+t)\ln 2} be the
probability density function for the Gauss distribution, which is preserved under the Gauss map. Since the probability density function is bounded above and below, a set is negligible with respect to the
Lebesgue measure if and only if to the Gauss distribution.
Lemma Lemma. \frac 1n \ln T^n x \to 0.
Proof. Since T^nx \leq 1, we have \frac 1n \ln T^n x \to 0 if and only if \liminf\frac 1n \ln T^n x = 0 Let us consider the set of all x that have \liminf\frac 1n \ln T^n x . That is, \{x : \exists c > 0, \forall N \geq 1, \exists n \geq N, T^n x = \cup_{c > 0} \cap_{N \geq 1} \cup_{n \geq N} [0; \N, \dots, \N, a_n > e^{cn}, \N, \dots] where [0; \N, \dots, \N, a_n > e^{cn}, \N, \dots] denotes the set of numbers whose continued fraction expansion has a_n > e^{cn} , but no other constraints. Now, since the Gauss map preserves the Gauss measure,[0; \N, \dots, \N, a_n > e^{cn}, \N, \dots]has the same Gauss measure as [0; a_n > e^{cn}, \N, \dots], which is the same as \int_0^{e^{-cn}} \rho(t)dt = \log_2(1+e^{-cn})\sim \frac{e^{-cn}}{\ln 2} The union over \cup_{n \geq N} sums to \sim \frac{e^{-cN}}{(1-e^{-c})\ln 2}, which at the N\to\infty limit is zero. Thus the set of such x has Gauss measure zero.
Finish the estimate Now, expand the term using basic continued fraction properties:\ln\left| x - \frac{p_n}{q_n} \right| = \ln \frac{T^n x}{q_n(q_n + q_{n-1}T^n x )} = - 2\ln q_n + \ln T^n x - \ln\left(1 + \frac{q_{n-1}}{q_n}T^n x \right)The second is o(n). The third term is \in [\ln 1, \ln 2]. Both disappear after dividing by n.Thus\lim_{n} \frac 1n \ln\left| x - \frac{p_n}{q_n} \right| = -2 \lim_n \frac 1n \ln q_n = -\frac{\pi^2}{6\ln 2} where we used the result from
Lévy's constant. ==References==