∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : Ω → ℝ},
  ProbabilityTheory.HasGaussianLaw (fun ω => (X ω, Y ω)) P →
    ProbabilityTheory.covariance X Y P = 0 → ProbabilityTheory.IndepFun X Y P