dirac_unit_compProd_const — Mathlib

English

With unit Dirac and a constant kernel μ, the composition equals the pushforward by Prod.mk of μ.

Русский

При Dirac на единице и константном ядре μ композиция равна отображению μ через Prod.mk.

LaTeX

$$$\\mathrm{dirac (Unit)} ⊗_m (Kernel.const Unit μ) = μ.map (\\mathrm{Prod.mk} \\; Unit.unit)$$$

Lean4

theorem dirac_unit_compProd_const (μ : Measure β) [SFinite μ] :
    Measure.dirac () ⊗ₘ Kernel.const Unit μ = μ.map (Prod.mk ()) := by rw [dirac_unit_compProd, Kernel.const_apply]

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