Covariance

We define the covariance of two real-valued random variables.

Main definitions

• covariance: covariance of two real-valued random variables, with notation cov[X, Y; μ]. cov[X, Y; μ] = ∫ ω, (X ω - μ[X]) * (Y ω - μ[Y]) ∂μ.

Main statements

• covariance_same: cov[X, X; μ] = Var[X; μ]

Notation

• cov[X, Y; μ] = covariance X Y μ
• cov[X, Y] = covariance X Y volume

noncomputable def ProbabilityTheory.covariance {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : ℝ

The covariance of two real-valued random variables defined as the integral of (X - 𝔼[X])(Y - 𝔼[Y]).

Equations

• ProbabilityTheory.covariance X Y μ = ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ

def ProbabilityTheory.«termCov[_,_;_]» : Lean.ParserDescr

The covariance of two real-valued random variables defined as the integral of (X - 𝔼[X])(Y - 𝔼[Y]).

Equations

• One or more equations did not get rendered due to their size.

def ProbabilityTheory.«termCov[_,_]» : Lean.ParserDescr

The covariance of the real-valued random variables X and Y according to the volume measure.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.covariance_same {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : AEMeasurable X μ) : covariance X X μ = variance X μ

@[simp]

theorem ProbabilityTheory.covariance_zero_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : covariance 0 Y μ = 0

@[simp]

theorem ProbabilityTheory.covariance_zero_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : covariance X 0 μ = 0

@[simp]

theorem ProbabilityTheory.covariance_zero_measure {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} : covariance X Y 0 = 0

theorem ProbabilityTheory.covariance_comm {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y : Ω → ℝ) {μ : MeasureTheory.Measure Ω} : covariance X Y μ = covariance Y X μ

@[simp]

theorem ProbabilityTheory.covariance_const_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (c : ℝ) : covariance (fun (x : Ω) => c) Y μ = 0

@[simp]

theorem ProbabilityTheory.covariance_const_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (c : ℝ) : covariance X (fun (x : Ω) => c) μ = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem ProbabilityTheory.covariance_add_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y Z : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) (hZ : MeasureTheory.MemLp Z 2 μ) : covariance (X + Y) Z μ = covariance X Z μ + covariance Y Z μ

theorem ProbabilityTheory.covariance_add_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y Z : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) (hZ : MeasureTheory.MemLp Z 2 μ) : covariance X (Y + Z) μ = covariance X Y μ + covariance X Z μ

theorem ProbabilityTheory.covariance_smul_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (c : ℝ) : covariance (c • X) Y μ = c * covariance X Y μ

theorem ProbabilityTheory.covariance_smul_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (c : ℝ) : covariance X (c • Y) μ = c * covariance X Y μ

@[simp]

theorem ProbabilityTheory.covariance_neg_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : covariance (-X) Y μ = -covariance X Y μ

@[simp]

theorem ProbabilityTheory.covariance_fun_neg_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : covariance (fun (ω : Ω) => -X ω) Y μ = -covariance X Y μ

@[simp]

theorem ProbabilityTheory.covariance_neg_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : covariance X (-Y) μ = -covariance X Y μ

@[simp]

theorem ProbabilityTheory.covariance_fun_neg_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : covariance X (fun (ω : Ω) => -Y ω) μ = -covariance X Y μ

theorem ProbabilityTheory.covariance_sub_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y Z : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) (hZ : MeasureTheory.MemLp Z 2 μ) : covariance (X - Y) Z μ = covariance X Z μ - covariance Y Z μ

theorem ProbabilityTheory.covariance_sub_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y Z : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) (hZ : MeasureTheory.MemLp Z 2 μ) : covariance X (Y - Z) μ = covariance X Y μ - covariance X Z μ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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