basic discrete probability

Stream: new members

[JK]

I would like to play around with discrete probability in Lean, but am having trouble finding basic references with examples. (I have seen this and this, but would really like to avoid any mention of measure theory and prefer some examples.)

Could someone provide examples of how I would (i) define a variable X with the uniform distribution over {0, 1}, (ii) prove that X and 1 - X have the same distribution, and (iii) prove that if X and X' are each independently uniform over {0, 1} then Pr[X + X' = 1] = 1/2?

[Lawrence Wu (llllvvuu)]

You can use docs#Finset.dens

import Mathlib

variable {α β : Type*} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β]

abbrev RandomVariable (α β) := α → β

abbrev Event (β) := Finset β

abbrev Pr (X : RandomVariable α β) (S : Event β) := (Finset.univ.filter (X · ∈ S)).dens

abbrev X : RandomVariable (Fin 2) (Fin 2) := id

#eval Pr X {}
#eval Pr X {0}
#eval Pr X {1}
#eval Pr X {0, 1}

abbrev one_minus_X : RandomVariable (Fin 2) (Fin 2) := (1 - ·) ∘ X

#eval Pr one_minus_X {}
#eval Pr one_minus_X {0}
#eval Pr one_minus_X {1}
#eval Pr one_minus_X {0, 1}

example : Pr X = Pr one_minus_X := funext (by decide +kernel)

abbrev X' : RandomVariable (Fin 2) (Fin 2) := id

abbrev X_add_X' : RandomVariable (Fin 2 × Fin 2) (Fin 3) := fun (a, b) => ⟨(X a).1 + (X' b).1, by grind⟩

#eval Pr X_add_X' {0}
#eval Pr X_add_X' {1}
#eval Pr X_add_X' {2}

example : Pr X_add_X' {1} = 1 / 2 := by decide +kernel

[JK]

Thanks.

I am conceptually confused about the definition of a RandomVariable. I would have thought to define a general random variable on {0, 1} as a function from Finset 2 to the non-negative reals that sums to 1 (i.e., as a PMF). Can you explain the intuition behind it?

[Lawrence Wu (llllvvuu)]

My code does define the PMF Pr X : Fin 2 -> Rat. But it is a derived quantity; that is, derived from the uniform probability measure implied by Finset.dens. Defining RVs and PMFs as originating from a sample space instead of just starting from a PMF makes more complex things easier to model.

[David Ledvinka]

FYI there is not too much support for this directly using Mathlib because Mathlib focuses on generality and most theorems about discrete probability theory have more general analogues. Similar to how its hard to do analysis in the way one would see in an undergraduate analysis textbook using Mathlib. Therefore if you want to do this now you could follow the approach Lawrence used and develop discrete probability separately, or you could write your own API that specializes the Mathlib definitions and theorems to the discrete case.

[Etienne Marion]

JK said:

Thanks.

I am conceptually confused about the definition of a RandomVariable. I would have thought to define a general random variable on {0, 1} as a function from Finset 2 to the non-negative reals that sums to 1 (i.e., as a PMF). Can you explain the intuition behind it?

A PMF will not give you a random variable, it gives you a measure.

[JK]

I must be mis-understanding something here, since #eval Pr X {1} gives the same result as #eval Pr X {2}.

[Bolton Bailey]

docs#PMF is in mathlib - this is a way of defining things in the form of a function as OP describes.

[JK]

Why does #eval Pr X {2} return 1/2?

[Bolton Bailey]

Well if X is the uniform distribution on {1,2} then it has a 1/2 chance of ending up on 2 (maybe I don't get your question)

[JK]

I thought X is the uniform distribution on {0, 1}. But

import Mathlib
variable {α β : Type*} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β]

abbrev RandomVariable (α β) := α → β

abbrev Event (β) := Finset β

abbrev Pr (X : RandomVariable α β) (S : Event β) := (Finset.univ.filter (X · ∈ S)).dens

abbrev X : RandomVariable (Fin 2) (Fin 2) := id

#eval Pr X {0}
#eval Pr X {1}
#eval Pr X {2}

all return 1/2

[Bolton Bailey]

Ah, I understand. The issue is that 2=0 in Fin 2

[JK]

ok, fair enough

[Bolton Bailey]

So I guess I should say that X is the uniform distribution on {0,1}, where 0 and 1 are elements of Fin 2

[JK]

I get a warning saying that grind should be avoided, and an error saying that grind fails, on

import Mathlib

variable {α β : Type*} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β]

abbrev RandomVariable (α β) := α → β

abbrev X : RandomVariable (Fin 2) (Fin 2) := id
abbrev X' : RandomVariable (Fin 2) (Fin 2) := id

abbrev X_add_X' : RandomVariable (Fin 2 × Fin 2) (Fin 3) :=
  fun (a, b) => ⟨(X a).1 + (X' b).1, by grind⟩

[Lawrence Wu (llllvvuu)]

Likely you have an outdated mathlib