FRDCSA:

Formalization of Large Deviations

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

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.