covariance — Mathlib

English

The covariance of two real-valued random variables X and Y with respect to μ is defined as the integral of (X − E[X])(Y − E[Y]).

Русский

Ковариация двух вещественных случайных величин X и Y по μ задается интегралом (X − E[X])(Y − E[Y]).

LaTeX

$$$\\mathrm{cov}(X,Y;\\mu) = \\int (X(\\omega) - \\mu[X])(Y(\\omega) - \\mu[Y]) \\, d\\mu(\\omega)$$$

Lean4

/-- The covariance of two real-valued random variables defined as
the integral of `(X - 𝔼[X])(Y - 𝔼[Y])`. -/
noncomputable def covariance (X Y : Ω → ℝ) (μ : Measure Ω) : ℝ :=
  ∫ ω, (X ω - μ[X]) * (Y ω - μ[Y]) ∂μ

Похожие утверждения