noncomputable def
ProbabilityTheory.Kernel.fst'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
(b : β)
:
Define a Kernel α γ from a Kernel (α × β) γ by taking the comap of fun a ↦ (a, b) for
a given b : β.
Equations
- κ.fst' b = κ.comap (fun (a : α) => (a, b)) ⋯
Instances For
@[simp]
theorem
ProbabilityTheory.Kernel.fst'_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
(b : β)
(a : α)
:
(κ.fst' b) a = κ (a, b)
@[simp]
theorem
ProbabilityTheory.Kernel.fst'_zero
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(b : β)
:
instance
ProbabilityTheory.Kernel.instIsMarkovKernelFst'OfProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
(b : β)
[ProbabilityTheory.IsMarkovKernel κ]
:
ProbabilityTheory.IsMarkovKernel (κ.fst' b)
Equations
- ⋯ = ⋯
instance
ProbabilityTheory.Kernel.instIsFiniteKernelFst'OfProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
(b : β)
[ProbabilityTheory.IsFiniteKernel κ]
:
ProbabilityTheory.IsFiniteKernel (κ.fst' b)
Equations
- ⋯ = ⋯
instance
ProbabilityTheory.Kernel.instIsSFiniteKernelFst'OfProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
(b : β)
[ProbabilityTheory.IsSFiniteKernel κ]
:
ProbabilityTheory.IsSFiniteKernel (κ.fst' b)
Equations
- ⋯ = ⋯
instance
ProbabilityTheory.Kernel.instNeZeroMeasureCoeFst'OfProdMk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
(a : α)
(b : β)
[NeZero (κ (a, b))]
:
NeZero ((κ.fst' b) a)
Equations
- ⋯ = ⋯
@[instance 100]
instance
ProbabilityTheory.Kernel.instIsMarkovKernelProdOfFst'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : ProbabilityTheory.Kernel (α × β) γ}
[∀ (b : β), ProbabilityTheory.IsMarkovKernel (κ.fst' b)]
:
Equations
- ⋯ = ⋯
theorem
ProbabilityTheory.Kernel.comap_fst'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{δ : Type u_5}
{mδ : MeasurableSpace δ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
(b : β)
{f : δ → α}
(hf : Measurable f)
:
(κ.fst' b).comap f hf = κ.comap (fun (d : δ) => (f d, b)) ⋯
@[simp]
theorem
ProbabilityTheory.Kernel.fst'_prodMkLeft
{β : Type u_2}
{γ : Type u_3}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(α : Type u_6)
[MeasurableSpace α]
(κ : ProbabilityTheory.Kernel β γ)
(a : α)
{b : β}
:
((ProbabilityTheory.Kernel.prodMkLeft α κ).fst' b) a = κ b
@[simp]
theorem
ProbabilityTheory.Kernel.fst'_prodMkRight
{α : Type u_1}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
(β : Type u_6)
[MeasurableSpace β]
(κ : ProbabilityTheory.Kernel α γ)
(b : β)
:
(ProbabilityTheory.Kernel.prodMkRight β κ).fst' b = κ
noncomputable def
ProbabilityTheory.Kernel.snd'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
(a : α)
:
Define a Kernel β γ from a Kernel (α × β) γ by taking the comap of fun b ↦ (a, b) for
a given a : α.
Equations
- κ.snd' a = κ.comap (fun (b : β) => (a, b)) ⋯
Instances For
@[simp]
theorem
ProbabilityTheory.Kernel.snd'_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
(b : β)
(a : α)
:
(κ.snd' a) b = κ (a, b)
@[simp]
theorem
ProbabilityTheory.Kernel.snd'_zero
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(a : α)
:
instance
ProbabilityTheory.Kernel.instIsMarkovKernelSnd'OfProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
(a : α)
[ProbabilityTheory.IsMarkovKernel κ]
:
ProbabilityTheory.IsMarkovKernel (κ.snd' a)
Equations
- ⋯ = ⋯
instance
ProbabilityTheory.Kernel.instIsFiniteKernelSnd'OfProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
(a : α)
[ProbabilityTheory.IsFiniteKernel κ]
:
ProbabilityTheory.IsFiniteKernel (κ.snd' a)
Equations
- ⋯ = ⋯
instance
ProbabilityTheory.Kernel.instIsSFiniteKernelSnd'OfProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
(a : α)
[ProbabilityTheory.IsSFiniteKernel κ]
:
ProbabilityTheory.IsSFiniteKernel (κ.snd' a)
Equations
- ⋯ = ⋯
instance
ProbabilityTheory.Kernel.instNeZeroMeasureCoeSnd'OfProdMk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
(a : α)
(b : β)
[NeZero (κ (a, b))]
:
NeZero ((κ.snd' a) b)
Equations
- ⋯ = ⋯
@[instance 100]
instance
ProbabilityTheory.Kernel.instIsMarkovKernelProdOfSnd'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : ProbabilityTheory.Kernel (α × β) γ}
[∀ (b : α), ProbabilityTheory.IsMarkovKernel (κ.snd' b)]
:
Equations
- ⋯ = ⋯
theorem
ProbabilityTheory.Kernel.comap_snd'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{δ : Type u_5}
{mδ : MeasurableSpace δ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
(a : α)
{f : δ → β}
(hf : Measurable f)
:
(κ.snd' a).comap f hf = κ.comap (fun (d : δ) => (a, f d)) ⋯
@[simp]
theorem
ProbabilityTheory.Kernel.snd'_prodMkLeft
{β : Type u_2}
{γ : Type u_3}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(α : Type u_6)
[MeasurableSpace α]
(κ : ProbabilityTheory.Kernel β γ)
(a : α)
:
(ProbabilityTheory.Kernel.prodMkLeft α κ).snd' a = κ
@[simp]
theorem
ProbabilityTheory.Kernel.snd'_prodMkRight
{α : Type u_1}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
(β : Type u_6)
[MeasurableSpace β]
(κ : ProbabilityTheory.Kernel α γ)
(b : β)
{a : α}
:
((ProbabilityTheory.Kernel.prodMkRight β κ).snd' a) b = κ a
@[simp]
theorem
ProbabilityTheory.Kernel.fst'_swapRight
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
:
κ.swapLeft.fst' = κ.snd'
@[simp]
theorem
ProbabilityTheory.Kernel.snd'_swapRight
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel (α × β) γ)
:
κ.swapLeft.snd' = κ.fst'
theorem
ProbabilityTheory.Kernel.compProd_apply_eq_compProd_snd'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel (α × β) γ)
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
(a : α)
:
(κ.compProd η) a = (κ a).compProd (η.snd' a)