## Formalization of Large Deviations

- Large deviations theory is covered here: https://en.wikipedia.org/wiki/Large_deviations_theory We are interested in formalizing aspects of large deviation theory in an ITP system like coq or Isabelle, in order to calibrate our efforts to formalize, aka make rigorous in a formal language, a useful field of mathematics for our Mathematical Knowledge Management efforts.