Measurable space of kernels

@[instance_reducible]

instance ProbabilityTheory.instMeasurableSpaceKernel {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} : MeasurableSpace (Kernel 𝓧 𝓨)

Equations

• ProbabilityTheory.instMeasurableSpaceKernel = MeasurableSpace.comap (fun (κ : ProbabilityTheory.Kernel 𝓧 𝓨) => ⇑κ) inferInstance

theorem ProbabilityTheory.measurable_kernel_iff {𝓧 : Type u_1} {𝓨 : Type u_2} {𝓩 : Type u_3} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {m𝓩 : MeasurableSpace 𝓩} (f : 𝓧 → Kernel 𝓨 𝓩) : Measurable f ↔ ∀ (y : 𝓨), Measurable fun (x : 𝓧) => (f x) y

theorem ProbabilityTheory.Kernel.measurable_const {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} : Measurable (const 𝓧)