# 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`, `IsFiniteKernel` and `IsSFiniteKernel` are stable by composition-product.

## Notation #

- `κ ⊗ₖ η = ProbabilityTheory.Kernel.compProd κ η`

### Composition-Product of kernels #

We define a kernel composition-product `compProd : Kernel α β → Kernel (α × β) γ → Kernel α (β × γ)`.

source
theorem ProbabilityTheory.Kernel.compProd_def {α : Type u_4} {β : Type u_5} {γ : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel (α × β) γ) :
κ.compProd η = (((((swap γ β).comp (η.parallelComp Kernel.id)).comp (deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯)).comp (Kernel.id.parallelComp (copy β))).comp (Kernel.id.parallelComp κ)).comp (copy α)
source
@[irreducible]
noncomputable def ProbabilityTheory.Kernel.compProd {α : Type u_4} {β : Type u_5} {γ : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : 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

source
def ProbabilityTheory.«term_⊗ₖ_» :
Lean.TrailingParserDescr

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

source
@[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 κ) :
κ.compProd η = 0
source
@[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 η) :
κ.compProd η = 0
source
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 : α) :
((κ.compProd η) a) s = ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a
source
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 (β × γ)) :
∫⁻ (b : β), (η (a, b)) {c : γ | (b, c) ∈ s} ∂κ a ≤ ((κ.compProd η) a) s
source
@[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 : α} :
((κ.compProd η) a) Set.univ = (κ a) Set.univ
source
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) :
((κ.compProd η) a) (s ×ˢ t) = ∫⁻ (b : β) in s, (η (a, b)) t ∂κ a
source
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)) :
κ.compProd η = κ.compProd η'
source
@[simp]
theorem ProbabilityTheory.Kernel.compProd_zero_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) :
compProd 0 κ = 0
source
@[simp]
theorem ProbabilityTheory.Kernel.compProd_zero_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) (γ : Type u_4) {mγ : MeasurableSpace γ} :
κ.compProd 0 = 0
source
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 η] :
κ.compProd η = 0 ↔ ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 0
source
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 : α) :
((κ.compProd η) x) (Prod.fst ⁻¹' s) = (κ x) s
source
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 : α) :
((κ.compProd (deterministic f hf)) x) s = (κ x) {b : β | (b, f (x, b)) ∈ s}

### `ae` filter of the composition-product #

source
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 ≠ ⊤) :
∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤
source
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) :
((κ.compProd η) a) s = 0 ↔ (fun (b : β) => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0
source
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) :
(fun (b : β) => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0
source
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) :
∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
source
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)) :
∀ᵐ (bc : β × γ) ∂(κ.compProd η) a, p bc
source
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}) :
(∀ᵐ (bc : β × γ) ∂(κ.compProd η) a, p bc) ↔ ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
source
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) :
(κ.restrict hs).compProd (η.restrict ht) = (κ.compProd η).restrict ⋯
source
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) :
(κ.restrict hs).compProd η = (κ.compProd η).restrict ⋯
source
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) :
κ.compProd (η.restrict ht) = (κ.compProd η).restrict ⋯

### Lebesgue integral #

source
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)) :
∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(κ.compProd η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂η (a, b) ∂κ a

Lebesgue integral against the composition-product of two kernels.

source
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) :
∫⁻ (bc : β × γ), f bc ∂(κ.compProd η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c) ∂η (a, b) ∂κ a

Lebesgue integral against the composition-product of two kernels.

source
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)) :
∫⁻ (z : β × γ), f z ∂(κ.compProd η) a = ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a

Lebesgue integral against the composition-product of two kernels.

source
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) :
∫⁻ (z : β × γ) in s ×ˢ t, f z ∂(κ.compProd η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
source
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) :
∫⁻ (z : β × γ) in s ×ˢ Set.univ, f z ∂(κ.compProd η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a
source
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) :
∫⁻ (z : β × γ) in Set.univ ×ˢ t, f z ∂(κ.compProd η) a = ∫⁻ (x : β), ∫⁻ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
source
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 (α × β) γ) :
κ.compProd η = Kernel.sum fun (n : ℕ) => (κ.seq n).compProd η
source
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 η] :
κ.compProd η = Kernel.sum fun (n : ℕ) => κ.compProd (η.seq n)
source
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 η] :
κ.compProd η = Kernel.sum fun (n : ℕ) => Kernel.sum fun (m : ℕ) => (κ.seq n).compProd (η.seq m)
source
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) :
((κ.compProd η) a) s = ∑' (n : ℕ) (m : ℕ), (((κ.seq n).compProd (η.seq m)) a) s
source
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 η)
source
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 η)
source
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 : α) :
((κ.compProd η) a) Set.univ ≤ (κ a) Set.univ * η.bound
source
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 η)
source
instance ProbabilityTheory.Kernel.IsSFiniteKernel.compProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel (α × β) γ) :
IsSFiniteKernel (κ.compProd η)
source
theorem ProbabilityTheory.Kernel.compProd_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {δ : Type u_4} {mδ : MeasurableSpace δ} {κ : Kernel α β} {η : Kernel (α × β) γ} {ξ : Kernel (α × β × γ) δ} :
(κ.compProd (η.compProd (ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯))).map ⇑MeasurableEquiv.prodAssoc.symm = (κ.compProd η).compProd ξ

`Kernel.compProd` is associative. We have to insert `MeasurableEquiv.prodAssoc` in two places because the products of types `α × β × γ` and `(α × β) × γ` are different.

source
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 κ] :
(μ + κ).compProd η = μ.compProd η + κ.compProd η
source
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 η] :
μ.compProd (κ + η) = μ.compProd κ + μ.compProd η
source
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)] :
(Kernel.sum κ).compProd η = Kernel.sum fun (i : ι) => (κ i).compProd η
source
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)] :
κ.compProd (Kernel.sum η) = Kernel.sum fun (i : ι) => κ.compProd (η i)
source
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) :
(κ.compProd η).comapRight ⋯ = κ.compProd (η.comapRight hf)
source
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) :
((κ.compProd η).fst x) s = ∫⁻ (b : β), s.indicator (fun (b : β) => (η (x, b)) Set.univ) b ∂κ x

If `η` is a Markov kernel, use instead `fst_compProd` to get `(κ ⊗ₖ η).fst = κ`.

source
@[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 η] :
(κ.compProd η).fst = κ