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)
:
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 : γ × β → δ}
:
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 α (β × γ × δ))
:
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)) ⋯
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 γ]
(κ : Kernel α (β × γ × δ))
:
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 κ]
:
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 κ]
:
@[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 α (β × γ × δ))
:
@[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 α (β × γ × δ))
:
@[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 γ]
(κ : Kernel α β)
{f : β → γ}
{g : β → δ}
{g' : β → ε}
(hg : Measurable g)
:
@[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 κ]
:
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 α (β × γ × δ))
:
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)) ⋯
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 γ]
(κ : 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 γ]
(κ : Kernel α (β × γ × δ))
[IsMarkovKernel κ]
:
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 κ]
:
@[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 α (β × γ × δ))
:
@[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 α (β × γ × δ))
:
@[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')
:
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 α (β × γ × δ))
:
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 γ]
(κ : 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 γ]
(κ : Kernel α (β × γ × δ))
:
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 κ]
:
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 κ]
:
@[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 α (β × γ × δ))
:
@[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 α (β × γ × δ))
:
@[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 α (β × γ × δ))
:
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)
:
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 μ)
: