covariance_fst_snd_prod — Mathlib

English

Let X ∈ L^2(μ) and Y ∈ L^2(ν). Then Cov[X, Y; μ×ν] = 0 for the product measure using X on the first coordinate and Y on the second.

Русский

Пусть X ∈ L^2(μ) и Y ∈ L^2(ν). Тогда ковариация Cov(X(·,1), Y(·,2)) по μ×ν равна нулю.

LaTeX

$$$\\operatorname{cov}[X, Y; \\mu \\times \\nu] = 0$$

Lean4

theorem covariance_fst_snd_prod (hfμ : MemLp X 2 μ) (hgν : MemLp Y 2 ν) :
    cov[fun p ↦ X p.1, fun p ↦ Y p.2; μ.prod ν] = 0 :=
  (indepFun_prod₀ hfμ.aemeasurable hgν.aemeasurable).covariance_eq_zero (hfμ.comp_fst ν) (hgν.comp_snd μ)

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