Proof of the central limit theorem in Lean.
Current status: we have a full proof of the CLT for real random variables if we assume Prokhorov's theorem.
Blueprint: https://remydegenne.github.io/CLT/blueprint/
clt
Central limit theorem in Lean
cltProof of the central limit theorem in Lean.
Current status: we have a full proof of the CLT for real random variables if we assume Prokhorov's theorem.
Blueprint: https://remydegenne.github.io/CLT/blueprint/