Basics of finite probability theory #1626

malarbol · 2025-10-24T02:31:32Z

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 · 2025-10-24T11:39:45Z

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 · 2025-10-24T13:41:43Z

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 · 2025-10-24T14:43:37Z

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 · 2025-10-24T14:48:27Z

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

malarbol · 2025-10-24T15:01:32Z

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.

src/probability-theory/measures-on-finite-types.lagda.md

fredrik-bakke · 2025-10-24T15:05:52Z

src/probability-theory/measures-on-finite-types.lagda.md

+A
+{{#concept "measure" Disambiguation="on a finite type" Agda=measure-Finite-Type}}
+on a [finite type](univalent-combinatorics.finite-types.md) is a function into
+the [positive real numbers](real-numbers.positive-real-numbers.md).


should this not be nonnegative real numbers?

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.

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

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.

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

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.

A nonempty event could also be impossible.

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?

src/probability-theory/measures-on-finite-types.lagda.md

src/finite-probability-theory/finite-probability-spaces.lagda.md

lowasser · 2025-10-24T16:34:21Z

...e-probability-theory/expected-value-random-real-variables-finite-probability-spaces.lagda.md

+
+## Definitions
+
+### Expected value of a random real variable in a finite probability space


This seems probably true of any rational ring, FWIW? It might help variables more usefully expressed in terms of integers and rational numbers.

I thought about it too but I think I'd need "rational-positive-distributions" for that (I'd need the coefficients μ(x) to be rational); maybe it would be a good thing to have. I can give it a go or feel free to join in if you want to!

On the other hand, we'll probably have the concept of "real ring" sometimes in the future so we'll be able to consider random variables in real rings then.

I noticed you made quite some progress on real multiplication etc. Do we have the ring of real numbers already or are there still some missing laws? ~~I suspect distributivity must be quite painful~~ 🫤 EDIT: I see distributivity is already there 🎊

[...] Do we have the ring of real numbers already or are there still some missing laws? [...]

you're probably working on large rings and such. Let's wait then. I think we need som ring structure on ℝ to follow with more interesting results.

Indeed, see #1586. The ring at lzero was originally contributed, but in the end it was concluded to wait for the large ring.

Perfect. I'll just wait then.

Wait, do you mean you will wait with finishing this PR until that one has been merged? If so, please mark this one as a draft.

Wait, do you mean you will wait with finishing this PR until that one has been merged? If so, please mark this one as a draft.

Yes. One of the endgoal is to prove that the space of real random variables is an ℝ-module and the expected value a linear map. For this I'll need more algebraic structure. And I'll need more time to figure out the level-polymorphic construction.

Thanks for your help anyways. Sorry for your time.

src/finite-probability-theory/random-real-variables-finite-probability-spaces.lagda.md

malarbol · 2025-10-24T20:05:07Z

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

Co-authored-by: Fredrik Bakke <[email protected]>

src/finite-probability-theory/finite-probability-spaces.lagda.md

fredrik-bakke · 2025-10-24T23:22:01Z

...e-probability-theory/expected-value-random-real-variables-finite-probability-spaces.lagda.md

+
+## Definitions
+
+### Expected value of a random real variable in a finite probability space


Indeed, see #1586. The ring at lzero was originally contributed, but in the end it was concluded to wait for the large ring.

Co-authored-by: Fredrik Bakke <[email protected]>

src/finite-probability-theory/finite-probability-spaces.lagda.md

src/finite-probability-theory/positive-distributions-on-finite-types.lagda.md

fredrik-bakke · 2025-10-25T13:31:23Z

src/finite-probability-theory/positive-distributions-on-finite-types.lagda.md

+```agda
+module _
+  {l : Level} (Ω : Finite-Type l)
+  where
+
+  positive-distribution-Finite-Type : UU (lsuc lzero ⊔ l)
+  positive-distribution-Finite-Type = type-Finite-Type Ω → ℝ⁺ lzero
+
+  real-positive-distribution-Finite-Type :
+    positive-distribution-Finite-Type → type-Finite-Type Ω → ℝ lzero
+  real-positive-distribution-Finite-Type μ = real-ℝ⁺ ∘ μ
+```


You're missing a universe level parameter in your definition here, and consequently everywhere else too

Suggested change

```agda

module _

{l : Level} (Ω : Finite-Type l)

where

positive-distribution-Finite-Type : UU (lsuc lzero ⊔ l)

positive-distribution-Finite-Type = type-Finite-Type Ω → ℝ⁺ lzero

real-positive-distribution-Finite-Type :

positive-distribution-Finite-Type → type-Finite-Type Ω → ℝ lzero

real-positive-distribution-Finite-Type μ = real-ℝ⁺ ∘ μ

```

```agda

module _

{l1 : Level} (l2 : Level) (Ω : Finite-Type l1)

where

positive-distribution-Finite-Type : UU (l1 ⊔ lsuc l2)

positive-distribution-Finite-Type = type-Finite-Type Ω → ℝ⁺ l2

module _

{l1 l2 : Level} (Ω : Finite-Type l1)

where

real-positive-distribution-Finite-Type :

positive-distribution-Finite-Type l2 Ω → type-Finite-Type Ω → ℝ l2

real-positive-distribution-Finite-Type μ = real-ℝ⁺ ∘ μ

```

If you don't introduce this level parameter now you'll probably hit your face against resizing problems later on

in general, your definitions should be in terms of ℝ at a universe level always. Always maximize the number of universe level parameters.

I started out this way but since we only have the additive abelian group of real numbers at lzero, to define even the simplest thing like the total measure, I needed to restrict to lzero.

I think I'll mark this as a draft and wait for large algebraic structures and re-try this then.

The large algebraic structures you need should be in.

src/finite-probability-theory/probability-distributions-on-finite-types.lagda.md

fredrik-bakke · 2025-10-25T13:39:54Z

src/finite-probability-theory/random-real-variables-finite-probability-spaces.lagda.md

+### Atomic random variables in a finite probability space
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Probability-Space l)
+  (e : type-Finite-Probability-Space Ω)
+  where
+
+  atomic-random-real-variable-Finite-Probability-Space :
+    random-real-variable-Finite-Probability-Space Ω
+  atomic-random-real-variable-Finite-Probability-Space e' =
+    rec-coproduct
+      ( λ _ → one-ℝ)
+      ( λ _ → zero-ℝ)
+      ( has-decidable-equality-is-finite
+        ( is-finite-type-Finite-Probability-Space Ω)
+        ( e)
+        ( e'))
+```


This should IMO be defined in terms of a general ~~large~~ semiring, and on its own page.

I mean a general semiring.

fredrik-bakke · 2025-10-25T13:41:12Z

src/finite-probability-theory/real-random-variables-finite-probability-spaces.lagda.md

+### Constant random variables in a finite probability space
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Probability-Space l)
+  where
+
+  const-random-real-variable-Finite-Probablity-Space :
+    (x : ℝ lzero) → random-real-variable-Finite-Probability-Space Ω
+  const-random-real-variable-Finite-Probablity-Space x _ = x
+```


This can also have a separate page.

...e-probability-theory/expected-value-random-real-variables-finite-probability-spaces.lagda.md

Co-authored-by: Fredrik Bakke <[email protected]>

…ite-types.lagda.md Co-authored-by: Fredrik Bakke <[email protected]>

…-types.lagda.md Co-authored-by: Fredrik Bakke <[email protected]>

fredrik-bakke · 2025-11-06T12:55:45Z

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

malarbol added 2 commits October 24, 2025 04:10

finite probability spaces & random variables

992890f

constant random variables

d941a54

malarbol changed the title ~~Bases for finite probability theory~~ Basics of finite probability theory Oct 24, 2025

fix link

9df4d7b

Merge branch 'master' into probability-theory

b3cad75

fredrik-bakke added the finite-probability-theory label Oct 24, 2025

malarbol added 2 commits October 24, 2025 16:55

rename module finite-probability-theory

c826867

fix links

6f03269

format

68bfd70

fredrik-bakke reviewed Oct 24, 2025

View reviewed changes

src/probability-theory/measures-on-finite-types.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed Oct 24, 2025

View reviewed changes

src/probability-theory/measures-on-finite-types.lagda.md Outdated Show resolved Hide resolved

typo

e4e361a

lowasser reviewed Oct 24, 2025

View reviewed changes

src/finite-probability-theory/finite-probability-spaces.lagda.md Outdated Show resolved Hide resolved

lowasser reviewed Oct 24, 2025

View reviewed changes

malarbol added 5 commits October 24, 2025 18:34

rename measure -> distribution

380bb36

add references

424c0f8

fix link

58f9c47

zero-is-not-one-R

76ac71b

finite probability spaces are inhabited

1c306a6

malarbol commented Oct 24, 2025

View reviewed changes

src/finite-probability-theory/random-real-variables-finite-probability-spaces.lagda.md Outdated Show resolved Hide resolved

malarbol added 2 commits October 24, 2025 21:27

atomic random variables

d4082d6

fix name

aeb66d1

malarbol marked this pull request as ready for review October 24, 2025 20:04

malarbol and others added 2 commits October 24, 2025 22:15

Update references.bib

1538f5d

Co-authored-by: Fredrik Bakke <[email protected]>

rephrase non-empty consequence/hypothesis for finite probability spaces

883489e

fredrik-bakke reviewed Oct 24, 2025

View reviewed changes

src/finite-probability-theory/finite-probability-spaces.lagda.md Outdated Show resolved Hide resolved

re-rephrase

a6de932

fredrik-bakke reviewed Oct 24, 2025

View reviewed changes

Update src/finite-probability-theory/finite-probability-spaces.lagda.md

ea39ce4

Co-authored-by: Fredrik Bakke <[email protected]>