compProd_apply_univ — Mathlib

English

If μ is S-finite and κ is a Markov kernel, then the total mass is preserved: the measure of the whole space under μ ⊗ₘ κ equals μ of the whole space.

Русский

Если μ — S-финитная мерa и κ — марковское ядро, тогда полная масса сохраняется: μ ⊗ₘ κ(α × β) = μ(α).

LaTeX

$$$[\\mathrm{SFinite}\\; μ] \\; [\\mathrm{IsMarkovKernel}\\; κ] \\Rightarrow (μ ⊗ₘ κ)\\, \\mathrm{univ} = μ\\, \\mathrm{univ}$$$

Lean4

@[simp]
theorem compProd_apply_univ [SFinite μ] [IsMarkovKernel κ] : (μ ⊗ₘ κ) univ = μ univ := by simp [compProd]

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