Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: The Laws of Large Numbers


view this post on Zulip Email Gateway (Feb 11 2021 at 05:40):

From: Gerwin Klein <kleing@unsw.edu.au>
The Laws of Large Numbers
By Manuel Ebers

The Law of Large Numbers states that, informally, if one performs a random experiment X many times and takes the average of the results, that average will be very close to the expected value E[X].

In this entry, I formally prove the strong law and from it the weak law. The approach used for the proof of the strong law is a particularly quick and slick one based on ergodic theory, which was formalised by Gouëzel in another AFP entry.

https://www.isa-afp.org/entries/Laws_of_Large_Numbers.html

Enjoy!
Gerwin


Last updated: Dec 05 2021 at 23:19 UTC