Integral and Expectation

Stream: mathlib4

[Zhang Ruichong]

I'm trying to prove something trivial: The expectation of a random variable is its integral over the probability space.
My code is as follows:

import Mathlib.Tactic
import Mathlib.Probability.Notation
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
import Mathlib.MeasureTheory.MeasurableSpaceDef

open MeasureTheory ProbabilityTheory

variable {Ω : Type _} [MeasureSpace Ω] {μ : ProbabilityMeasure Ω}
variable {X : Ω → ℝ}
#check (∫ (a : Ω), X a)

lemma expectation_equals_integral (integrability: Integrable X μ): 𝔼[X] = (∫ (a : Ω), X a ∂μ) := by
  rw [integral]
  rw [integral]

and I get the state:

Ω: Type u_1
inst✝: MeasureSpace Ω
μ: ProbabilityMeasure Ω
X: Ω → ℝ
integrability: Integrable X
⊢ (if hf : Integrable fun a => X a then L1.integral (Integrable.toL1 (fun a => X a) hf) else 0) =
  if hf : Integrable fun a => X a then L1.integral (Integrable.toL1 (fun a => X a) hf) else 0

It's showing the same thing over both sides of the equality. However, I tried rfl but it couldn't close the goal.

[Damiano Testa]

I'm not at a computer now, but maybe using congr may zoom in on some hidden difference?

[Zhang Ruichong]

It is showing

Ω: Type u_1
inst✝: MeasureSpace Ω
μ: ProbabilityMeasure Ω
X: Ω → ℝ
integrability: Integrable X
⊢ ℙ = ↑μ
case h.e_3.e_1.e_μ
Ω: Type u_1
inst✝: MeasureSpace Ω
μ: ProbabilityMeasure Ω
X: Ω → ℝ
integrability: Integrable X
⊢ ℙ = ↑μ
case h.e_4
Ω: Type u_1
inst✝: MeasureSpace Ω
μ: ProbabilityMeasure Ω
X: Ω → ℝ
integrability: Integrable X
⊢ HEq (fun hf => L1.integral (Integrable.toL1 (fun a => X a) hf)) fun hf =>
  L1.integral (Integrable.toL1 (fun a => X a) hf)
case h.e_5
Ω: Type u_1
inst✝: MeasureSpace Ω
μ: ProbabilityMeasure Ω
X: Ω → ℝ
integrability: Integrable X
⊢ HEq (fun hf => 0) fun hf => 0

Does it mean that ℙ is the default probability measure?

[Damiano Testa]

Yes, I think that the two sides are using different measures.

[Damiano Testa]

(Note that I have not looked much at the probability part of mathlib, so maybe someone else can confirm!)

[Eric Wieser]

I assume there's an implicit measure argument somewhere in mathlib that probably ought to be explicit?

[Damiano Testa]

It seems that docs#MeasureTheory.MeasureSpace makes the choice of a measure for you: MeasureTheory.MeasureSpace.volume.

[Damiano Testa]

Maybe, using docs#MeasurableSpace, rather than docs#MeasureTheory.MeasureSpace is closer to what you want?

[Anatole Dedecker]

I'm not used to the probability theory library either so please correct me, but I think there are two ways to express your statement.

• If you want to have a default measure on Ω:

import Mathlib.Tactic
import Mathlib.Probability.Notation
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
import Mathlib.MeasureTheory.MeasurableSpaceDef

open MeasureTheory ProbabilityTheory

variable {Ω : Type _} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)]
variable {X : Ω → ℝ}

lemma expectation_equals_integral : 𝔼[X] = (∫ (a : Ω), X a) := rfl

• if not (especially if you want to make a generic lemma for the library):

import Mathlib.Tactic
import Mathlib.Probability.Notation
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
import Mathlib.MeasureTheory.MeasurableSpaceDef

open MeasureTheory ProbabilityTheory

variable {Ω : Type _} [MeasurableSpace Ω] (μ : Measure Ω := by volume_tac)
variable [IsProbabilityMeasure μ] {X : Ω → ℝ}

lemma expectation_equals_integral : μ[X] = (∫ (a : Ω), X a ∂μ) := rfl

[Anatole Dedecker]

I think ProbabilityMeasure should mostly be used when you care about the space of probability measures, otherwise you can just use IsProbabilityMeasure. @Kalle Kytölä does that sound right?

[Kalle Kytölä]

Anatole Dedecker said:

I think ProbabilityMeasure should mostly be used when you care about the space of probability measures, otherwise you can just use IsProbabilityMeasure. Kalle Kytölä does that sound right?

Yes!

What Anatole describes should be the right conservative way to use Measure, IsProbabilityMeasure, and ProbabilityMeasure. It should first of all not cause objections, and it probably makes things work better in practice, too. For example having (P : Measure Ω) [IsProbabilityMeasure P] will make using the whole measure theory library (including integrals) more straightforward, because then one doesn't need to coerce ProbabilityMeasure Ω → Measure Ω. (It is possible to do the coercions and use P : ProbabilityMeasure Ω instead, but one should only do this in some particular circumstances.)

The main thing that ProbabilityMeasure Ω has is the topology of convergence in distribution, so if you want to take limits of probability measures (for example limits of distributions of random variables), then you should work with ProbabilityMeasure. As a rule of thumb, otherwise not.