LeanPool.RlTheoryInLean.Probability.Kernel.Composition.MapComap

noncomputable def ProbabilityTheory.Kernel.comapLast {α : Type u_1} [MeasurableSpace α] (κ : Kernel α α) (n : ℕ) : Kernel (↥(Finset.Iic n) → α) α

Comap a kernel along the last coordinate of a finite trajectory prefix.

Equations

• κ.comapLast n = κ.comap (fun (history : ↥(Finset.Iic n) → α) => history ⟨n, ⋯⟩) ⋯

theorem ProbabilityTheory.Kernel.prodMap_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsMarkovKernel η] : (κ.prod η).map Prod.fst = κ

theorem ProbabilityTheory.Kernel.prodMap_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (κ : Kernel α β) [IsMarkovKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] : (κ.prod η).map Prod.snd = η