copy — Mathlib

English

There is a deterministic kernel that sends x to the Dirac measure at (x, x) in α × α.

Русский

Существует детерминированное ядро, которое отправляет x в меру Дирака, концентрированную в (x, x) ∈ α × α.

LaTeX

$$$(\text{copy }\alpha)(a) = \delta_{(a,a)}$$$

Lean4

/-- The deterministic kernel that maps `x : α` to the Dirac measure at `(x, x) : α × α`. -/
noncomputable def copy (α : Type*) [MeasurableSpace α] : Kernel α (α × α) :=
  Kernel.deterministic (fun x ↦ (x, x)) (measurable_id.prod measurable_id)

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