Theorems · Theorem · probability

ProbabilityTheory.covariance_fst_snd_prod

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_2} {mΩ' : MeasurableSpace Ω'}
  {ν : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν]
  {X : Ω → ℝ} {Y : Ω' → ℝ},
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 ν → ProbabilityTheory.covariance (fun p => X p.1) (fun p => Y p.2) (μ.prod ν) = 0

Defined in

Mathlib.Probability.Moments.Covariance

Cited by

0 results in Mathlib

Foundations

Depth 272 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.IsProbabilityMeasureMeasureTheory.IsProbabilityMeasure