covariance_map_equiv — Mathlib

English

Let X, Y be random variables on Ω and Z a measure-preserving bijection between Ω' and Ω. Then Cov(X, Y; μ.map Z) equals Cov(X ∘ Z, Y ∘ Z; μ).

Русский

Пусть X, Y — случайные величины на Ω, Z — биекция между Ω' и Ω, меппирует меры μ так, что μ.map Z — новая мера. Тогда Cov(X, Y; μ.map Z) = Cov(X ∘ Z, Y ∘ Z; μ).

LaTeX

$$$\\operatorname{cov}_{\\mu\\map Z}\\left(X, Y\\right) = \\operatorname{cov}_{\\mu}\\left(X\\circ Z, Y\\circ Z\\right)$$$

Lean4

theorem covariance_map_equiv (X Y : Ω → ℝ) (Z : Ω' ≃ᵐ Ω) : cov[X, Y; μ.map Z] = cov[X ∘ Z, Y ∘ Z; μ] := by
  simp_rw [covariance, integral_map_equiv, Function.comp_apply]

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