Proof of the central limit theorem in Lean.
Current status: the CLT for i.i.d. real valued random variables is done and has been upstreamed to Mathlib. No further development will happen here.
Blueprint: https://remydegenne.github.io/CLT/blueprint/
RemyDegenne/CLT
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|