covariance_map_fun — Mathlib

English

Let X, Y be random processes and Z a measure-preserving map; then Cov[X, Y; μ.map Z] equals Cov[X ∘ Z, Y ∘ Z; μ].

Русский

Пусть X, Y — случайные процессы, Z — отображение меры, сохраняющее массу; тогда ковариация после отображения равна ковариации после композиции с Z.

LaTeX

$$$\\operatorname{cov}\\bigl[X, Y; \\mu\\map Z\\bigr] = \\operatorname{cov}\\bigl[X\\circ Z, Y\\circ Z; \\mu\\bigr]$$$

Lean4

theorem covariance_map_fun {Z : Ω' → Ω} (hX : AEStronglyMeasurable X (μ.map Z)) (hY : AEStronglyMeasurable Y (μ.map Z))
    (hZ : AEMeasurable Z μ) : cov[X, Y; μ.map Z] = cov[fun ω ↦ X (Z ω), fun ω ↦ Y (Z ω); μ] :=
  covariance_map hX hY hZ

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