coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Formalization of probability estimator in Coq

From: Van Chan Ngo <chan.ngo2203 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Formalization of probability estimator in Coq
Date: Mon, 9 Mar 2020 11:54:19 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=chan.ngo2203 AT gmail.com; spf=Pass smtp.mailfrom=chan.ngo2203 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f51.google.com
Ironport-phdr: 9a23:tq2cxxFaeMm8ZSrsUCBZap1GYnF86YWxBRYc798ds5kLTJ76osSwAkXT6L1XgUPTWs2DsrQf1LqQ7viocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TXhpQIVTx74LE9+Ivn/Mo/UlcW+ke6oqLPJZAAdujO7KZhyJRP+iwrW/p0dgYJkbKA+zUGT+iBgdOFfxGcuLlWWyUWvrvys9YJupnwD88kq8NRNBP2jI/YICIdABTFjCFgbodXxvECaHwSK73oYFG4Rl0gQWlmX3FTBRp709xDCmK940SieM9fxSOltCzun5qZvDhTvjXVebmNrwCTsksV1yZljjlehqhh4mdOGZYiUML95YvqYc45DA2VGWclVWmpKBYbuN4Y=

Hello Coq Users,

I have a questions about formalization of probability estimator in Coq.

Given that there are many probability estimation techniques such as Crude Monte Carlo method, important sampling, and (adaptive) multi-split sampling.

Is there any formalization of the above estimations in Coq?

Any information will be appreciated.

Best,

-Van Chan

[Coq-Club] Formalization of probability estimator in Coq, Van Chan Ngo, 03/09/2020