integral_comp — Mathlib

English

If Y has law ν with respect to μ and X has law μ with respect to P, then the composition Y ∘ X has law ν with respect to P.

Русский

Если Y имеет закон ν относительно μ, а X имеет закон μ относительно P, то композиция Y ∘ X имеет закон ν относительно P.

LaTeX

$$$$ \\HasLaw Y\\; \\nu\\; \\mu \\; \\Rightarrow\\; \\HasLaw X\\; \\mu\\; P \\Rightarrow \\HasLaw (Y \\circ X)\\; \\nu\\; P $$$$

Lean4

theorem integral_comp {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : Ω → 𝓧} (hX : HasLaw X μ P) {f : 𝓧 → E}
    (hf : AEStronglyMeasurable f μ) : P[f ∘ X] = ∫ x, f x ∂μ :=
  by
  rw [← hX.map_eq, integral_map hX.aemeasurable, Function.comp_def]
  rwa [hX.map_eq]

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