comp — Mathlib

English

If η and κ are Markov kernels, then their composition η ∘ₖ κ is again a Markov kernel; in particular, it defines a probability measure after fixing the input.

Русский

Если η и κ — марковыe ядра, то их композиция η ∘ₖ κ снова является марковым ядром; она задаёт вероятность после фиксации входа.

LaTeX

$$$ (\eta \circ_K \kappa) \text{ is a Markov kernel}$$$

Lean4

instance comp (η : Kernel β γ) [IsMarkovKernel η] (κ : Kernel α β) [IsMarkovKernel κ] : IsMarkovKernel (η ∘ₖ κ) where
  isProbabilityMeasure
    a := by
    rw [comp_apply]
    constructor
    rw [Measure.bind_apply .univ η.aemeasurable]
    simp

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