Expected value of a uniformly distributed random variable

Stream: mathlib4

[Enrico Borba]

I'm trying to get my hands wet with probability in mathlib, but I'm having some issues. I'm trying to show that the expected value for a random variable X : Ω → ℝ is 1/2:

import Mathlib.Analysis.SpecialFunctions.Integrals
import Mathlib.Probability.Density
import Mathlib.Probability.Notation

open MeasureTheory ProbabilityTheory

variable {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)]
variable (X : Ω → ℝ) (hX : MeasureTheory.pdf.IsUniform X (Set.Icc 0 1) ℙ)

example : 𝔼[X] = 1 / 2 := by
  rw [MeasureTheory.pdf.IsUniform.integral_eq ?measurable ?nonempty ?top hX]
  case measurable => simp
  case top => simp
  case nonempty => simp
  simp
  /-
  Ω : Type u_1
  inst✝¹ : MeasureSpace Ω
  inst✝ : IsProbabilityMeasure ℙ
  X : Ω → ℝ
  hX : pdf.IsUniform X (Set.Icc 0 1) ℙ
  ⊢ ∫ (x : ℝ) in Set.Icc 0 1, x = 2⁻¹
  -/

Here I'm stuck showing that this integral has the value 1/2. A few things I noted:

• Looking around mathlib, it looks like interval integrals are defined on Set.Ioc instead of Set.Icc, and I'm unsure how to convert this integral to one like that in order to use the existing lemmas.
• Hovering over the integral itself in the tactics window, I see this:
  @integral ℝ ℝ Real.normedAddCommGroup InnerProductSpace.toNormedSpace MeasureSpace.toMeasurableSpace (Measure.restrict ℙ (Set.Icc 0 1)) fun x => x : ℝ. I'm confused why the measure ℙ is being referenced in this integral.

[Yury G. Kudryashov]

ℙ is a notation for volume in the ProbabilityTheory scope.

[Yury G. Kudryashov]

example : 𝔼[X] = 1 / 2 := by
  rw [hX.integral_eq, ← set_integral_congr_set_ae Ioc_ae_eq_Icc,
    ← intervalIntegral.integral_of_le zero_le_one]
  all_goals simp

[Enrico Borba]

Ah indeed it is, hovering over ℙ shows @volume ℝ Real.measureSpace : Measure ℝ

[Enrico Borba]

set_integral_congr_set_ae Ioc_ae_eq_Icc what an incantation

[Enrico Borba]

Makes a ton of sense, thanks a ton :)

[Yury G. Kudryashov]

In fact, some of the assumptions (e.g., μ s ≠ 0) in IsUniform.integral_eq are not needed at all. I'm going to drop them.

[Yury G. Kudryashov]

@Jason KY. :up: #10021

[Yury G. Kudryashov]

Also, please turn HasPDF into a structure with 3 fields, not one field with two ∧s.