covariance_map — Mathlib

English

If X and Y are AEStronglyMeasurable with respect to μ.map Z and hZ is AEMeasurable, then Cov[X, Y; μ.map Z] equals Cov[X ∘ Z, Y ∘ Z; μ].

Русский

Пусть X и Y — AEStronglyMeasurable относительно μ.map Z, и hZ — AEMeasurable. Тогда Cov[X, Y; μ.map Z] = Cov[X ∘ Z, Y ∘ Z; μ].

LaTeX

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

Lean4

theorem covariance_map {Z : Ω' → Ω} (hX : AEStronglyMeasurable X (μ.map Z)) (hY : AEStronglyMeasurable Y (μ.map Z))
    (hZ : AEMeasurable Z μ) : cov[X, Y; μ.map Z] = cov[X ∘ Z, Y ∘ Z; μ] :=
  by
  simp_rw [covariance, Function.comp_apply]
  repeat rw [integral_map]
  any_goals assumption
  exact (hX.sub aestronglyMeasurable_const).mul (hY.sub aestronglyMeasurable_const)

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