Bayes theorem + future directions

Stream: maths

[Koundinya Vajjha]

hello,

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]

Matrices are in ring_theory/matrix