Theorems · Definition · probability

ProbabilityTheory.condVar

{Ω : Type u_1} → {m₀ : MeasurableSpace Ω} → MeasurableSpace Ω → (Ω → ℝ) → MeasureTheory.Measure Ω → Ω → ℝ

Conditional variance of a real-valued random variable. It is defined as 0 if any one of the following conditions is true: - m is not a sub-σ-algebra of m₀, - μ is not σ-finite with respect to m, - X - μ[X | m] is not square-integrable.

Defined in

Mathlib.Probability.CondVar

Cited by

21 results in Mathlib

Foundations

Depth 294 from the axioms · uses propext, Classical.choice, Quot.sound