Theorems · Theorem · probability

ProbabilityTheory.HasLaw.covariance_fun_comp

∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.HasLaw X μ P →
    ∀ {f g : 𝓧 → ℝ},
      AEMeasurable f μ →
        AEMeasurable g μ →
          ProbabilityTheory.covariance (fun ω => f (X ω)) (fun ω => g (X ω)) P = ProbabilityTheory.covariance f g μ

Defined in

Mathlib.Probability.HasLaw

Cited by

1 results in Mathlib

Foundations

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