Basic deterministic kernels

noncomputable def ProbabilityTheory.Kernel.id {α : Type u_1} {mα : MeasurableSpace α} : ProbabilityTheory.Kernel α α

The identity kernel.

Equations

• ProbabilityTheory.Kernel.id = ProbabilityTheory.Kernel.deterministic id ⋯

instance ProbabilityTheory.Kernel.instIsMarkovKernelId {α : Type u_1} {mα : MeasurableSpace α} : ProbabilityTheory.IsMarkovKernel ProbabilityTheory.Kernel.id

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.Kernel.id_apply {α : Type u_1} {mα : MeasurableSpace α} (a : α) : ProbabilityTheory.Kernel.id a = MeasureTheory.Measure.dirac a

noncomputable def ProbabilityTheory.Kernel.copy (α : Type u_3) [MeasurableSpace α] : ProbabilityTheory.Kernel α (α × α)

The deterministic kernel that maps x : α to the Dirac measure at (x, x) : α × α.

Equations

• ProbabilityTheory.Kernel.copy α = ProbabilityTheory.Kernel.deterministic (fun (x : α) => (x, x)) ⋯

instance ProbabilityTheory.Kernel.instIsMarkovKernelProdCopy {α : Type u_1} {mα : MeasurableSpace α} : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.copy α)

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.Kernel.copy_apply {α : Type u_1} {mα : MeasurableSpace α} (a : α) : (ProbabilityTheory.Kernel.copy α) a = MeasureTheory.Measure.dirac (a, a)

noncomputable def ProbabilityTheory.Kernel.discard (α : Type u_3) [MeasurableSpace α] : ProbabilityTheory.Kernel α Unit

The Markov kernel to the Unit type.

Equations

• ProbabilityTheory.Kernel.discard α = ProbabilityTheory.Kernel.deterministic (fun (x : α) => ()) ⋯

instance ProbabilityTheory.Kernel.instIsMarkovKernelUnitDiscard {α : Type u_1} {mα : MeasurableSpace α} : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.discard α)

Equations

• ⋯ = ⋯

@[simp]

theorem ProbabilityTheory.Kernel.discard_apply {α : Type u_1} {mα : MeasurableSpace α} (a : α) : (ProbabilityTheory.Kernel.discard α) a = MeasureTheory.Measure.dirac ()

@[simp]

theorem MeasureTheory.Measure.comp_discard {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) : μ.bind ⇑(ProbabilityTheory.Kernel.discard α) = μ Set.univ • MeasureTheory.Measure.dirac ()

noncomputable def ProbabilityTheory.Kernel.swap (α : Type u_3) (β : Type u_4) [MeasurableSpace α] [MeasurableSpace β] : ProbabilityTheory.Kernel (α × β) (β × α)

The deterministic kernel that maps (x, y) to the Dirac measure at (y, x).

Equations

• ProbabilityTheory.Kernel.swap α β = ProbabilityTheory.Kernel.deterministic Prod.swap ⋯

instance ProbabilityTheory.Kernel.instIsMarkovKernelProdSwap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.swap α β)

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.Kernel.swap_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (ab : α × β) : (ProbabilityTheory.Kernel.swap α β) ab = MeasureTheory.Measure.dirac ab.swap

theorem ProbabilityTheory.Kernel.swap_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (ab : α × β) {s : Set (β × α)} (hs : MeasurableSet s) : ((ProbabilityTheory.Kernel.swap α β) ab) s = s.indicator 1 ab.swap