This repository serves two purposes. First, it is a means for me to learn Verso, by writing a custom blueprint website (and possibly, PDF file) with it. My goal is to replicate and hopefully improve on much of the Leanblueprint functionality.
Second, it has the goal of formalizing results about conditional measures, measure-theoretic entropy and the variational principle. The theory of topological entropy is already in Mathlib, so it is not part of this project.