The central limit theorem is now in the Isabelle repository:
* Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM
Proof of the central limit theorem: includes weak convergence, characteristic
functions, and Levy's uniqueness and continuity theorem.
On Wed, 6 Jan 2016, Johannes Hölzl wrote:
The central limit theorem is now in the Isabelle repository:
* Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM
Proof of the central limit theorem: includes weak convergence, characteristic
functions, and Levy's uniqueness and
