noncomputable def ConditionalExpectation.condExp {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) (f : Ω → ℝ) : Ω → ℝ

The conditional expectation of f : Ω → ℝ given the sub-σ-algebra m, under the measure μ.

Following the textbook definition, given a probability space (Ω, m₀, μ), a sub-σ-field m ⊆ m₀, and a random variable f measurable w.r.t. m₀ with E|f| < ∞, the conditional expectation μ[f | m] is an m-measurable random variable Y such that ∫_A f dμ = ∫_A Y dμ for every A ∈ m.