∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.MemLp X 2 μ → MeasureTheory.MemLp Y 2 μ → ProbabilityTheory.covariance X Y μ = 0