Basics of finite probability theory

[malarbol]

This PR introduces a new module finite-probability-theory with some basic definitions on finite probability theory, following https://people.cs.uchicago.edu/~laci/reu02/prob.pdf.

• finite-probability-theory.positive-distributions-on-finite-types:
  • functions from a finite type to ℝ⁺;
  • total measure of a positive distribution.
• finite-probability-theory.probability-distributions-on-finite-types:
  • positive distributions with total measure equal to one.
• finite-probability-theory.finite-probability-spaces:
  • finite types with a probability distribution;
  • finite probability types are inhabited.
• finite-probability-theory.random-real-variables-finite-probability-spaces:
  • functions from a finite probability space to ℝ.
• finite-probability-theory.expected-value-random-real-variables-finite-probability-spaces:
  • weighted sum of the values of the random variable.

[fredrik-bakke]

Very cool project!

I wonder if this namespace should be called finite-probability-theory, since it's flavour is quite distinct from general probability theory.

[fredrik-bakke]

references :

• https://people.cs.uchicago.edu/~laci/reu02/prob.pdf

By the way, you can add your reference to our references.bib file, so that you can cite it on the relevant pages!
See the guide at https://unimath.github.io/agda-unimath/CITING-SOURCES.html

[malarbol]

Very cool project!

Thanks. I hope it can be a new playground for all the new results on real numbers.

I wonder if this namespace should be called finite-probability-theory, since it's flavour is quite distinct from general probability theory.

Sure. I thought that future results on non-finite probability theory could also go here, but having them separated would be coherent with the current division finite-group-theory/group-theory.

[fredrik-bakke]

Let me know if you have a preferred color code for the label, since it is used for the dependency graph art :)

[malarbol]

Let me know if you have a preferred color code for the label, since it is used for the dependency graph art :)

I'm ok with the one from the new label finite-probability-theory you just created.

[fredrik-bakke]

should this not be nonnegative real numbers?

[malarbol]

I'v seen contradicting references for this but there seems to be a slight preference for only considering positive distributions.

Moreover, in our context, I think it will be easier to work with: for a nonnegative real number we can't decide if it's zero or positive so we won't be able to identify elements with zero-measure.

[fredrik-bakke]

Okiedokie. Please make sure to reflect this choice in the naming though, since in the real world an event can be impossible.

[malarbol]

I'm not sure where you stand on the positive vs. nonnegative debate. I added the reference to Balai00 but didn't emphasize on the positive part. Maybe I should?

Also, I have the feeling that the notion of "impossible events" will appear later, considering random variables (functions from the finite probability space to ℝ) and, then, some subsets of ℝ will have empty pre-image, and "zero-measure". But I haven't really worked that part out, yet.

[lowasser]

I would definitely expect to have to use nonnegative numbers -- impossible events, the intersection of exclusive events...

[malarbol]

I would definitely expect to have to use nonnegative numbers -- impossible events, the intersection of exclusive events...

I think this will come later, when we define events in a finite probability space as subsets of the underlying type. Then the probability of an event will be the sum of the probabilities of its elements (decidability issues to be discussed) and the empty event will have zero probability. Nonetheless it really seems reasonable to have positive values for atomic distributions on finite types.

[fredrik-bakke]

A nonempty event could also be impossible.

[malarbol]

A nonempty event could also be impossible.

yes.
I have the feeling I'm not explaining myself well.
I can try to change the definition to consider nonnegative distributions if you really want to. Do you have reference that construct finite probability spaces this way?

[malarbol]

There's still a lot more to say but maybe it's good enough to start.

[fredrik-bakke]

The large ring of real numbers has now been contributed to the library #1664 :)