compProd

Mathlib.Probability.Kernel.Composition.MeasureCompProd

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.compProd

← MathLib Explorer

English

If μ is not finite in the sense SFinite, then μ ⊗ₘ κ = 0 for any kernel κ.

Русский

Если μ не SFinite, то μ ⊗ₘ κ = 0 для любого ядра κ.

LaTeX

$$$Not( SFinite(\\mu) ) \\Rightarrow \\mu \\otimes_{m} \\kappa = 0$$$

Lean4

/-- The composition-product of a measure and a kernel. -/
noncomputable def compProd (μ : Measure α) (κ : Kernel α β) : Measure (α × β) :=
  (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ()

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru