## Stream: maths

### Topic: Bayes theorem + future directions

#### Koundinya Vajjha (Dec 21 2018 at 05:21):

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 (Dec 21 2018 at 05:28):

Matrices are in ring_theory/matrix

Last updated: May 11 2021 at 16:22 UTC