covariance_fun_comp — Mathlib

English

For HasLaw X μ P, and X mapping to a normed space E, the integral of X with respect to μ equals the integral of X with respect to P mapped by the appropriate measurable structure.

Русский

Для HasLaw X μ P и отображения X в нормированное пространство E выполняется тождество интегралов между μ и P через отображение X.

LaTeX

$$$$ \\int x \\, dP = \\int x \\, d\\mu $$$$

Lean4

theorem covariance_fun_comp (hX : HasLaw X μ P) {f g : 𝓧 → ℝ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    cov[fun ω ↦ f (X ω), fun ω ↦ g (X ω); P] = cov[f, g; μ] :=
  hX.covariance_comp hf hg

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