Theorems · Theorem · probability

ProbabilityTheory.covariance_add_const_left

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Integrable X μ →
    ∀ (c : ℝ), ProbabilityTheory.covariance (fun ω => X ω + c) Y μ = ProbabilityTheory.covariance X Y μ

Defined in

Mathlib.Probability.Moments.Covariance

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasure