parallelComp_apply_prod — Mathlib

English

Let κ and η be s-finite kernels. For s ⊆ β and t ⊆ δ, the parallel composition evaluated at x = (x1, x2) on the product set s × t equals the product of the marginals: (κ x1 s) · (η x2 t).

Русский

Пусть κ и η — s-конечные ядра. Для любые подмножества s ⊆ β и t ⊆ δ, значение на произведении множеств s × t равно произведению маргинальных масс: (κ x1 s) · (η x2 t).

LaTeX

$$$$(κ ∥ₖ η) x (s \\times t) = (κ x.1 s) \\cdot (η x.2 t),$$$$

Lean4

theorem parallelComp_apply_prod [IsSFiniteKernel κ] [IsSFiniteKernel η] (s : Set β) (t : Set δ) :
    (κ ∥ₖ η) x (s ×ˢ t) = (κ x.1 s) * (η x.2 t) := by rw [parallelComp_apply, Measure.prod_prod]

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