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_self: 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_eq_sub {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance X Y μ = ∫ (x : Ω), (X * Y) x ∂μ - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y 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 μ

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

theorem ProbabilityTheory.covariance_mul_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (c : ℝ) : covariance X (fun (ω : Ω) => 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 μ

theorem ProbabilityTheory.covariance_sum_left' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ] (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance (∑ i ∈ s, X i) Y μ = ∑ i ∈ s, covariance (X i) Y μ

theorem ProbabilityTheory.covariance_sum_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance (∑ i : ι, X i) Y μ = ∑ i : ι, covariance (X i) Y μ

theorem ProbabilityTheory.covariance_fun_sum_left' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ] (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance (fun (ω : Ω) => ∑ i ∈ s, X i ω) Y μ = ∑ i ∈ s, covariance (X i) Y μ

theorem ProbabilityTheory.covariance_fun_sum_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance (fun (ω : Ω) => ∑ i : ι, X i ω) Y μ = ∑ i : ι, covariance (X i) Y μ

theorem ProbabilityTheory.covariance_sum_right' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ] (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance Y (∑ i ∈ s, X i) μ = ∑ i ∈ s, covariance Y (X i) μ

theorem ProbabilityTheory.covariance_sum_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance Y (∑ i : ι, X i) μ = ∑ i : ι, covariance Y (X i) μ

theorem ProbabilityTheory.covariance_fun_sum_right' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ] (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance Y (fun (ω : Ω) => ∑ i ∈ s, X i ω) μ = ∑ i ∈ s, covariance Y (X i) μ

theorem ProbabilityTheory.covariance_fun_sum_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance Y (fun (ω : Ω) => ∑ i : ι, X i ω) μ = ∑ i : ι, covariance Y (X i) μ

theorem ProbabilityTheory.covariance_sum_sum' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ] {ι' : Type u_3} {Y : ι' → Ω → ℝ} {t : Finset ι'} (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hY : ∀ i ∈ t, MeasureTheory.MemLp (Y i) 2 μ) : covariance (∑ i ∈ s, X i) (∑ j ∈ t, Y j) μ = ∑ i ∈ s, ∑ j ∈ t, covariance (X i) (Y j) μ

theorem ProbabilityTheory.covariance_sum_sum {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] {ι' : Type u_3} [Fintype ι'] {Y : ι' → Ω → ℝ} (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (hY : ∀ (i : ι'), MeasureTheory.MemLp (Y i) 2 μ) : covariance (∑ i : ι, X i) (∑ j : ι', Y j) μ = ∑ i : ι, ∑ j : ι', covariance (X i) (Y j) μ

theorem ProbabilityTheory.covariance_fun_sum_fun_sum' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ] {ι' : Type u_3} {Y : ι' → Ω → ℝ} {t : Finset ι'} (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hY : ∀ i ∈ t, MeasureTheory.MemLp (Y i) 2 μ) : covariance (fun (ω : Ω) => ∑ i ∈ s, X i ω) (fun (ω : Ω) => ∑ j ∈ t, Y j ω) μ = ∑ i ∈ s, ∑ j ∈ t, covariance (X i) (Y j) μ

theorem ProbabilityTheory.covariance_fun_sum_fun_sum {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] {ι' : Type u_3} [Fintype ι'] {Y : ι' → Ω → ℝ} (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (hY : ∀ (i : ι'), MeasureTheory.MemLp (Y i) 2 μ) : covariance (fun (ω : Ω) => ∑ i : ι, X i ω) (fun (ω : Ω) => ∑ j : ι', Y j ω) μ = ∑ i : ι, ∑ j : ι', covariance (X i) (Y j) μ

theorem ProbabilityTheory.covariance_map_equiv {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Ω' : Type u_2} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'} (X Y : Ω → ℝ) (Z : Ω' ≃ᵐ Ω) : covariance X Y (MeasureTheory.Measure.map (⇑Z) μ) = covariance (X ∘ ⇑Z) (Y ∘ ⇑Z) μ

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

theorem ProbabilityTheory.covariance_map_fun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {Ω' : Type u_2} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'} {Z : Ω' → Ω} (hX : MeasureTheory.AEStronglyMeasurable X (MeasureTheory.Measure.map Z μ)) (hY : MeasureTheory.AEStronglyMeasurable Y (MeasureTheory.Measure.map Z μ)) (hZ : AEMeasurable Z μ) : covariance X Y (MeasureTheory.Measure.map Z μ) = covariance (fun (ω : Ω') => X (Z ω)) (fun (ω : Ω') => Y (Z ω)) μ

theorem ProbabilityTheory.IndepFun.covariance_eq_zero {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : IndepFun X Y μ) (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : covariance X Y μ = 0