∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ},
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.IndepFun X Y μ →
        ProbabilityTheory.variance (X + Y) μ = ProbabilityTheory.variance X μ + ProbabilityTheory.variance Y μ