map — Mathlib

English

If f is not measurable, then the kernel map κ.map f is identically zero.

Русский

Если f не измерима, то ядро κ.map f равно нулю (всегда).

LaTeX

$$$$\\text{If } f \\text{ is not measurable, then } κ.map f = 0.$$$$

Lean4

/-- The pushforward of a kernel along a function.
If the function is not measurable, we use zero instead. This choice of junk
value ensures that typeclass inference can infer that the `map` of a kernel
satisfying `IsZeroOrMarkovKernel` again satisfies this property. -/
noncomputable def map [MeasurableSpace γ] (κ : Kernel α β) (f : β → γ) : Kernel α γ :=
  if hf : Measurable f then mapOfMeasurable κ f hf else 0

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