Koundinya Vajjha (Dec 21 2018 at 05:21):
I have just completed a formalization of Bayes theorem building on top of the measure theory library. this was my first formalization effort so it is a bit rough around the edges and needs cleaning up. https://github.com/kodyvajjha/mathlib/commit/54639f16ec9e6a646fe43d870131a6099e8a550c
i had set this target as a first milestone in formalizing the (G)ARCH time series models, and I wanted to ask the community if they had any tips/suggestions on getting there. as i understand it - matrices aren't yet formalized, are there any plans on getting to matrices in the near future?
Chris Hughes (Dec 21 2018 at 05:28):
Matrices are in
Last updated: May 11 2021 at 16:22 UTC