deterministic_parallelComp_deterministic

English

The parallel composition of deterministic kernels corresponds to the deterministic kernel induced by the product map.

Русский

Параллельная композиция детерминированных ядер эквивалентна детерминированному ядру, индуцируемому картой произведения.

LaTeX

$$$$\\text{deterministic }f hf \\; \\parallel_κ\\; \\text{deterministic }g hg = \\text{deterministic }(Prod.map f g) (hf.prodMap hg).$$$$

Lean4

theorem deterministic_parallelComp_deterministic {f : α → γ} {g : β → δ} (hf : Measurable f) (hg : Measurable g) :
    (deterministic f hf) ∥ₖ (deterministic g hg) = deterministic (Prod.map f g) (hf.prodMap hg) :=
  by
  ext x : 1
  simp_rw [parallelComp_apply, deterministic_apply, Prod.map, Measure.dirac_prod_dirac]

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