theorem
ProbabilityTheory.Kernel.map_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[MeasurableSpace γ]
(κ : ProbabilityTheory.Kernel α β)
{f : β → γ}
(hf : Measurable f)
{g : γ → δ}
(hg : Measurable g)
:
theorem
ProbabilityTheory.Kernel.map_swapRight
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[MeasurableSpace γ]
(κ : ProbabilityTheory.Kernel α (β × γ))
{f : γ × β → δ}
:
@[simp]
theorem
ProbabilityTheory.Kernel.swapLeft_zero
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
[MeasurableSpace γ]
:
@[simp]
theorem
ProbabilityTheory.Kernel.swapRight_zero
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
[MeasurableSpace γ]
:
@[simp]
theorem
ProbabilityTheory.Kernel.prod_zero_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
[MeasurableSpace γ]
(η : ProbabilityTheory.Kernel α γ)
:
@[simp]
theorem
ProbabilityTheory.Kernel.prod_zero_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
[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✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[MeasurableSpace γ]
(κ : ProbabilityTheory.Kernel α (β × γ × δ))
:
ProbabilityTheory.Kernel α (β × δ)
Given a kernel taking values in a product of three spaces, forget the middle one.
Instances For
theorem
ProbabilityTheory.Kernel.deleteMiddle_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[MeasurableSpace γ]
(κ : ProbabilityTheory.Kernel α (β × γ × δ))
:
instance
ProbabilityTheory.Kernel.instIsMarkovKernelProdDeleteMiddle
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[MeasurableSpace γ]
(κ : ProbabilityTheory.Kernel α (β × γ × δ))
[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✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[MeasurableSpace γ]
(κ : ProbabilityTheory.Kernel α (β × γ × δ))
[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✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[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✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[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✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[MeasurableSpace γ]
:
@[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 γ]
(κ : ProbabilityTheory.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 γ]
(ξ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel ξ]
(κ : ProbabilityTheory.Kernel (α × β) (γ × δ))
[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✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[MeasurableSpace γ]
(κ : ProbabilityTheory.Kernel α (β × γ × δ))
:
ProbabilityTheory.Kernel α (β × γ)
Given a kernel taking values in a product of three spaces, forget the last variable.
Instances For
theorem
ProbabilityTheory.Kernel.deleteRight_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[MeasurableSpace γ]
(κ : ProbabilityTheory.Kernel α (β × γ × δ))
:
@[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 γ]
:
instance
ProbabilityTheory.Kernel.instIsMarkovKernelProdDeleteRight
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[MeasurableSpace γ]
(κ : ProbabilityTheory.Kernel α (β × γ × δ))
[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✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[MeasurableSpace γ]
(κ : ProbabilityTheory.Kernel α (β × γ × δ))
[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✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[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✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[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✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
{x✝³ : MeasurableSpace ε}
[MeasurableSpace γ]
(κ : ProbabilityTheory.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 γ]
(κ : ProbabilityTheory.Kernel α (β × γ × δ))
:
ProbabilityTheory.Kernel α (δ × γ × β)
Given a kernel taking values in a product of three spaces, reverse the order of the spaces.
Instances For
theorem
ProbabilityTheory.Kernel.reverse_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[MeasurableSpace γ]
(κ : ProbabilityTheory.Kernel α (β × γ × δ))
:
theorem
ProbabilityTheory.Kernel.reverse_zero
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[MeasurableSpace γ]
:
@[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 γ]
(κ : ProbabilityTheory.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 γ]
(κ : ProbabilityTheory.Kernel α (β × γ × δ))
[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✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[MeasurableSpace γ]
(κ : ProbabilityTheory.Kernel α (β × γ × δ))
[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✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[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✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[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✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace δ}
[MeasurableSpace γ]
(κ : ProbabilityTheory.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 γ]
{κ : ProbabilityTheory.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 γ]
{κ : ProbabilityTheory.Kernel T (S × β × γ)}
{μ : MeasureTheory.Measure T}
(hκ : κ.AEFiniteKernelSupport μ)
:
κ.reverse.AEFiniteKernelSupport μ