This is a formalisation of Prokhorov's theorem in Lean4 for Mathlib. This repository is a mess as I PRed code to mathlib as I went, bumping when I wrote new code. I have not fixed the code that breaks with each bump as it is in Mathlib anyway, but I keep this as storage for some of the stuff I have written.
-
Notifications
You must be signed in to change notification settings - Fork 3
FormulaRabbit81/ProkhorovTheorem
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
Prokhorov's Theorem formalisation
Resources
Stars
Watchers
Forks
Packages 0
No packages published