English
Given a measurable set s, and kernels κ, η, the piecewise kernel agrees with κ on s and with η on its complement.
Русский
Дано измеримое множество s и ядра κ, η. Ядро piecewise совпадает с κ на s и с η на дополнении к s.
LaTeX
$$$\\text{piecewise}(s,\\kappa,\\eta) : \\alpha \\to \\beta \\quad\\text{ satisfies } (\\text{piecewise } s\\ \\kappa\\ \\eta)(a) = \\begin{cases} \\kappa(a) & a \\in s \\\\ \\eta(a) & a \\notin s \\end{cases}$$$
Lean4
/-- `ProbabilityTheory.Kernel.piecewise hs κ η` is the kernel equal to `κ` on the measurable set `s`
and to `η` on its complement. -/
def piecewise (hs : MeasurableSet s) (κ η : Kernel α β) : Kernel α β
where
toFun a := if a ∈ s then κ a else η a
measurable' := κ.measurable.piecewise hs η.measurable
