congr — Mathlib

English

If Y and X have laws with respect to measures μ, P and ν respectively, and Y and X are independent with respect to P, then Y ∘ X has law ν with respect to P and μ.

Русский

Если Y и X имеют распределения по мерам μ, 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 congr {Y : Ω → 𝓧} (hX : HasLaw X μ P) (hY : Y =ᵐ[P] X) : HasLaw Y μ P
    where
  aemeasurable := hX.aemeasurable.congr hY.symm
  map_eq := by rw [map_congr hY, hX.map_eq]

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