Bounded random variables

A typeclass for random variables f : Ω → ℝ bounded in [a, b] almost everywhere under a measure μ, plus measurability of f.

class ProbabilityTheory.BoundedRandomVariable {Ω : Type u_1} [MeasurableSpace Ω] (f : Ω → ℝ) (μ : MeasureTheory.Measure Ω) (a b : ℝ) : Prop

A random variable f : Ω → ℝ is bounded in [a, b] almost everywhere under μ, with f itself measurable.

• ae_mem_Icc : ∀ᵐ (ω : Ω) ∂μ, f ω ∈ Set.Icc a b
• measurable : Measurable f