Kernels on a sigma type

Kernel.sigma κ is the kernel on Σ a, β a which is κ a on the fiber β a.

def ProbabilityTheory.Kernel.sigma {α : Type u_1} {γ : Type u_2} {β : α → Type u_3} [(a : α) → MeasurableSpace (β a)] {mγ : MeasurableSpace γ} (κ : (a : α) → Kernel (β a) γ) : Kernel ((a : α) × β a) γ

The kernel on Σ a, β a which is κ a on the fiber β a.

Equations

• ProbabilityTheory.Kernel.sigma κ = { toFun := fun (x : (a : α) × β a) => (κ x.fst) x.snd, measurable' := ⋯ }

@[simp]

theorem ProbabilityTheory.Kernel.sigma_apply {α : Type u_1} {γ : Type u_2} {β : α → Type u_3} [(a : α) → MeasurableSpace (β a)] {mγ : MeasurableSpace γ} (κ : (a : α) → Kernel (β a) γ) (x : (a : α) × β a) : (sigma κ) x = (κ x.fst) x.snd

theorem ProbabilityTheory.Kernel.sigma_apply_mk {α : Type u_1} {γ : Type u_2} {β : α → Type u_3} [(a : α) → MeasurableSpace (β a)] {mγ : MeasurableSpace γ} (κ : (a : α) → Kernel (β a) γ) (a : α) (b : β a) : (sigma κ) ⟨a, b⟩ = (κ a) b

theorem ProbabilityTheory.Kernel.comap_sigma_mk {α : Type u_1} {γ : Type u_2} {β : α → Type u_3} [(a : α) → MeasurableSpace (β a)] {mγ : MeasurableSpace γ} (κ : (a : α) → Kernel (β a) γ) (a : α) : (sigma κ).comap (Sigma.mk a) ⋯ = κ a

instance ProbabilityTheory.Kernel.instIsMarkovKernelSigmaSigma {α : Type u_1} {γ : Type u_2} {β : α → Type u_3} [(a : α) → MeasurableSpace (β a)] {mγ : MeasurableSpace γ} (κ : (a : α) → Kernel (β a) γ) [∀ (a : α), IsMarkovKernel (κ a)] : IsMarkovKernel (sigma κ)