I was expecting some math but there is only a norm, I would be more interested in how to transfer from advanced math to code. example : what would be a good code abstraction for a Borel Space
@somethingsome If you want to turn arbitrary maths into code, you should take a look at interactive proof assistants. I'm a fan of https://leanprover-community.github.io/