# Product and composition of kernels #

We define

• the composition-product κ ⊗ₖ η of two s-finite kernels κ : kernel α β and η : kernel (α × β) γ, a kernel from α to β × γ.
• the map and comap of a kernel along a measurable function.
• the composition η ∘ₖ κ of kernels κ : kernel α β and η : kernel β γ, kernel from α to γ.
• the product κ ×ₖ η of 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 #

Kernels built from other kernels:

• 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)
• map (κ : kernel α β) (f : β → γ) (hf : Measurable f) : kernel α γ ∫⁻ c, g c ∂(map κ f hf a) = ∫⁻ b, g (f b) ∂(κ a)
• comap (κ : kernel α β) (f : γ → α) (hf : Measurable f) : kernel γ β ∫⁻ b, g b ∂(comap κ f hf c) = ∫⁻ b, g b ∂(κ (f c))
• comp (η : kernel β γ) (κ : kernel α β) : kernel α γ: composition of 2 kernels. We define a notation η ∘ₖ κ = comp η κ. ∫⁻ c, g c ∂((η ∘ₖ κ) a) = ∫⁻ b, ∫⁻ c, g c ∂(η b) ∂(κ a)
• prod (κ : kernel α β) (η : kernel α γ) : kernel α (β × γ): product of 2 s-finite kernels. ∫⁻ bc, f bc ∂((κ ×ₖ η) a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η a) ∂(κ a)

## Main statements #

• lintegral_compProd, lintegral_map, lintegral_comap, lintegral_comp, lintegral_prod: Lebesgue integral of a function against a composition-product/map/comap/composition/product of kernels.
• Instances of the form <class>.<operation> where class is one of IsMarkovKernel, IsFiniteKernel, IsSFiniteKernel and operation is one of compProd, map, comap, comp, prod. These instances state that the three classes are stable by the various operations.

## Notations #

• κ ⊗ₖ η = ProbabilityTheory.kernel.compProd κ η
• η ∘ₖ κ = ProbabilityTheory.kernel.comp η κ
• κ ×ₖ η = ProbabilityTheory.kernel.prod κ η

### 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} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.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.

Equations
• = ∫⁻ (b : β), (η (a, b)) {c : γ | (b, c) s}κ a
Instances For
theorem ProbabilityTheory.kernel.compProdFun_empty {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) :
theorem ProbabilityTheory.kernel.compProdFun_iUnion {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) (f : Set (β × γ)) (hf_meas : ∀ (i : ), MeasurableSet (f i)) (hf_disj : Pairwise (Disjoint on f)) :
ProbabilityTheory.kernel.compProdFun κ η a (⋃ (i : ), f i) = ∑' (i : ),
theorem ProbabilityTheory.kernel.compProdFun_tsum_right {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {s : Set (β × γ)} (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) (hs : ) :
= ∑' (n : ),
theorem ProbabilityTheory.kernel.compProdFun_tsum_left {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) (s : Set (β × γ)) :
= ∑' (n : ),
theorem ProbabilityTheory.kernel.compProdFun_eq_tsum {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {s : Set (β × γ)} (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) (hs : ) :
= ∑' (n : ) (m : ),
theorem ProbabilityTheory.kernel.measurable_compProdFun_of_finite {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {s : Set (β × γ)} (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (hs : ) :
Measurable fun (a : α) =>

Auxiliary lemma for measurable_compProdFun.

theorem ProbabilityTheory.kernel.measurable_compProdFun {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {s : Set (β × γ)} (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (hs : ) :
Measurable fun (a : α) =>
noncomputable def ProbabilityTheory.kernel.compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.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
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} {mα : } {mβ : } {γ : Type u_4} {mγ : } {s : Set (β × γ)} (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) (hs : ) :
() s =
theorem ProbabilityTheory.kernel.compProd_of_not_isSFiniteKernel_left {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) :
theorem ProbabilityTheory.kernel.compProd_of_not_isSFiniteKernel_right {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) :
theorem ProbabilityTheory.kernel.compProd_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {s : Set (β × γ)} (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) (hs : ) :
() s = ∫⁻ (b : β), (η (a, b)) {c : γ | (b, c) s}κ a
theorem ProbabilityTheory.kernel.le_compProd_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) (s : Set (β × γ)) :
∫⁻ (b : β), (η (a, b)) {c : γ | (b, c) s}κ a () s
@[simp]
theorem ProbabilityTheory.kernel.compProd_zero_left {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : (ProbabilityTheory.kernel (α × β) γ)) :
@[simp]
theorem ProbabilityTheory.kernel.compProd_zero_right {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) (γ : Type u_5) [] :

### ae filter of the composition-product #

theorem ProbabilityTheory.kernel.ae_kernel_lt_top {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {s : Set (β × γ)} {κ : ()} {η : (ProbabilityTheory.kernel (α × β) γ)} (a : α) (h2s : () s ) :
∀ᵐ (b : β) ∂κ a, (η (a, b)) ( ⁻¹' s) <
theorem ProbabilityTheory.kernel.compProd_null {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {s : Set (β × γ)} {κ : ()} {η : (ProbabilityTheory.kernel (α × β) γ)} (a : α) (hs : ) :
() s = 0 (κ a).ae.EventuallyEq (fun (b : β) => (η (a, b)) ( ⁻¹' s)) 0
theorem ProbabilityTheory.kernel.ae_null_of_compProd_null {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {s : Set (β × γ)} {κ : ()} {η : (ProbabilityTheory.kernel (α × β) γ)} {a : α} (h : () s = 0) :
(κ a).ae.EventuallyEq (fun (b : β) => (η (a, b)) ( ⁻¹' s)) 0
theorem ProbabilityTheory.kernel.ae_ae_of_ae_compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {κ : ()} {η : (ProbabilityTheory.kernel (α × β) γ)} {a : α} {p : β × γProp} (h : ∀ᵐ (bc : β × γ) ∂, p bc) :
∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
theorem ProbabilityTheory.kernel.ae_compProd_of_ae_ae {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {κ : ()} {η : (ProbabilityTheory.kernel (α × β) γ)} {a : α} {p : β × γProp} (hp : MeasurableSet {x : β × γ | p x}) (h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)) :
∀ᵐ (bc : β × γ) ∂, p bc
theorem ProbabilityTheory.kernel.ae_compProd_iff {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {κ : ()} {η : (ProbabilityTheory.kernel (α × β) γ)} {a : α} {p : β × γProp} (hp : MeasurableSet {x : β × γ | p x}) :
(∀ᵐ (bc : β × γ) ∂, p bc) ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
theorem ProbabilityTheory.kernel.compProd_restrict {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {κ : ()} {η : (ProbabilityTheory.kernel (α × β) γ)} {s : Set β} {t : Set γ} (hs : ) (ht : ) :
theorem ProbabilityTheory.kernel.compProd_restrict_left {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {κ : ()} {η : (ProbabilityTheory.kernel (α × β) γ)} {s : Set β} (hs : ) :
theorem ProbabilityTheory.kernel.compProd_restrict_right {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {κ : ()} {η : (ProbabilityTheory.kernel (α × β) γ)} {t : Set γ} (ht : ) :

### Lebesgue integral #

theorem ProbabilityTheory.kernel.lintegral_compProd' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) {f : βγENNReal} (hf : ) :
∫⁻ (bc : β × γ), f bc.1 bc.2 = ∫⁻ (b : β), ∫⁻ (c : γ), f b cη (a, b)κ a

Lebesgue integral against the composition-product of two kernels.

theorem ProbabilityTheory.kernel.lintegral_compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) {f : β × γENNReal} (hf : ) :
∫⁻ (bc : β × γ), f bc = ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c)η (a, b)κ a

Lebesgue integral against the composition-product of two kernels.

theorem ProbabilityTheory.kernel.lintegral_compProd₀ {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) {f : β × γENNReal} (hf : ) :
∫⁻ (z : β × γ), f z = ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y)η (a, x)κ a

Lebesgue integral against the composition-product of two kernels.

theorem ProbabilityTheory.kernel.set_lintegral_compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) {f : β × γENNReal} (hf : ) {s : Set β} {t : Set γ} (hs : ) (ht : ) :
∫⁻ (z : β × γ) in s ×ˢ t, f z = ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y)η (a, x)κ a
theorem ProbabilityTheory.kernel.set_lintegral_compProd_univ_right {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) {f : β × γENNReal} (hf : ) {s : Set β} (hs : ) :
∫⁻ (z : β × γ) in s ×ˢ Set.univ, f z = ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y)η (a, x)κ a
theorem ProbabilityTheory.kernel.set_lintegral_compProd_univ_left {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) {f : β × γENNReal} (hf : ) {t : Set γ} (ht : ) :
∫⁻ (z : β × γ) in Set.univ ×ˢ t, f z = ∫⁻ (x : β), ∫⁻ (y : γ) in t, f (x, y)η (a, x)κ a
theorem ProbabilityTheory.kernel.compProd_eq_tsum_compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {s : Set (β × γ)} (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) (hs : ) :
() s = ∑' (n : ) (m : ),
theorem ProbabilityTheory.kernel.compProd_eq_sum_compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) :
theorem ProbabilityTheory.kernel.compProd_eq_sum_compProd_left {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) :
theorem ProbabilityTheory.kernel.compProd_eq_sum_compProd_right {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) :
instance ProbabilityTheory.kernel.IsMarkovKernel.compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) :
Equations
• =
theorem ProbabilityTheory.kernel.compProd_apply_univ_le {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) (a : α) :
() Set.univ (κ a) Set.univ *
instance ProbabilityTheory.kernel.IsFiniteKernel.compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) :
Equations
• =
theorem ProbabilityTheory.kernel.compProd_add_left {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (μ : ()) (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) :
theorem ProbabilityTheory.kernel.compProd_add_right {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (μ : ()) (κ : (ProbabilityTheory.kernel (α × β) γ)) (η : (ProbabilityTheory.kernel (α × β) γ)) :
theorem ProbabilityTheory.kernel.comapRight_compProd_id_prod {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {δ : Type u_5} {mδ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) {f : δγ} (hf : ) :

### map, comap #

noncomputable def ProbabilityTheory.kernel.map {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (f : βγ) (hf : ) :
()

The pushforward of a kernel along a measurable function. We include measurability in the assumptions instead of using junk values to make sure that typeclass inference can infer that the map of a Markov kernel is again a Markov kernel.

Equations
• = fun (a : α) => ,
Instances For
theorem ProbabilityTheory.kernel.map_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {f : βγ} (κ : ()) (hf : ) (a : α) :
() a =
theorem ProbabilityTheory.kernel.map_apply' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {f : βγ} (κ : ()) (hf : ) (a : α) {s : Set γ} (hs : ) :
(() a) s = (κ a) (f ⁻¹' s)
@[simp]
theorem ProbabilityTheory.kernel.map_zero {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {f : βγ} (hf : ) :
= 0
@[simp]
theorem ProbabilityTheory.kernel.map_id {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :
= κ
@[simp]
theorem ProbabilityTheory.kernel.map_id' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :
ProbabilityTheory.kernel.map κ (fun (a : β) => a) = κ
theorem ProbabilityTheory.kernel.lintegral_map {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {f : βγ} (κ : ()) (hf : ) (a : α) {g' : γENNReal} (hg : ) :
∫⁻ (b : γ), g' b() a = ∫⁻ (a : β), g' (f a)κ a
theorem ProbabilityTheory.kernel.sum_map_seq {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {f : βγ} (κ : ()) (hf : ) :
instance ProbabilityTheory.kernel.IsMarkovKernel.map {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {f : βγ} (κ : ()) (hf : ) :
Equations
• =
instance ProbabilityTheory.kernel.IsFiniteKernel.map {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {f : βγ} (κ : ()) (hf : ) :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.map {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {f : βγ} (κ : ()) (hf : ) :
Equations
• =
@[simp]
theorem ProbabilityTheory.kernel.map_const {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (μ : ) {f : αβ} (hf : ) :
def ProbabilityTheory.kernel.comap {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (g : γα) (hg : ) :
()

Pullback of a kernel, such that for each set s comap κ g hg c s = κ (g c) s. We include measurability in the assumptions instead of using junk values to make sure that typeclass inference can infer that the comap of a Markov kernel is again a Markov kernel.

Equations
• = fun (a : γ) => κ (g a),
Instances For
theorem ProbabilityTheory.kernel.comap_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {g : γα} (κ : ()) (hg : ) (c : γ) :
() c = κ (g c)
theorem ProbabilityTheory.kernel.comap_apply' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {g : γα} (κ : ()) (hg : ) (c : γ) (s : Set β) :
(() c) s = (κ (g c)) s
@[simp]
theorem ProbabilityTheory.kernel.comap_zero {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {g : γα} (hg : ) :
= 0
@[simp]
theorem ProbabilityTheory.kernel.comap_id {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :
= κ
@[simp]
theorem ProbabilityTheory.kernel.comap_id' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :
ProbabilityTheory.kernel.comap κ (fun (a : α) => a) = κ
theorem ProbabilityTheory.kernel.lintegral_comap {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {g : γα} (κ : ()) (hg : ) (c : γ) (g' : βENNReal) :
∫⁻ (b : β), g' b() c = ∫⁻ (b : β), g' bκ (g c)
theorem ProbabilityTheory.kernel.sum_comap_seq {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {g : γα} (κ : ()) (hg : ) :
instance ProbabilityTheory.kernel.IsMarkovKernel.comap {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {g : γα} (κ : ()) (hg : ) :
Equations
• =
instance ProbabilityTheory.kernel.IsFiniteKernel.comap {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {g : γα} (κ : ()) (hg : ) :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.comap {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {g : γα} (κ : ()) (hg : ) :
Equations
• =
theorem ProbabilityTheory.kernel.comap_map_comm {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {δ : Type u_5} {mγ : } {mδ : } (κ : ()) {f : αβ} {g : γδ} (hf : ) (hg : ) :
=
def ProbabilityTheory.kernel.prodMkLeft {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (γ : Type u_5) [] (κ : ()) :

Define a kernel (γ × α) β from a kernel α β by taking the comap of the projection.

Equations
Instances For
def ProbabilityTheory.kernel.prodMkRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (γ : Type u_5) [] (κ : ()) :

Define a kernel (α × γ) β from a kernel α β by taking the comap of the projection.

Equations
Instances For
@[simp]
theorem ProbabilityTheory.kernel.prodMkLeft_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : ()) (ca : γ × α) :
= κ ca.2
@[simp]
theorem ProbabilityTheory.kernel.prodMkRight_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : ()) (ca : α × γ) :
= κ ca.1
theorem ProbabilityTheory.kernel.prodMkLeft_apply' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : ()) (ca : γ × α) (s : Set β) :
() s = (κ ca.2) s
theorem ProbabilityTheory.kernel.prodMkRight_apply' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : ()) (ca : α × γ) (s : Set β) :
() s = (κ ca.1) s
@[simp]
theorem ProbabilityTheory.kernel.prodMkLeft_zero {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } :
@[simp]
theorem ProbabilityTheory.kernel.prodMkRight_zero {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } :
@[simp]
theorem ProbabilityTheory.kernel.prodMkLeft_add {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : ()) (η : ()) :
@[simp]
theorem ProbabilityTheory.kernel.prodMkRight_add {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : ()) (η : ()) :
theorem ProbabilityTheory.kernel.lintegral_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : ()) (ca : γ × α) (g : βENNReal) :
∫⁻ (b : β), g b = ∫⁻ (b : β), g bκ ca.2
theorem ProbabilityTheory.kernel.lintegral_prodMkRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : ()) (ca : α × γ) (g : βENNReal) :
∫⁻ (b : β), g b = ∫⁻ (b : β), g bκ ca.1
instance ProbabilityTheory.kernel.IsMarkovKernel.prodMkLeft {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : ()) :
Equations
• =
instance ProbabilityTheory.kernel.IsMarkovKernel.prodMkRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : ()) :
Equations
• =
instance ProbabilityTheory.kernel.IsFiniteKernel.prodMkLeft {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : ()) :
Equations
• =
instance ProbabilityTheory.kernel.IsFiniteKernel.prodMkRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : ()) :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.prodMkLeft {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : ()) :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.prodMkRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : ()) :
Equations
• =
theorem ProbabilityTheory.kernel.map_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {δ : Type u_4} {mδ : } (γ : Type u_6) [] (κ : ()) {f : βδ} (hf : ) :
theorem ProbabilityTheory.kernel.map_prodMkRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {δ : Type u_4} {mδ : } (κ : ()) (γ : Type u_6) [] {f : βδ} (hf : ) :
def ProbabilityTheory.kernel.swapLeft {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel (α × β) γ)) :

Define a kernel (β × α) γ from a kernel (α × β) γ by taking the comap of Prod.swap.

Equations
Instances For
@[simp]
theorem ProbabilityTheory.kernel.swapLeft_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel (α × β) γ)) (a : β × α) :
= κ a.swap
theorem ProbabilityTheory.kernel.swapLeft_apply' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel (α × β) γ)) (a : β × α) (s : Set γ) :
s = (κ a.swap) s
theorem ProbabilityTheory.kernel.lintegral_swapLeft {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel (α × β) γ)) (a : β × α) (g : γENNReal) :
∫⁻ (c : γ), g c = ∫⁻ (c : γ), g cκ a.swap
instance ProbabilityTheory.kernel.IsMarkovKernel.swapLeft {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel (α × β) γ)) :
Equations
• =
instance ProbabilityTheory.kernel.IsFiniteKernel.swapLeft {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel (α × β) γ)) :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.swapLeft {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel (α × β) γ)) :
Equations
• =
@[simp]
theorem ProbabilityTheory.kernel.swapLeft_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) (γ : Type u_6) [] :
@[simp]
theorem ProbabilityTheory.kernel.swapLeft_prodMkRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) (γ : Type u_6) [] :
noncomputable def ProbabilityTheory.kernel.swapRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) :

Define a kernel α (γ × β) from a kernel α (β × γ) by taking the map of Prod.swap.

Equations
Instances For
theorem ProbabilityTheory.kernel.swapRight_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) (a : α) :
= MeasureTheory.Measure.map Prod.swap (κ a)
theorem ProbabilityTheory.kernel.swapRight_apply' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) (a : α) {s : Set (γ × β)} (hs : ) :
s = (κ a) {p : β × γ | p.swap s}
theorem ProbabilityTheory.kernel.lintegral_swapRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) (a : α) {g : γ × βENNReal} (hg : ) :
∫⁻ (c : γ × β), g c = ∫⁻ (bc : β × γ), g bc.swapκ a
instance ProbabilityTheory.kernel.IsMarkovKernel.swapRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) :
Equations
• =
instance ProbabilityTheory.kernel.IsFiniteKernel.swapRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.swapRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) :
Equations
• =
noncomputable def ProbabilityTheory.kernel.fst {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) :
()

Define a kernel α β from a kernel α (β × γ) by taking the map of the first projection.

Equations
Instances For
theorem ProbabilityTheory.kernel.fst_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) (a : α) :
= MeasureTheory.Measure.map Prod.fst (κ a)
theorem ProbabilityTheory.kernel.fst_apply' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) (a : α) {s : Set β} (hs : ) :
() s = (κ a) {p : β × γ | p.1 s}
@[simp]
theorem ProbabilityTheory.kernel.fst_zero {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } :
theorem ProbabilityTheory.kernel.lintegral_fst {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) (a : α) {g : βENNReal} (hg : ) :
∫⁻ (c : β), g c = ∫⁻ (bc : β × γ), g bc.1κ a
instance ProbabilityTheory.kernel.IsMarkovKernel.fst {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) :
Equations
• =
instance ProbabilityTheory.kernel.IsFiniteKernel.fst {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.fst {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) :
Equations
• =
@[instance 100]
instance ProbabilityTheory.kernel.isFiniteKernel_of_isFiniteKernel_fst {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } {κ : (ProbabilityTheory.kernel α (β × γ))} :
Equations
• =
theorem ProbabilityTheory.kernel.fst_map_prod {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {δ : Type u_4} {mδ : } {γ : Type u_5} {mγ : } (κ : ()) {f : βγ} {g : βδ} (hf : ) (hg : ) :
ProbabilityTheory.kernel.fst (ProbabilityTheory.kernel.map κ (fun (x : β) => (f x, g x)) ) =
theorem ProbabilityTheory.kernel.fst_map_id_prod {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) {γ : Type u_6} {mγ : } {f : βγ} (hf : ) :
ProbabilityTheory.kernel.fst (ProbabilityTheory.kernel.map κ (fun (a : β) => (a, f a)) ) = κ
@[simp]
theorem ProbabilityTheory.kernel.fst_compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : ()) (η : (ProbabilityTheory.kernel (α × β) γ)) :
theorem ProbabilityTheory.kernel.fst_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (δ : Type u_6) [] (κ : (ProbabilityTheory.kernel α (β × γ))) :
theorem ProbabilityTheory.kernel.fst_prodMkRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) (δ : Type u_6) [] :
noncomputable def ProbabilityTheory.kernel.snd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) :
()

Define a kernel α γ from a kernel α (β × γ) by taking the map of the second projection.

Equations
Instances For
theorem ProbabilityTheory.kernel.snd_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) (a : α) :
= MeasureTheory.Measure.map Prod.snd (κ a)
theorem ProbabilityTheory.kernel.snd_apply' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) (a : α) {s : Set γ} (hs : ) :
() s = (κ a) {p : β × γ | p.2 s}
@[simp]
theorem ProbabilityTheory.kernel.snd_zero {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } :
theorem ProbabilityTheory.kernel.lintegral_snd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) (a : α) {g : γENNReal} (hg : ) :
∫⁻ (c : γ), g c = ∫⁻ (bc : β × γ), g bc.2κ a
instance ProbabilityTheory.kernel.IsMarkovKernel.snd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) :
Equations
• =
instance ProbabilityTheory.kernel.IsFiniteKernel.snd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.snd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) :
Equations
• =
@[instance 100]
instance ProbabilityTheory.kernel.isFiniteKernel_of_isFiniteKernel_snd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } {κ : (ProbabilityTheory.kernel α (β × γ))} :
Equations
• =
theorem ProbabilityTheory.kernel.snd_map_prod {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {δ : Type u_4} {mδ : } {γ : Type u_5} {mγ : } (κ : ()) {f : βγ} {g : βδ} (hf : ) (hg : ) :
ProbabilityTheory.kernel.snd (ProbabilityTheory.kernel.map κ (fun (x : β) => (f x, g x)) ) =
theorem ProbabilityTheory.kernel.snd_map_prod_id {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) {γ : Type u_6} {mγ : } {f : βγ} (hf : ) :
ProbabilityTheory.kernel.snd (ProbabilityTheory.kernel.map κ (fun (a : β) => (f a, a)) ) = κ
theorem ProbabilityTheory.kernel.snd_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (δ : Type u_6) [] (κ : (ProbabilityTheory.kernel α (β × γ))) :
theorem ProbabilityTheory.kernel.snd_prodMkRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) (δ : Type u_6) [] :
@[simp]
theorem ProbabilityTheory.kernel.fst_swapRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) :
@[simp]
theorem ProbabilityTheory.kernel.snd_swapRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_5} {mγ : } (κ : (ProbabilityTheory.kernel α (β × γ))) :

### Composition of two kernels #

noncomputable def ProbabilityTheory.kernel.comp {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (η : ()) (κ : ()) :
()

Composition of two kernels.

Equations
• = fun (a : α) => (κ a).bind η,
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ProbabilityTheory.kernel.comp_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (η : ()) (κ : ()) (a : α) :
= (κ a).bind η
theorem ProbabilityTheory.kernel.comp_apply' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (η : ()) (κ : ()) (a : α) {s : Set γ} (hs : ) :
() s = ∫⁻ (b : β), (η b) sκ a
theorem ProbabilityTheory.kernel.comp_eq_snd_compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (η : ()) (κ : ()) :
theorem ProbabilityTheory.kernel.lintegral_comp {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (η : ()) (κ : ()) (a : α) {g : γENNReal} (hg : ) :
∫⁻ (c : γ), g c = ∫⁻ (b : β), ∫⁻ (c : γ), g cη bκ a
instance ProbabilityTheory.kernel.IsMarkovKernel.comp {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (η : ()) (κ : ()) :
Equations
• =
instance ProbabilityTheory.kernel.IsFiniteKernel.comp {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (η : ()) (κ : ()) :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.comp {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (η : ()) (κ : ()) :
Equations
• =
theorem ProbabilityTheory.kernel.comp_assoc {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {δ : Type u_5} {mδ : } (ξ : ()) (η : ()) (κ : ()) :

Composition of kernels is associative.

theorem ProbabilityTheory.kernel.deterministic_comp_eq_map {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {f : βγ} (hf : ) (κ : ()) :
theorem ProbabilityTheory.kernel.comp_deterministic_eq_comap {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {g : γα} (κ : ()) (hg : ) :

### Product of two kernels #

noncomputable def ProbabilityTheory.kernel.prod {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : ()) :

Product of two kernels. This is meaningful only when the kernels are s-finite.

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ProbabilityTheory.kernel.prod_apply' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : ()) (a : α) {s : Set (β × γ)} (hs : ) :
() s = ∫⁻ (b : β), (η a) {c : γ | (b, c) s}κ a
theorem ProbabilityTheory.kernel.prod_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : ()) (a : α) :
= (κ a).prod (η a)
theorem ProbabilityTheory.kernel.prod_const {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (μ : ) (ν : ) :
theorem ProbabilityTheory.kernel.lintegral_prod {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : ()) (a : α) {g : β × γENNReal} (hg : ) :
∫⁻ (c : β × γ), g c = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c)η aκ a
instance ProbabilityTheory.kernel.IsMarkovKernel.prod {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : ()) :
Equations
• =
instance ProbabilityTheory.kernel.IsFiniteKernel.prod {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : ()) :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.prod {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : ()) :
Equations
• =
@[simp]
theorem ProbabilityTheory.kernel.fst_prod {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : ()) :
@[simp]
theorem ProbabilityTheory.kernel.snd_prod {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } (κ : ()) (η : ()) :