Composition-product of kernels #
We define the composition-product κ ⊗ₖ η of two s-finite kernels κ : Kernel α β and
η : Kernel (α × β) γ, a kernel from α to β × γ.
A note on names:
The composition-product Kernel α β → Kernel (α × β) γ → Kernel α (β × γ) is named composition in
[kallenberg2021] and product on the wikipedia article on transition kernels.
Most papers studying categories of kernels call composition the map we call composition. We adopt
that convention because it fits better with the use of the name comp elsewhere in mathlib.
Main definitions #
compProd (κ : Kernel α β) (η : Kernel (α × β) γ) : Kernel α (β × γ): composition-product of 2 s-finite kernels. We define a notationκ ⊗ₖ η = compProd κ η.∫⁻ bc, f bc ∂((κ ⊗ₖ η) a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)
Main statements #
lintegral_compProd: Lebesgue integral of a function against a composition-product of kernels.- Instances stating that
IsMarkovKernel,IsZeroOrMarkovKernel,IsFiniteKernelandIsSFiniteKernelare stable by composition-product.
Notations #
κ ⊗ₖ η = ProbabilityTheory.Kernel.compProd κ η
Composition-Product of kernels #
We define a kernel composition-product
compProd : Kernel α β → Kernel (α × β) γ → Kernel α (β × γ).
noncomputable def
ProbabilityTheory.Kernel.compProdFun
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
(a : α)
(s : Set (β × γ))
:
Auxiliary function for the definition of the composition-product of two kernels.
For all a : α, compProdFun κ η a is a countably additive function with value zero on the empty
set, and the composition-product of kernels is defined in Kernel.compProd through
Measure.ofMeasurable.
Instances For
theorem
ProbabilityTheory.Kernel.compProdFun_empty
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
(a : α)
:
theorem
ProbabilityTheory.Kernel.compProdFun_iUnion
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
(f : ℕ → Set (β × γ))
(hf_meas : ∀ (i : ℕ), MeasurableSet (f i))
(hf_disj : Pairwise (Function.onFun Disjoint f))
:
theorem
ProbabilityTheory.Kernel.compProdFun_tsum_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.Kernel.compProdFun_tsum_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsSFiniteKernel κ]
(a : α)
(s : Set (β × γ))
:
theorem
ProbabilityTheory.Kernel.compProdFun_eq_tsum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.Kernel.measurable_compProdFun
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(hs : MeasurableSet s)
:
Measurable fun (a : α) => κ.compProdFun η a s
@[deprecated ProbabilityTheory.Kernel.measurable_compProdFun (since := "2024-08-30")]
theorem
ProbabilityTheory.Kernel.measurable_compProdFun_of_finite
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(hs : MeasurableSet s)
:
Measurable fun (a : α) => κ.compProdFun η a s
noncomputable def
ProbabilityTheory.Kernel.compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
:
Composition-Product of kernels. For s-finite kernels, it satisfies
∫⁻ bc, f bc ∂(compProd κ η a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)
(see ProbabilityTheory.Kernel.lintegral_compProd).
If either of the kernels is not s-finite, compProd is given the junk value 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Composition-Product of kernels. For s-finite kernels, it satisfies
∫⁻ bc, f bc ∂(compProd κ η a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)
(see ProbabilityTheory.Kernel.lintegral_compProd).
If either of the kernels is not s-finite, compProd is given the junk value 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.Kernel.compProd_apply_eq_compProdFun
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
(hs : MeasurableSet s)
:
@[simp]
theorem
ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
(h : ¬IsSFiniteKernel κ)
:
@[simp]
theorem
ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
(h : ¬IsSFiniteKernel η)
:
theorem
ProbabilityTheory.Kernel.compProd_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
(hs : MeasurableSet s)
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
:
theorem
ProbabilityTheory.Kernel.le_compProd_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
(s : Set (β × γ))
:
@[simp]
theorem
ProbabilityTheory.Kernel.compProd_apply_univ
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η : Kernel (α × β) γ}
[IsSFiniteKernel κ]
[IsMarkovKernel η]
{a : α}
:
theorem
ProbabilityTheory.Kernel.compProd_apply_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η : Kernel (α × β) γ}
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
{a : α}
{s : Set β}
{t : Set γ}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.Kernel.compProd_congr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η η' : Kernel (α × β) γ}
[IsSFiniteKernel η]
[IsSFiniteKernel η']
(h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = η' (a, b))
:
@[simp]
theorem
ProbabilityTheory.Kernel.compProd_zero_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel (α × β) γ)
:
@[simp]
theorem
ProbabilityTheory.Kernel.compProd_zero_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : Kernel α β)
(γ : Type u_4)
{mγ : MeasurableSpace γ}
:
theorem
ProbabilityTheory.Kernel.compProd_eq_zero_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η : Kernel (α × β) γ}
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
:
theorem
ProbabilityTheory.Kernel.compProd_preimage_fst
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set β}
(hs : MeasurableSet s)
(κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsSFiniteKernel κ]
[IsMarkovKernel η]
(x : α)
:
theorem
ProbabilityTheory.Kernel.compProd_deterministic_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSingletonClass γ]
{f : α × β → γ}
(hf : Measurable f)
{s : Set (β × γ)}
(hs : MeasurableSet s)
(κ : Kernel α β)
[IsSFiniteKernel κ]
(x : α)
:
ae filter of the composition-product #
theorem
ProbabilityTheory.Kernel.ae_kernel_lt_top
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
(a : α)
(h2s : ((κ.compProd η) a) s ≠ ⊤)
:
theorem
ProbabilityTheory.Kernel.compProd_null
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
(a : α)
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.Kernel.ae_null_of_compProd_null
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
(h : ((κ.compProd η) a) s = 0)
:
theorem
ProbabilityTheory.Kernel.ae_ae_of_ae_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
{p : β × γ → Prop}
(h : ∀ᵐ (bc : β × γ) ∂(κ.compProd η) a, p bc)
:
theorem
ProbabilityTheory.Kernel.ae_compProd_of_ae_ae
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{a : α}
{κ : Kernel α β}
{η : Kernel (α × β) γ}
{p : β × γ → Prop}
(hp : MeasurableSet {x : β × γ | p x})
(h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c))
:
theorem
ProbabilityTheory.Kernel.ae_compProd_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
{p : β × γ → Prop}
(hp : MeasurableSet {x : β × γ | p x})
:
theorem
ProbabilityTheory.Kernel.compProd_restrict
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{s : Set β}
{t : Set γ}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.Kernel.compProd_restrict_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{s : Set β}
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.Kernel.compProd_restrict_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{t : Set γ}
(ht : MeasurableSet t)
:
Lebesgue integral #
theorem
ProbabilityTheory.Kernel.lintegral_compProd'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
{f : β → γ → ENNReal}
(hf : Measurable (Function.uncurry f))
:
Lebesgue integral against the composition-product of two kernels.
theorem
ProbabilityTheory.Kernel.lintegral_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
{f : β × γ → ENNReal}
(hf : Measurable f)
:
Lebesgue integral against the composition-product of two kernels.
theorem
ProbabilityTheory.Kernel.lintegral_compProd₀
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
{f : β × γ → ENNReal}
(hf : AEMeasurable f ((κ.compProd η) a))
:
Lebesgue integral against the composition-product of two kernels.
theorem
ProbabilityTheory.Kernel.setLIntegral_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
{f : β × γ → ENNReal}
(hf : Measurable f)
{s : Set β}
{t : Set γ}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.Kernel.setLIntegral_compProd_univ_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
{f : β × γ → ENNReal}
(hf : Measurable f)
{s : Set β}
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.Kernel.setLIntegral_compProd_univ_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
{f : β × γ → ENNReal}
(hf : Measurable f)
{t : Set γ}
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.Kernel.compProd_eq_tsum_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.Kernel.compProd_eq_sum_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
:
theorem
ProbabilityTheory.Kernel.compProd_eq_sum_compProd_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
:
theorem
ProbabilityTheory.Kernel.compProd_eq_sum_compProd_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
:
instance
ProbabilityTheory.Kernel.IsMarkovKernel.compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsMarkovKernel κ]
(η : Kernel (α × β) γ)
[IsMarkovKernel η]
:
IsMarkovKernel (κ.compProd η)
instance
ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsZeroOrMarkovKernel κ]
(η : Kernel (α × β) γ)
[IsZeroOrMarkovKernel η]
:
IsZeroOrMarkovKernel (κ.compProd η)
theorem
ProbabilityTheory.Kernel.compProd_apply_univ_le
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsFiniteKernel η]
(a : α)
:
instance
ProbabilityTheory.Kernel.IsFiniteKernel.compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsFiniteKernel η]
:
IsFiniteKernel (κ.compProd η)
instance
ProbabilityTheory.Kernel.IsSFiniteKernel.compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
:
IsSFiniteKernel (κ.compProd η)
theorem
ProbabilityTheory.Kernel.compProd_add_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(μ κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsSFiniteKernel μ]
[IsSFiniteKernel κ]
:
theorem
ProbabilityTheory.Kernel.compProd_add_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(μ : Kernel α β)
(κ η : Kernel (α × β) γ)
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
:
theorem
ProbabilityTheory.Kernel.compProd_sum_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{ι : Type u_4}
[Countable ι]
{κ : ι → Kernel α β}
{η : Kernel (α × β) γ}
[∀ (i : ι), IsSFiniteKernel (κ i)]
:
theorem
ProbabilityTheory.Kernel.compProd_sum_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{ι : Type u_4}
[Countable ι]
{κ : Kernel α β}
{η : ι → Kernel (α × β) γ}
[∀ (i : ι), IsSFiniteKernel (η i)]
:
theorem
ProbabilityTheory.Kernel.comapRight_compProd_id_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{δ : Type u_4}
{mδ : MeasurableSpace δ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
{f : δ → γ}
(hf : MeasurableEmbedding f)
:
theorem
ProbabilityTheory.Kernel.fst_compProd_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
(x : α)
{s : Set β}
(hs : MeasurableSet s)
:
If η is a Markov kernel, use instead fst_compProd to get (κ ⊗ₖ η).fst = κ.
@[simp]
theorem
ProbabilityTheory.Kernel.fst_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsSFiniteKernel κ]
[IsMarkovKernel η]
: