Theorems · Theorem · probability

ProbabilityTheory.covariance_map

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {Ω' : Type u_2} {mΩ' : MeasurableSpace Ω'}
  {μ : MeasureTheory.Measure Ω'} {Z : Ω' → Ω},
  MeasureTheory.AEStronglyMeasurable X (MeasureTheory.Measure.map Z μ) →
    MeasureTheory.AEStronglyMeasurable Y (MeasureTheory.Measure.map Z μ) →
      AEMeasurable Z μ →
        ProbabilityTheory.covariance X Y (MeasureTheory.Measure.map Z μ) =
          ProbabilityTheory.covariance (X ∘ Z) (Y ∘ Z) μ

Defined in

Mathlib.Probability.Moments.Covariance

Cited by

5 results in Mathlib

Foundations

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