prodAssoc_prod — Mathlib

English

Associativity of kernel product up to a measurable equivalence: ((κ ×ξ) ×η) ≈ κ × (ξ × η) via prodAssoc.

Русский

Ассоциативность произведения ядер до измеримого эквивалентности: ((κ × ξ) × η) через prodAssoc эквивалентно κ × (ξ × η).

LaTeX

$$$\\displaystyle ((\\kappa \\times_K \\xi) \\times_K \\eta)^{\\phantom{}} \\! = \\text{kernel}_{prodAssoc}(κ, ξ, η) \\; \\text{ maps to } κ ×_K (ξ ×_K η)$$$

Lean4

theorem prodAssoc_prod (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] (ξ : Kernel α δ)
    [IsSFiniteKernel ξ] : ((κ ×ₖ ξ) ×ₖ η).map MeasurableEquiv.prodAssoc = κ ×ₖ (ξ ×ₖ η) :=
  by
  ext1 a
  rw [map_apply _ (by fun_prop), prod_apply, prod_apply, Measure.prodAssoc_prod, prod_apply, prod_apply]

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