lintegral_comp — Mathlib

English

If X has a law with respect to μ and P, then the covariance of f(X) and g(X) with respect to P equals the covariance of f and g with respect to μ, for AEMeasurable f and g.

Русский

Если X имеет закон по отношению к μ и P, то ковариация f(X) и g(X) по P равна ковариации f и g по μ для AEMeasurable функций f, g.

LaTeX

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

Lean4

theorem lintegral_comp {X : Ω → 𝓧} (hX : HasLaw X μ P) {f : 𝓧 → ℝ≥0∞} (hf : AEMeasurable f μ) :
    ∫⁻ ω, f (X ω) ∂P = ∫⁻ x, f x ∂μ :=
  by
  rw [← hX.map_eq, lintegral_map' _ hX.aemeasurable]
  rwa [hX.map_eq]

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