From Pmf to Expectations

Stream: mathlib4

[Joachim Breitner]

I defined the Pmf for binominal distributions:

def binominal (p : ENNReal) (h : p ≤ 1) (n : ℕ) : Pmf (Fin (n + 1)) :=
  .ofFintype (fun i => p^(i : ℕ) * (1-p)^(n - (i : ℕ)) * (n.choose i : ℕ)) (by
  …
  )

Now I want to do some calculations about $E[f(X)]$ where $X$ is binominally distributed, and I am trying to find my way around the library. It seems that expected values are written using integral and require a Measure, and I saw that I can turn a Pmf into a measure, so I tried

def E p h n (f : Fin (n + 1) → ℝ) :=
  ∫ i, (f i) ∂((binominal p h n).toMeasure)

but that gives me

failed to synthesize instance
  MeasurableSpace (Fin (n + 1))

Am I approaching this the wrong way? If not, will this way lead me to a formula involving a finite ∑ somehow?
(I could just state stuff explicitly as a finite sum, without connecting to the existing infrastructure for probability theory, but that doesn't seem nice.)

[Joachim Breitner]

It works for Pmf.bernoulli, which is already in mathlib:

import Mathlib.Probability.ProbabilityMassFunction.Constructions
import Mathlib.Probability.Notation
noncomputable
def E p h (f : Bool → ℝ) :=
  ∫ i, (f i) ∂((Pmf.bernoulli p h).toMeasure)

And it’s because there is a MeasurableSpace Bool instance. So should there simply be Measurablespace (Fin (n+1)) instances?

[Joachim Breitner]

Indeed, writing

instance Fin.instMeasurableSpace n : MeasurableSpace (Fin n) :=
  .comap  Fin.val Nat.instMeasurableSpace

make the definition go through. Is that something that should be in Mathlib.MeasureTheory.MeasurableSpace (e.g. as in mathlib4#6431)?

[Joachim Breitner]

Ah, there is lintegral_fintype to prove ∫⁻ (x : α), f x ∂μ = ∑x, f x * ↑↑μ {x}. But no such lemma for ∫ (x : α), f x ∂μ it seems.

[Joachim Breitner]

And for integral the answer is probably “it’s just not done yet”, so I started porting some of the lintegral API to integral at https://github.com/leanprover-community/mathlib4/pull/6446

Once this is in, I can combine it with a pmf.ToMeasure {x} = pmf x, and after some shuffling of .toReal I’ll be able to related E[f(X)] for a binomial X to the explicit finite sum formula

[Bjørn Kjos-Hanssen]

@Joachim Breitner Is the expectation of a binomial random variable already in Mathlib at this point?

[Jeremy Tan]

Not that I know of – only the exponential and normal distributions have landed at this point

[Bjørn Kjos-Hanssen]

@Jeremy Tan It looks like there is PMF.bernoulli on the measure space Bool and then there is PMF.binomial on the measure space Fin (n+1). But I don't see a binomial on Fin n → Bool, which would be the most natural way to get the expectation as the expectation of a sum.

[Rémy Degenne]

Joachim Breitner said:

Ah, there is lintegral_fintype to prove ∫⁻ (x : α), f x ∂μ = ∑x, f x * ↑↑μ {x}. But no such lemma for ∫ (x : α), f x ∂μ it seems.

There is docs#MeasureTheory.integral_fintype .

[Joachim Breitner]

Now there is docs#MeasureTheory.integral_fintype :-)

I think the expectation of a binomial was the next thing I would have done had I had time to continue that project, but then didn’t get to it. So go for it!

[Rémy Degenne]

Sorry, I did not see the date on those first messages :)

[Rémy Degenne]

Thanks for adding it!

[Rémy Degenne]

We use it a lot in the PFR project

[Yaël Dillies]

Bjørn Kjos-Hanssen said:

It looks like there is PMF.bernoulli on the measure space Bool

From having tried using it, I want to change it to be Prop-valued.

[Rémy Degenne]

And I want to be able to take an average of Bernoulli random variables, so I want something that can be coerced to 0 and 1 in Q. We might need several versions for different purposes.