compProd_const — Mathlib

English

The composition product of μ with a constant kernel κ is the ordinary product measure μ.prod ν.

Русский

compProd μ с константным ядром κ даёт обычное произведение мер μ.prod ν.

LaTeX

$$$\\[μ : \\mathrm{Measure}\\; \\alpha\\], [ν : \\mathrm{Measure}\\; \\beta], [\\mathrm{SFinite}\\; μ] [\\mathrm{SFinite}\\; ν] : μ ⊗ₘ (\\mathrm Kernel.const α ν) = μ.prod ν$$$

Lean4

/-- The composition product of a measure and a constant kernel is the product between the two
measures. -/
@[simp]
theorem compProd_const {ν : Measure β} [SFinite μ] [SFinite ν] : μ ⊗ₘ (Kernel.const α ν) = μ.prod ν :=
  by
  ext s hs
  simp_rw [compProd_apply hs, prod_apply hs, Kernel.const_apply]

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