covariance_comp — Mathlib

English

If X has law μ and Y has law ν with respect to P and X ⟂⊥ Y under P, then the covariance of f(X) and g(X) equals the covariance of f and g under μ.

Русский

Если X имеет закон μ и Y имеет закон ν относительно P и X и Y независимы под P, ковариация f(X) и g(X) равна ковариации f и g по μ.

LaTeX

$$$$ \\operatorname{cov} [f \\circ X, g \\circ X; P] = \\operatorname{cov} [f, g; \\mu] $$$$

Lean4

theorem covariance_comp (hX : HasLaw X μ P) {f g : 𝓧 → ℝ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    cov[f ∘ X, g ∘ X; P] = cov[f, g; μ] := by
  rw [← hX.map_eq, covariance_map]
  · rw [hX.map_eq]
    exact hf.aestronglyMeasurable
  · rw [hX.map_eq]
    exact hg.aestronglyMeasurable
  · exact hX.aemeasurable

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