theorem ProbabilityTheory.Kernel.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α β) {f : β → γ}, Measurable f → ∀ {g : γ → δ}, 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_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α (β × γ)) {f : γ × β → δ}, κ.swapRight.map f = κ.map (f ∘ Prod.swap)

@[simp]

theorem ProbabilityTheory.Kernel.swapLeft_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} [inst : MeasurableSpace γ], ProbabilityTheory.Kernel.swapLeft 0 = 0

@[simp]

theorem ProbabilityTheory.Kernel.swapRight_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} [inst : MeasurableSpace γ], ProbabilityTheory.Kernel.swapRight 0 = 0

@[simp]

theorem ProbabilityTheory.Kernel.prod_zero_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} [inst : MeasurableSpace γ] (η : ProbabilityTheory.Kernel α γ), ProbabilityTheory.Kernel.prod 0 η = 0

@[simp]

theorem ProbabilityTheory.Kernel.prod_zero_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α β), κ.prod 0 = 0

noncomputable def ProbabilityTheory.Kernel.deleteMiddle {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} : {x : MeasurableSpace α} → {x_1 : MeasurableSpace β} → {x_2 : MeasurableSpace δ} → [inst : MeasurableSpace γ] → ProbabilityTheory.Kernel α (β × γ × δ) → ProbabilityTheory.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_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.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_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α (β × γ × δ)) [inst_1 : ProbabilityTheory.IsMarkovKernel κ], ProbabilityTheory.IsMarkovKernel κ.deleteMiddle

Equations

• ⋯ = ⋯

instance ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelProdDeleteMiddle {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α (β × γ × δ)) [inst_1 : ProbabilityTheory.IsZeroOrMarkovKernel κ], ProbabilityTheory.IsZeroOrMarkovKernel κ.deleteMiddle

Equations

• ⋯ = ⋯

@[simp]

theorem ProbabilityTheory.Kernel.fst_deleteMiddle {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.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_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.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_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ], ProbabilityTheory.Kernel.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_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} {x_3 : MeasurableSpace ε} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α β) {f : β → γ} {g : β → δ} {g' : β → ε}, 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_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (ξ : ProbabilityTheory.Kernel α β) [inst_1 : ProbabilityTheory.IsSFiniteKernel ξ] (κ : ProbabilityTheory.Kernel (α × β) (γ × δ)) [inst_2 : ProbabilityTheory.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_1 : MeasurableSpace β} → {x_2 : MeasurableSpace δ} → [inst : MeasurableSpace γ] → ProbabilityTheory.Kernel α (β × γ × δ) → ProbabilityTheory.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_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.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_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ], ProbabilityTheory.Kernel.deleteRight 0 = 0

instance ProbabilityTheory.Kernel.instIsMarkovKernelProdDeleteRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α (β × γ × δ)) [inst_1 : ProbabilityTheory.IsMarkovKernel κ], ProbabilityTheory.IsMarkovKernel κ.deleteRight

Equations

• ⋯ = ⋯

instance ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelProdDeleteRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α (β × γ × δ)) [inst_1 : ProbabilityTheory.IsZeroOrMarkovKernel κ], ProbabilityTheory.IsZeroOrMarkovKernel κ.deleteRight

Equations

• ⋯ = ⋯

@[simp]

theorem ProbabilityTheory.Kernel.fst_deleteRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.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_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.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_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} {x_3 : MeasurableSpace ε} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α β) {f : β → γ} {g : β → δ} {g' : β → ε}, 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_1 : MeasurableSpace β} → {x_2 : MeasurableSpace δ} → [inst : MeasurableSpace γ] → ProbabilityTheory.Kernel α (β × γ × δ) → ProbabilityTheory.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_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.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_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ], ProbabilityTheory.Kernel.reverse 0 = 0

@[simp]

theorem ProbabilityTheory.Kernel.reverse_reverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α (β × γ × δ)), κ.reverse.reverse = κ

instance ProbabilityTheory.Kernel.instIsMarkovKernelProdReverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α (β × γ × δ)) [inst_1 : ProbabilityTheory.IsMarkovKernel κ], ProbabilityTheory.IsMarkovKernel κ.reverse

Equations

• ⋯ = ⋯

instance ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelProdReverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α (β × γ × δ)) [inst_1 : ProbabilityTheory.IsZeroOrMarkovKernel κ], ProbabilityTheory.IsZeroOrMarkovKernel κ.reverse

Equations

• ⋯ = ⋯

@[simp]

theorem ProbabilityTheory.Kernel.swapRight_deleteMiddle_reverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.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_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.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_1 : MeasurableSpace β} {x_2 : MeasurableSpace δ} [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α (β × γ × δ)), κ.reverse.deleteRight.swapRight = κ.snd

theorem ProbabilityTheory.Kernel.FiniteKernelSupport.reverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {T : Type u_8} [inst : MeasurableSpace T] [inst_1 : MeasurableSpace γ] [inst_2 : MeasurableSingletonClass α] [inst_3 : MeasurableSingletonClass β] [inst_4 : MeasurableSingletonClass γ] {κ : ProbabilityTheory.Kernel T (α × β × γ)}, κ.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} [inst : MeasurableSpace S] [inst_1 : MeasurableSpace T] [inst_2 : MeasurableSpace γ] [inst_3 : MeasurableSingletonClass S] [inst_4 : MeasurableSingletonClass β] [inst_5 : MeasurableSingletonClass γ] {κ : ProbabilityTheory.Kernel T (S × β × γ)} {μ : MeasureTheory.Measure T}, κ.AEFiniteKernelSupport μ → κ.reverse.AEFiniteKernelSupport μ