Formalization of Large Deviations

Brief: Formalize the theory of large deviations in an ITP
Jump To: Parent Description

  • Large deviations theory is covered here: 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.