condKernelBorel — Mathlib

English

Same as above: fst κ ⊗ borelMarkovFromReal Ω η = κ under hη.

Русский

То же самое: при условии hη выполняется fst κ ⊗ borelMarkovFromReal Ω η = κ.

LaTeX

$$$fst\\,κ \\otimes_{ℓ} borelMarkovFromReal\\,Ω\\,η = κ$$$

Lean4

/-- Auxiliary definition for `ProbabilityTheory.Kernel.condKernel`.
A conditional kernel for `κ : Kernel α (γ × Ω)` where `γ` is countably generated and `Ω` is
standard Borel. -/
noncomputable def condKernelBorel (κ : Kernel α (γ × Ω)) [IsFiniteKernel κ] : Kernel (α × γ) Ω :=
  let κ' := map κ (Prod.map (id : γ → γ) (embeddingReal Ω))
  borelMarkovFromReal Ω (condKernelReal κ')

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