deterministic_prod_deterministic — Mathlib

English

The product of two deterministic kernels is deterministic: det f hf ×K det g hg = det (λ a, (f a, g a)) (hf.prodMk hg).

Русский

Произведение двух детерминированных ядер является детерминированным: det f hf ×K det g hg = det (λ a, (f a, g a)) (hf.prodMk hg).

LaTeX

$$$\\displaystyle (\\mathrm{deterministic} f hf \\times_K \\mathrm{deterministic} g hg) = \\mathrm{deterministic}(a \\mapsto (f a, g a))(hf.prodMk hg)$$$

Lean4

theorem deterministic_prod_deterministic {f : α → β} {g : α → γ} (hf : Measurable f) (hg : Measurable g) :
    deterministic f hf ×ₖ deterministic g hg = deterministic (fun a ↦ (f a, g a)) (hf.prodMk hg) := by ext;
  simp_rw [prod_apply, deterministic_apply, Measure.dirac_prod_dirac]

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