∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {hm : m ≤ m₀} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [inst : MeasureTheory.SigmaFinite (μ.trim hm)],
  ProbabilityTheory.condVar m X μ =
    if MeasureTheory.Integrable (fun ω => (X ω - μ[X | m] ω) ^ 2) μ then
      if MeasureTheory.StronglyMeasurable fun ω => (X ω - μ[X | m] ω) ^ 2 then fun ω => (X ω - μ[X | m] ω) ^ 2
      else MeasureTheory.AEStronglyMeasurable.mk ↑↑(MeasureTheory.condExpL1 hm μ fun ω => (X ω - μ[X | m] ω) ^ 2) ⋯
    else 0