∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.AEStronglyMeasurable X μ →
    ∀ (c : ℝ), ProbabilityTheory.variance (fun ω => X ω - c) μ = ProbabilityTheory.variance X μ