compProd_deterministic — Mathlib

English

For μ finite and f : α → β measurable, μ ⊗ₘ Kernel.deterministic f hf = μ.map (a ↦ (a, f a)).

Русский

Для конечной μ и детерминированного ядра f, μ ⊗ f = μ.map (a ↦ (a, f(a))).

LaTeX

$$$[SFinite(\\mu)] \\;{f : α \\to β} \\; (hf : Measurable f) : \\mu \\otimes_{m} \\mathrm{Kernel.deterministic}(f, hf) = \\mu.map (\\lambda a. (a, f a))$$$

Lean4

theorem compProd_deterministic [SFinite μ] {f : α → β} (hf : Measurable f) :
    μ ⊗ₘ Kernel.deterministic f hf = μ.map (fun a ↦ (a, f a)) :=
  by
  rw [compProd_eq_comp_prod, Kernel.id, Kernel.deterministic_prod_deterministic, deterministic_comp_eq_map]
  rfl

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