Zulip Chat Archive

Stream: maths

Topic: Bayes theorem + future directions

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Dec 21 2018 at 05:28):

Matrices are in ring_theory/matrix

Last updated: May 11 2021 at 16:22 UTC