theorem ProbabilityTheory.kernel.map_map {α : Type u_1} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace δ} {β : Type u_9} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] (κ : ↥(ProbabilityTheory.kernel α β)) {f : β → γ} (hf : Measurable f) {g : γ → δ} (hg : Measurable g), ProbabilityTheory.kernel.map (ProbabilityTheory.kernel.map κ f hf) g hg = ProbabilityTheory.kernel.map κ (g ∘ f) ⋯

theorem ProbabilityTheory.kernel.map_swapRight {α : Type u_1} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace δ} {β : Type u_9} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] (κ : ↥(ProbabilityTheory.kernel α (β × γ))) {f : γ × β → δ} (hf : Measurable f), ProbabilityTheory.kernel.map (ProbabilityTheory.kernel.swapRight κ) f hf = ProbabilityTheory.kernel.map κ (f ∘ Prod.swap) ⋯

noncomputable def ProbabilityTheory.kernel.deleteMiddle {α : Type u_1} {γ : Type u_3} {δ : Type u_4} : {x : MeasurableSpace α} → {x_1 : MeasurableSpace δ} → {β : Type u_9} → [inst : MeasurableSpace β] → [inst_1 : MeasurableSpace γ] → ↥(ProbabilityTheory.kernel α (β × γ × δ)) → ↥(ProbabilityTheory.kernel α (β × δ))

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

Equations

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

instance ProbabilityTheory.kernel.instIsMarkovKernelProdDeleteMiddle {α : Type u_1} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace δ} {β : Type u_9} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] (κ : ↥(ProbabilityTheory.kernel α (β × γ × δ))) [inst_2 : ProbabilityTheory.IsMarkovKernel κ], ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.deleteMiddle κ)

Equations

• ⋯ = ⋯

@[simp]

theorem ProbabilityTheory.kernel.fst_deleteMiddle {α : Type u_1} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace δ} {β : Type u_9} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] (κ : ↥(ProbabilityTheory.kernel α (β × γ × δ))), ProbabilityTheory.kernel.fst (ProbabilityTheory.kernel.deleteMiddle κ) = ProbabilityTheory.kernel.fst κ

@[simp]

theorem ProbabilityTheory.kernel.snd_deleteMiddle {α : Type u_1} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace δ} {β : Type u_9} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] (κ : ↥(ProbabilityTheory.kernel α (β × γ × δ))), ProbabilityTheory.kernel.snd (ProbabilityTheory.kernel.deleteMiddle κ) = ProbabilityTheory.kernel.snd (ProbabilityTheory.kernel.snd κ)

@[simp]

theorem ProbabilityTheory.kernel.deleteMiddle_map_prod {α : Type u_1} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace δ} {x_2 : MeasurableSpace ε} {β : Type u_9} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] (κ : ↥(ProbabilityTheory.kernel α β)) {f : β → γ} {g : β → δ} {g' : β → ε} (hf : Measurable f) (hg : Measurable g) (hg' : Measurable g'), ProbabilityTheory.kernel.deleteMiddle (ProbabilityTheory.kernel.map κ (fun (b : β) => (f b, g b, g' b)) ⋯) = ProbabilityTheory.kernel.map κ (fun (b : β) => (f b, g' b)) ⋯

@[simp]

theorem ProbabilityTheory.kernel.deleteMiddle_compProd {α : Type u_1} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace δ} {β : Type u_9} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] (ξ : ↥(ProbabilityTheory.kernel α β)) [inst_2 : ProbabilityTheory.IsSFiniteKernel ξ] (κ : ↥(ProbabilityTheory.kernel (α × β) (γ × δ))) [inst_3 : ProbabilityTheory.IsSFiniteKernel κ], ProbabilityTheory.kernel.deleteMiddle (ProbabilityTheory.kernel.compProd ξ κ) = ProbabilityTheory.kernel.compProd ξ (ProbabilityTheory.kernel.snd κ)

noncomputable def ProbabilityTheory.kernel.deleteRight {α : Type u_1} {γ : Type u_3} {δ : Type u_4} : {x : MeasurableSpace α} → {x_1 : MeasurableSpace δ} → {β : Type u_9} → [inst : MeasurableSpace β] → [inst_1 : MeasurableSpace γ] → ↥(ProbabilityTheory.kernel α (β × γ × δ)) → ↥(ProbabilityTheory.kernel α (β × γ))

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

Equations

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

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

Equations

• ⋯ = ⋯

@[simp]

theorem ProbabilityTheory.kernel.fst_deleteRight {α : Type u_1} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace δ} {β : Type u_9} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] (κ : ↥(ProbabilityTheory.kernel α (β × γ × δ))), ProbabilityTheory.kernel.fst (ProbabilityTheory.kernel.deleteRight κ) = ProbabilityTheory.kernel.fst κ

@[simp]

theorem ProbabilityTheory.kernel.snd_deleteRight {α : Type u_1} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace δ} {β : Type u_9} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] (κ : ↥(ProbabilityTheory.kernel α (β × γ × δ))), ProbabilityTheory.kernel.snd (ProbabilityTheory.kernel.deleteRight κ) = ProbabilityTheory.kernel.fst (ProbabilityTheory.kernel.snd κ)

@[simp]

theorem ProbabilityTheory.kernel.deleteRight_map_prod {α : Type u_1} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace δ} {x_2 : MeasurableSpace ε} {β : Type u_9} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] (κ : ↥(ProbabilityTheory.kernel α β)) {f : β → γ} {g : β → δ} {g' : β → ε} (hf : Measurable f) (hg : Measurable g) (hg' : Measurable g'), ProbabilityTheory.kernel.deleteRight (ProbabilityTheory.kernel.map κ (fun (b : β) => (f b, g b, g' b)) ⋯) = ProbabilityTheory.kernel.map κ (fun (b : β) => (f b, g b)) ⋯

noncomputable def ProbabilityTheory.kernel.reverse {α : Type u_1} {γ : Type u_3} {δ : Type u_4} : {x : MeasurableSpace α} → {x_1 : MeasurableSpace δ} → {β : Type u_9} → [inst : MeasurableSpace β] → [inst_1 : MeasurableSpace γ] → ↥(ProbabilityTheory.kernel α (β × γ × δ)) → ↥(ProbabilityTheory.kernel α (δ × γ × β))

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

Equations

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

@[simp]

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

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

Equations

• ⋯ = ⋯

@[simp]

theorem ProbabilityTheory.kernel.swapRight_deleteMiddle_reverse {α : Type u_1} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace δ} {β : Type u_9} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] (κ : ↥(ProbabilityTheory.kernel α (β × γ × δ))), ProbabilityTheory.kernel.swapRight (ProbabilityTheory.kernel.deleteMiddle (ProbabilityTheory.kernel.reverse κ)) = ProbabilityTheory.kernel.deleteMiddle κ

@[simp]

theorem ProbabilityTheory.kernel.swapRight_snd_reverse {α : Type u_1} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace δ} {β : Type u_9} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] (κ : ↥(ProbabilityTheory.kernel α (β × γ × δ))), ProbabilityTheory.kernel.swapRight (ProbabilityTheory.kernel.snd (ProbabilityTheory.kernel.reverse κ)) = ProbabilityTheory.kernel.deleteRight κ

@[simp]

theorem ProbabilityTheory.kernel.swapRight_deleteRight_reverse {α : Type u_1} {γ : Type u_3} {δ : Type u_4} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace δ} {β : Type u_9} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] (κ : ↥(ProbabilityTheory.kernel α (β × γ × δ))), ProbabilityTheory.kernel.swapRight (ProbabilityTheory.kernel.deleteRight (ProbabilityTheory.kernel.reverse κ)) = ProbabilityTheory.kernel.snd κ

theorem ProbabilityTheory.kernel.finiteKernelSupport_of_reverse {α : Type u_1} {γ : Type u_3} : ∀ {x : MeasurableSpace α} {T : Type u_8} {β : Type u_9} [inst : MeasurableSpace T] [inst_1 : Countable β] [inst_2 : MeasurableSpace β] [inst_3 : MeasurableSingletonClass β] [inst_4 : Countable γ] [inst_5 : MeasurableSpace γ] [inst_6 : MeasurableSingletonClass γ] [inst_7 : Countable α] [inst_8 : MeasurableSingletonClass α] {κ : ↥(ProbabilityTheory.kernel T (α × β × γ))}, ProbabilityTheory.kernel.FiniteKernelSupport κ → ProbabilityTheory.kernel.FiniteKernelSupport (ProbabilityTheory.kernel.reverse κ)

Reversing preserves finite kernel support

theorem ProbabilityTheory.kernel.AEFiniteKernelSupport.reverse {γ : Type u_3} {S : Type u_7} {T : Type u_8} {β : Type u_9} [Countable S] [MeasurableSpace S] [MeasurableSingletonClass S] [MeasurableSpace T] [Countable β] [MeasurableSpace β] [MeasurableSingletonClass β] [Countable γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] {κ : ↥(ProbabilityTheory.kernel T (S × β × γ))} {μ : MeasureTheory.Measure T} (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : ProbabilityTheory.kernel.AEFiniteKernelSupport (ProbabilityTheory.kernel.reverse κ) μ