Composition of kernels #
We define the composition η ∘ₖ κ of kernels κ : Kernel α β and η : Kernel β γ, which is
a kernel from α to γ.
Main definitions #
comp (η : Kernel β γ) (κ : Kernel α β) : Kernel α γ: composition of 2 kernels. We define a notationη ∘ₖ κ = comp η κ.∫⁻ c, g c ∂((η ∘ₖ κ) a) = ∫⁻ b, ∫⁻ c, g c ∂(η b) ∂(κ a)
Main statements #
lintegral_comp: Lebesgue integral of a function against a composition of kernels.- Instances stating that
IsMarkovKernel,IsZeroOrMarkovKernel,IsFiniteKernelandIsSFiniteKernelare stable by composition.
Notations #
η ∘ₖ κ = ProbabilityTheory.Kernel.comp η κ
noncomputable def
ProbabilityTheory.Kernel.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(η : Kernel β γ)
(κ : Kernel α β)
:
Kernel α γ
Composition of two kernels.
Composition of two kernels.
Equations
- One or more equations did not get rendered due to their size.
theorem
ProbabilityTheory.Kernel.comp_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(η : Kernel β γ)
(κ : Kernel α β)
(a : α)
:
theorem
ProbabilityTheory.Kernel.comp_apply'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(η : Kernel β γ)
(κ : Kernel α β)
(a : α)
{s : Set γ}
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.Kernel.comp_apply_univ_le
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel β γ)
[IsFiniteKernel η]
(a : α)
:
@[simp]
theorem
ProbabilityTheory.Kernel.zero_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
:
@[simp]
theorem
ProbabilityTheory.Kernel.comp_zero
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel β γ)
:
ae filter of the composition #
theorem
ProbabilityTheory.Kernel.ae_lt_top_of_comp_ne_top
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η : Kernel β γ}
{s : Set γ}
(a : α)
(hs : ((η.comp κ) a) s ≠ ⊤)
:
theorem
ProbabilityTheory.Kernel.comp_null
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η : Kernel β γ}
{s : Set γ}
(a : α)
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.Kernel.ae_null_of_comp_null
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η : Kernel β γ}
{a : α}
{s : Set γ}
(h : ((η.comp κ) a) s = 0)
:
theorem
ProbabilityTheory.Kernel.ae_ae_of_ae_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η : Kernel β γ}
{a : α}
{p : γ → Prop}
(h : ∀ᵐ (z : γ) ∂(η.comp κ) a, p z)
:
theorem
ProbabilityTheory.Kernel.ae_comp_of_ae_ae
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η : Kernel β γ}
{a : α}
{p : γ → Prop}
(hp : MeasurableSet {z : γ | p z})
(h : ∀ᵐ (y : β) ∂κ a, ∀ᵐ (z : γ) ∂η y, p z)
:
theorem
ProbabilityTheory.Kernel.ae_comp_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η : Kernel β γ}
{a : α}
{p : γ → Prop}
(hp : MeasurableSet {z : γ | p z})
:
theorem
ProbabilityTheory.Kernel.comp_restrict
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η : Kernel β γ}
{s : Set γ}
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.Kernel.lintegral_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(η : Kernel β γ)
(κ : Kernel α β)
(a : α)
{g : γ → ENNReal}
(hg : Measurable g)
:
theorem
ProbabilityTheory.Kernel.comp_assoc
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{δ : Type u_4}
{mδ : MeasurableSpace δ}
(ξ : Kernel γ δ)
(η : Kernel β γ)
(κ : Kernel α β)
:
Composition of kernels is associative.
@[simp]
theorem
ProbabilityTheory.Kernel.comp_discard
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : Kernel α β)
[IsMarkovKernel κ]
:
@[simp]
theorem
ProbabilityTheory.Kernel.const_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(μ : MeasureTheory.Measure γ)
(κ : Kernel α β)
:
@[simp]
theorem
ProbabilityTheory.Kernel.const_comp'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(μ : MeasureTheory.Measure γ)
(κ : Kernel α β)
[IsMarkovKernel κ]
:
theorem
ProbabilityTheory.Kernel.comp_add_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(μ κ : Kernel α β)
(η : Kernel β γ)
:
theorem
ProbabilityTheory.Kernel.comp_add_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(μ : Kernel α β)
(κ η : Kernel β γ)
:
theorem
ProbabilityTheory.Kernel.comp_sum_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{ι : Type u_4}
[Countable ι]
(κ : ι → Kernel α β)
(η : Kernel β γ)
:
theorem
ProbabilityTheory.Kernel.comp_sum_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{ι : Type u_4}
[Countable ι]
(κ : Kernel α β)
(η : ι → Kernel β γ)
:
instance
ProbabilityTheory.Kernel.IsMarkovKernel.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(η : Kernel β γ)
[IsMarkovKernel η]
(κ : Kernel α β)
[IsMarkovKernel κ]
:
IsMarkovKernel (η.comp κ)
instance
ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsZeroOrMarkovKernel κ]
(η : Kernel β γ)
[IsZeroOrMarkovKernel η]
:
IsZeroOrMarkovKernel (η.comp κ)
instance
ProbabilityTheory.Kernel.IsFiniteKernel.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(η : Kernel β γ)
[IsFiniteKernel η]
(κ : Kernel α β)
[IsFiniteKernel κ]
:
IsFiniteKernel (η.comp κ)
instance
ProbabilityTheory.Kernel.IsSFiniteKernel.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(η : Kernel β γ)
[IsSFiniteKernel η]
(κ : Kernel α β)
[IsSFiniteKernel κ]
:
IsSFiniteKernel (η.comp κ)