I got this book. "Probability: A Graduate course" by Allan Gut. I'd like to read it to learn about probability theory.
Previously, I argued that, given a clear enough structure and documentation, Isabelle theory files could be used to introduce students to mathematical topics in a formal way- I want to put my money where my mouth is, and see if I can produce an Isabelle theory file that accompanies my studies.
Ideally, it could then be used by others to get a structured overview of concepts from basic probability theory and of how they are represented in the Isabelle library.
In a perfect world, I want to formalise the results and definitions I'm interested in learning about myself, while using others (in particular those relating to analysis) from the Isabelle library. I shall try one of these two:
(i) Make a nice selection of imports that lets me assume exactly what I don't want to attempt myself.
(ii) Just import everything but creating duplicate definitions / results, cross-referencing with the Isabelle library every now and then.
We'll see how it goes.