theorem ProbabilityTheory.Kernel.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α β) {f : β → γ} (hf : Measurable f) {g : γ → δ} (hg : Measurable g) : (κ.map f).map g = κ.map (g ∘ f)

theorem ProbabilityTheory.Kernel.map_swapRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ)) {f : γ × β → δ} : κ.swapRight.map f = κ.map (f ∘ Prod.swap)

noncomputable def ProbabilityTheory.Kernel.deleteMiddle {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) : Kernel α (β × δ)

Given a kernel taking values in a product of three spaces, forget the middle one.

Equations

• κ.deleteMiddle = κ.mapOfMeasurable (fun (p : β × γ × δ) => (p.1, p.2.2)) ⋯

theorem ProbabilityTheory.Kernel.deleteMiddle_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) : κ.deleteMiddle = κ.map fun (p : β × γ × δ) => (p.1, p.2.2)

instance ProbabilityTheory.Kernel.instIsMarkovKernelProdDeleteMiddle {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) [IsMarkovKernel κ] : IsMarkovKernel κ.deleteMiddle

instance ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelProdDeleteMiddle {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel κ.deleteMiddle

@[simp]

theorem ProbabilityTheory.Kernel.fst_deleteMiddle {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) : κ.deleteMiddle.fst = κ.fst

@[simp]

theorem ProbabilityTheory.Kernel.snd_deleteMiddle {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) : κ.deleteMiddle.snd = κ.snd.snd

@[simp]

theorem ProbabilityTheory.Kernel.deleteMiddle_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] : deleteMiddle 0 = 0

@[simp]

theorem ProbabilityTheory.Kernel.deleteMiddle_map_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} {x✝³ : MeasurableSpace ε} [MeasurableSpace γ] (κ : Kernel α β) {f : β → γ} {g : β → δ} {g' : β → ε} (hg : Measurable g) : (κ.map fun (b : β) => (f b, g b, g' b)).deleteMiddle = κ.map fun (b : β) => (f b, g' b)

@[simp]

theorem ProbabilityTheory.Kernel.deleteMiddle_compProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (ξ : Kernel α β) [IsSFiniteKernel ξ] (κ : Kernel (α × β) (γ × δ)) [IsSFiniteKernel κ] : (ξ.compProd κ).deleteMiddle = ξ.compProd κ.snd

noncomputable def ProbabilityTheory.Kernel.deleteRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) : Kernel α (β × γ)

Given a kernel taking values in a product of three spaces, forget the last variable.

Equations

• κ.deleteRight = κ.mapOfMeasurable (fun (p : β × γ × δ) => (p.1, p.2.1)) ⋯

theorem ProbabilityTheory.Kernel.deleteRight_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) : κ.deleteRight = κ.map fun (p : β × γ × δ) => (p.1, p.2.1)

@[simp]

theorem ProbabilityTheory.Kernel.deleteRight_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] : deleteRight 0 = 0

instance ProbabilityTheory.Kernel.instIsMarkovKernelProdDeleteRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) [IsMarkovKernel κ] : IsMarkovKernel κ.deleteRight

instance ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelProdDeleteRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel κ.deleteRight

@[simp]

theorem ProbabilityTheory.Kernel.fst_deleteRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) : κ.deleteRight.fst = κ.fst

@[simp]

theorem ProbabilityTheory.Kernel.snd_deleteRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) : κ.deleteRight.snd = κ.snd.fst

@[simp]

theorem ProbabilityTheory.Kernel.deleteRight_map_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} {x✝³ : MeasurableSpace ε} [MeasurableSpace γ] (κ : Kernel α β) {f : β → γ} {g : β → δ} {g' : β → ε} (hg' : Measurable g') : (κ.map fun (b : β) => (f b, g b, g' b)).deleteRight = κ.map fun (b : β) => (f b, g b)

noncomputable def ProbabilityTheory.Kernel.reverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) : Kernel α (δ × γ × β)

Given a kernel taking values in a product of three spaces, reverse the order of the spaces.

Equations

• κ.reverse = κ.mapOfMeasurable (fun (p : β × γ × δ) => (p.2.2, p.2.1, p.1)) ⋯

theorem ProbabilityTheory.Kernel.reverse_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) : κ.reverse = κ.map fun (p : β × γ × δ) => (p.2.2, p.2.1, p.1)

theorem ProbabilityTheory.Kernel.reverse_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] : reverse 0 = 0

@[simp]

theorem ProbabilityTheory.Kernel.reverse_reverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) : κ.reverse.reverse = κ

instance ProbabilityTheory.Kernel.instIsMarkovKernelProdReverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) [IsMarkovKernel κ] : IsMarkovKernel κ.reverse

instance ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelProdReverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel κ.reverse

@[simp]

theorem ProbabilityTheory.Kernel.swapRight_deleteMiddle_reverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) : κ.reverse.deleteMiddle.swapRight = κ.deleteMiddle

@[simp]

theorem ProbabilityTheory.Kernel.swapRight_snd_reverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) : κ.reverse.snd.swapRight = κ.deleteRight

@[simp]

theorem ProbabilityTheory.Kernel.swapRight_deleteRight_reverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace δ} [MeasurableSpace γ] (κ : Kernel α (β × γ × δ)) : κ.reverse.deleteRight.swapRight = κ.snd

theorem ProbabilityTheory.Kernel.FiniteKernelSupport.reverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {T : Type u_8} [MeasurableSpace T] [MeasurableSpace γ] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [MeasurableSingletonClass γ] {κ : Kernel T (α × β × γ)} (hκ : κ.FiniteKernelSupport) : κ.reverse.FiniteKernelSupport

Reversing preserves finite kernel support

theorem ProbabilityTheory.Kernel.AEFiniteKernelSupport.reverse {β : Type u_2} {γ : Type u_3} {x✝ : MeasurableSpace β} {S : Type u_7} {T : Type u_8} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace γ] [MeasurableSingletonClass S] [MeasurableSingletonClass β] [MeasurableSingletonClass γ] {κ : Kernel T (S × β × γ)} {μ : MeasureTheory.Measure T} (hκ : κ.AEFiniteKernelSupport μ) : κ.reverse.AEFiniteKernelSupport μ