My copy of mathlib 🍅 This repository stores my work-in-progress branches from Mathlib. The major ones that I've been working on are listed below. maximal inequality and pointwise ergodic theorem the ergodic decomposition, via categories