prod_apply — Mathlib

English

The product kernel (κ ×ₖ η) evaluated at a equals the product of the marginal measures κ a and η a.

Русский

Ядро произведения (κ ×ₖ η) на a равно произведению мер κ a и η a.

LaTeX

$$$$(κ ×ₖ η) a = (κ a) .prod (η a).$$$$

Lean4

theorem prod_apply (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] (a : α) :
    (κ ×ₖ η) a = (κ a).prod (η a) := by
  ext s hs
  rw [prod_apply' _ _ _ hs, Measure.prod_apply hs]

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