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 . 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α : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) (a : α) (s : Set (β × γ)) : ENNReal

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.

theorem ProbabilityTheory.kernel.compProdFun_empty {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) (a : α) : ProbabilityTheory.kernel.compProdFun κ η a ∅ = 0

theorem ProbabilityTheory.kernel.compProdFun_iUnion {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (f : ℕ → Set (β × γ)) (hf_meas : ∀ (i : ℕ), MeasurableSet (f i)) (hf_disj : Pairwise (Disjoint on f)) : ProbabilityTheory.kernel.compProdFun κ η a (⋃ (i : ℕ), f i) = ∑' (i : ℕ), ProbabilityTheory.kernel.compProdFun κ η a (f i)

theorem ProbabilityTheory.kernel.compProdFun_tsum_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) : ProbabilityTheory.kernel.compProdFun κ η a s = ∑' (n : ℕ), ProbabilityTheory.kernel.compProdFun κ (ProbabilityTheory.kernel.seq η n) a s

theorem ProbabilityTheory.kernel.compProdFun_tsum_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel κ] (a : α) (s : Set (β × γ)) : ProbabilityTheory.kernel.compProdFun κ η a s = ∑' (n : ℕ), ProbabilityTheory.kernel.compProdFun (ProbabilityTheory.kernel.seq κ n) η a s

theorem ProbabilityTheory.kernel.compProdFun_eq_tsum {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) : ProbabilityTheory.kernel.compProdFun κ η a s = ∑' (n : ℕ) (m : ℕ), ProbabilityTheory.kernel.compProdFun (ProbabilityTheory.kernel.seq κ n) (ProbabilityTheory.kernel.seq η m) a s

theorem ProbabilityTheory.kernel.measurable_compProdFun_of_finite {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsFiniteKernel η] (hs : MeasurableSet s) : Measurable fun a => ProbabilityTheory.kernel.compProdFun κ η a s

Auxiliary lemma for measurable_compProdFun.

theorem ProbabilityTheory.kernel.measurable_compProdFun {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] (hs : MeasurableSet s) : Measurable fun a => ProbabilityTheory.kernel.compProdFun κ η a s

noncomputable def ProbabilityTheory.kernel.compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) : { x // x ∈ 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.

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

theorem ProbabilityTheory.kernel.compProd_apply_eq_compProdFun {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) : ↑↑(↑(ProbabilityTheory.kernel.compProd κ η) a) s = ProbabilityTheory.kernel.compProdFun κ η a s

theorem ProbabilityTheory.kernel.compProd_of_not_isSFiniteKernel_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) (h : ¬ProbabilityTheory.IsSFiniteKernel κ) : ProbabilityTheory.kernel.compProd κ η = 0

theorem ProbabilityTheory.kernel.compProd_of_not_isSFiniteKernel_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) (h : ¬ProbabilityTheory.IsSFiniteKernel η) : ProbabilityTheory.kernel.compProd κ η = 0

theorem ProbabilityTheory.kernel.compProd_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) : ↑↑(↑(ProbabilityTheory.kernel.compProd κ η) a) s = ∫⁻ (b : β), ↑↑(↑η (a, b)) {c | (b, c) ∈ s} ∂↑κ a

theorem ProbabilityTheory.kernel.le_compProd_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (s : Set (β × γ)) : ∫⁻ (b : β), ↑↑(↑η (a, b)) {c | (b, c) ∈ s} ∂↑κ a ≤ ↑↑(↑(ProbabilityTheory.kernel.compProd κ η) a) s

@[simp]

theorem ProbabilityTheory.kernel.compProd_zero_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) : ProbabilityTheory.kernel.compProd 0 κ = 0

@[simp]

theorem ProbabilityTheory.kernel.compProd_zero_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (γ : Type u_5) [MeasurableSpace γ] : ProbabilityTheory.kernel.compProd κ 0 = 0

ae filter of the composition-product

theorem ProbabilityTheory.kernel.ae_kernel_lt_top {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} {κ : { x // x ∈ ProbabilityTheory.kernel α β }} [ProbabilityTheory.IsSFiniteKernel κ] {η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }} [ProbabilityTheory.IsSFiniteKernel η] (a : α) (h2s : ↑↑(↑(ProbabilityTheory.kernel.compProd κ η) a) s ≠ ⊤) : ∀ᵐ (b : β) ∂↑κ a, ↑↑(↑η (a, b)) (Prod.mk b ⁻¹' s) < ⊤

theorem ProbabilityTheory.kernel.compProd_null {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} {κ : { x // x ∈ ProbabilityTheory.kernel α β }} [ProbabilityTheory.IsSFiniteKernel κ] {η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }} [ProbabilityTheory.IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) : ↑↑(↑(ProbabilityTheory.kernel.compProd κ η) a) s = 0 ↔ (fun b => ↑↑(↑η (a, b)) (Prod.mk b ⁻¹' s)) =ᶠ[MeasureTheory.Measure.ae (↑κ a)] 0

theorem ProbabilityTheory.kernel.ae_null_of_compProd_null {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} {κ : { x // x ∈ ProbabilityTheory.kernel α β }} [ProbabilityTheory.IsSFiniteKernel κ] {η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }} [ProbabilityTheory.IsSFiniteKernel η] {a : α} (h : ↑↑(↑(ProbabilityTheory.kernel.compProd κ η) a) s = 0) : (fun b => ↑↑(↑η (a, b)) (Prod.mk b ⁻¹' s)) =ᶠ[MeasureTheory.Measure.ae (↑κ a)] 0

theorem ProbabilityTheory.kernel.ae_ae_of_ae_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : { x // x ∈ ProbabilityTheory.kernel α β }} [ProbabilityTheory.IsSFiniteKernel κ] {η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }} [ProbabilityTheory.IsSFiniteKernel η] {a : α} {p : β × γ → Prop} (h : ∀ᵐ (bc : β × γ) ∂↑(ProbabilityTheory.kernel.compProd κ η) a, p bc) : ∀ᵐ (b : β) ∂↑κ a, ∀ᵐ (c : γ) ∂↑η (a, b), p (b, c)

theorem ProbabilityTheory.kernel.compProd_restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : { x // x ∈ ProbabilityTheory.kernel α β }} [ProbabilityTheory.IsSFiniteKernel κ] {η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }} [ProbabilityTheory.IsSFiniteKernel η] {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) : ProbabilityTheory.kernel.compProd (ProbabilityTheory.kernel.restrict κ hs) (ProbabilityTheory.kernel.restrict η ht) = ProbabilityTheory.kernel.restrict (ProbabilityTheory.kernel.compProd κ η) (_ : MeasurableSet (s ×ˢ t))

theorem ProbabilityTheory.kernel.compProd_restrict_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : { x // x ∈ ProbabilityTheory.kernel α β }} [ProbabilityTheory.IsSFiniteKernel κ] {η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }} [ProbabilityTheory.IsSFiniteKernel η] {s : Set β} (hs : MeasurableSet s) : ProbabilityTheory.kernel.compProd (ProbabilityTheory.kernel.restrict κ hs) η = ProbabilityTheory.kernel.restrict (ProbabilityTheory.kernel.compProd κ η) (_ : MeasurableSet (s ×ˢ Set.univ))

theorem ProbabilityTheory.kernel.compProd_restrict_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : { x // x ∈ ProbabilityTheory.kernel α β }} [ProbabilityTheory.IsSFiniteKernel κ] {η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }} [ProbabilityTheory.IsSFiniteKernel η] {t : Set γ} (ht : MeasurableSet t) : ProbabilityTheory.kernel.compProd κ (ProbabilityTheory.kernel.restrict η ht) = ProbabilityTheory.kernel.restrict (ProbabilityTheory.kernel.compProd κ η) (_ : MeasurableSet (Set.univ ×ˢ t))

Lebesgue integral

theorem ProbabilityTheory.kernel.lintegral_compProd' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β → γ → ENNReal} (hf : Measurable (Function.uncurry f)) : ∫⁻ (bc : β × γ), f bc.fst bc.snd ∂↑(ProbabilityTheory.kernel.compProd κ η) a = ∫⁻ (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α : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γ → ENNReal} (hf : Measurable f) : ∫⁻ (bc : β × γ), f bc ∂↑(ProbabilityTheory.kernel.compProd κ η) a = ∫⁻ (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α : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γ → ENNReal} (hf : AEMeasurable f) : ∫⁻ (z : β × γ), f z ∂↑(ProbabilityTheory.kernel.compProd κ η) a = ∫⁻ (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α : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γ → ENNReal} (hf : Measurable f) {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) : ∫⁻ (z : β × γ) in s ×ˢ t, f z ∂↑(ProbabilityTheory.kernel.compProd κ η) a = ∫⁻ (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α : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γ → ENNReal} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) : ∫⁻ (z : β × γ) in s ×ˢ Set.univ, f z ∂↑(ProbabilityTheory.kernel.compProd κ η) a = ∫⁻ (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α : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γ → ENNReal} (hf : Measurable f) {t : Set γ} (ht : MeasurableSet t) : ∫⁻ (z : β × γ) in Set.univ ×ˢ t, f z ∂↑(ProbabilityTheory.kernel.compProd κ η) a = ∫⁻ (x : β), ∫⁻ (y : γ) in t, f (x, y) ∂↑η (a, x) ∂↑κ a

theorem ProbabilityTheory.kernel.compProd_eq_tsum_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) : ↑↑(↑(ProbabilityTheory.kernel.compProd κ η) a) s = ∑' (n : ℕ) (m : ℕ), ↑↑(↑(ProbabilityTheory.kernel.compProd (ProbabilityTheory.kernel.seq κ n) (ProbabilityTheory.kernel.seq η m)) a) s

theorem ProbabilityTheory.kernel.compProd_eq_sum_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] : ProbabilityTheory.kernel.compProd κ η = ProbabilityTheory.kernel.sum fun n => ProbabilityTheory.kernel.sum fun m => ProbabilityTheory.kernel.compProd (ProbabilityTheory.kernel.seq κ n) (ProbabilityTheory.kernel.seq η m)

theorem ProbabilityTheory.kernel.compProd_eq_sum_compProd_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) : ProbabilityTheory.kernel.compProd κ η = ProbabilityTheory.kernel.sum fun n => ProbabilityTheory.kernel.compProd (ProbabilityTheory.kernel.seq κ n) η

theorem ProbabilityTheory.kernel.compProd_eq_sum_compProd_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel η] : ProbabilityTheory.kernel.compProd κ η = ProbabilityTheory.kernel.sum fun n => ProbabilityTheory.kernel.compProd κ (ProbabilityTheory.kernel.seq η n)

instance ProbabilityTheory.kernel.IsMarkovKernel.compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsMarkovKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsMarkovKernel η] : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.compProd κ η)

theorem ProbabilityTheory.kernel.compProd_apply_univ_le {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsFiniteKernel η] (a : α) : ↑↑(↑(ProbabilityTheory.kernel.compProd κ η) a) Set.univ ≤ ↑↑(↑κ a) Set.univ * ProbabilityTheory.IsFiniteKernel.bound η

instance ProbabilityTheory.kernel.IsFiniteKernel.compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.compProd κ η)

instance ProbabilityTheory.kernel.IsSFiniteKernel.compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (η : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.compProd κ η)

map, comap

noncomputable def ProbabilityTheory.kernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (f : β → γ) (hf : Measurable f) : { x // x ∈ ProbabilityTheory.kernel α γ }

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.

theorem ProbabilityTheory.kernel.map_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : β → γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (hf : Measurable f) (a : α) : ↑(ProbabilityTheory.kernel.map κ f hf) a = MeasureTheory.Measure.map f (↑κ a)

theorem ProbabilityTheory.kernel.map_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : β → γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (hf : Measurable f) (a : α) {s : Set γ} (hs : MeasurableSet s) : ↑↑(↑(ProbabilityTheory.kernel.map κ f hf) a) s = ↑↑(↑κ a) (f ⁻¹' s)

@[simp]

theorem ProbabilityTheory.kernel.map_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : β → γ} (hf : Measurable f) : ProbabilityTheory.kernel.map 0 f hf = 0

theorem ProbabilityTheory.kernel.lintegral_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : β → γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (hf : Measurable f) (a : α) {g' : γ → ENNReal} (hg : Measurable g') : ∫⁻ (b : γ), g' b ∂↑(ProbabilityTheory.kernel.map κ f hf) a = ∫⁻ (a : β), g' (f a) ∂↑κ a

theorem ProbabilityTheory.kernel.sum_map_seq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : β → γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (hf : Measurable f) : (ProbabilityTheory.kernel.sum fun n => ProbabilityTheory.kernel.map (ProbabilityTheory.kernel.seq κ n) f hf) = ProbabilityTheory.kernel.map κ f hf

instance ProbabilityTheory.kernel.IsMarkovKernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : β → γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsMarkovKernel κ] (hf : Measurable f) : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.map κ f hf)

instance ProbabilityTheory.kernel.IsFiniteKernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : β → γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsFiniteKernel κ] (hf : Measurable f) : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.map κ f hf)

instance ProbabilityTheory.kernel.IsSFiniteKernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : β → γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (hf : Measurable f) : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.map κ f hf)

def ProbabilityTheory.kernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (g : γ → α) (hg : Measurable g) : { x // x ∈ ProbabilityTheory.kernel γ β }

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.

theorem ProbabilityTheory.kernel.comap_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (hg : Measurable g) (c : γ) : ↑(ProbabilityTheory.kernel.comap κ g hg) c = ↑κ (g c)

theorem ProbabilityTheory.kernel.comap_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (hg : Measurable g) (c : γ) (s : Set β) : ↑↑(↑(ProbabilityTheory.kernel.comap κ g hg) c) s = ↑↑(↑κ (g c)) s

@[simp]

theorem ProbabilityTheory.kernel.comap_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γ → α} (hg : Measurable g) : ProbabilityTheory.kernel.comap 0 g hg = 0

theorem ProbabilityTheory.kernel.lintegral_comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (hg : Measurable g) (c : γ) (g' : β → ENNReal) : ∫⁻ (b : β), g' b ∂↑(ProbabilityTheory.kernel.comap κ g hg) c = ∫⁻ (b : β), g' b ∂↑κ (g c)

theorem ProbabilityTheory.kernel.sum_comap_seq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (hg : Measurable g) : (ProbabilityTheory.kernel.sum fun n => ProbabilityTheory.kernel.comap (ProbabilityTheory.kernel.seq κ n) g hg) = ProbabilityTheory.kernel.comap κ g hg

instance ProbabilityTheory.kernel.IsMarkovKernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsMarkovKernel κ] (hg : Measurable g) : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.comap κ g hg)

instance ProbabilityTheory.kernel.IsFiniteKernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsFiniteKernel κ] (hg : Measurable g) : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.comap κ g hg)

instance ProbabilityTheory.kernel.IsSFiniteKernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (hg : Measurable g) : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.comap κ g hg)

def ProbabilityTheory.kernel.prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (γ : Type u_4) [MeasurableSpace γ] (κ : { x // x ∈ ProbabilityTheory.kernel α β }) : { x // x ∈ ProbabilityTheory.kernel (γ × α) β }

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

theorem ProbabilityTheory.kernel.prodMkLeft_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (ca : γ × α) : ↑(ProbabilityTheory.kernel.prodMkLeft γ κ) ca = ↑κ ca.snd

theorem ProbabilityTheory.kernel.prodMkLeft_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (ca : γ × α) (s : Set β) : ↑↑(↑(ProbabilityTheory.kernel.prodMkLeft γ κ) ca) s = ↑↑(↑κ ca.snd) s

theorem ProbabilityTheory.kernel.lintegral_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (ca : γ × α) (g : β → ENNReal) : ∫⁻ (b : β), g b ∂↑(ProbabilityTheory.kernel.prodMkLeft γ κ) ca = ∫⁻ (b : β), g b ∂↑κ ca.snd

instance ProbabilityTheory.kernel.IsMarkovKernel.prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsMarkovKernel κ] : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.prodMkLeft γ κ)

instance ProbabilityTheory.kernel.IsFiniteKernel.prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.prodMkLeft γ κ)

instance ProbabilityTheory.kernel.IsSFiniteKernel.prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.prodMkLeft γ κ)

def ProbabilityTheory.kernel.swapLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) : { x // x ∈ ProbabilityTheory.kernel (β × α) γ }

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

theorem ProbabilityTheory.kernel.swapLeft_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) (a : β × α) : ↑(ProbabilityTheory.kernel.swapLeft κ) a = ↑κ (Prod.swap a)

theorem ProbabilityTheory.kernel.swapLeft_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) (a : β × α) (s : Set γ) : ↑↑(↑(ProbabilityTheory.kernel.swapLeft κ) a) s = ↑↑(↑κ (Prod.swap a)) s

theorem ProbabilityTheory.kernel.lintegral_swapLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) (a : β × α) (g : γ → ENNReal) : ∫⁻ (c : γ), g c ∂↑(ProbabilityTheory.kernel.swapLeft κ) a = ∫⁻ (c : γ), g c ∂↑κ (Prod.swap a)

instance ProbabilityTheory.kernel.IsMarkovKernel.swapLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsMarkovKernel κ] : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.swapLeft κ)

instance ProbabilityTheory.kernel.IsFiniteKernel.swapLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.swapLeft κ)

instance ProbabilityTheory.kernel.IsSFiniteKernel.swapLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel (α × β) γ }) [ProbabilityTheory.IsSFiniteKernel κ] : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.swapLeft κ)

noncomputable def ProbabilityTheory.kernel.swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) : { x // x ∈ ProbabilityTheory.kernel α (γ × β) }

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

theorem ProbabilityTheory.kernel.swapRight_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) (a : α) : ↑(ProbabilityTheory.kernel.swapRight κ) a = MeasureTheory.Measure.map Prod.swap (↑κ a)

theorem ProbabilityTheory.kernel.swapRight_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) (a : α) {s : Set (γ × β)} (hs : MeasurableSet s) : ↑↑(↑(ProbabilityTheory.kernel.swapRight κ) a) s = ↑↑(↑κ a) {p | Prod.swap p ∈ s}

theorem ProbabilityTheory.kernel.lintegral_swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) (a : α) {g : γ × β → ENNReal} (hg : Measurable g) : ∫⁻ (c : γ × β), g c ∂↑(ProbabilityTheory.kernel.swapRight κ) a = ∫⁻ (bc : β × γ), g (Prod.swap bc) ∂↑κ a

instance ProbabilityTheory.kernel.IsMarkovKernel.swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) [ProbabilityTheory.IsMarkovKernel κ] : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.swapRight κ)

instance ProbabilityTheory.kernel.IsFiniteKernel.swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.swapRight κ)

instance ProbabilityTheory.kernel.IsSFiniteKernel.swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) [ProbabilityTheory.IsSFiniteKernel κ] : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.swapRight κ)

noncomputable def ProbabilityTheory.kernel.fst {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) : { x // x ∈ ProbabilityTheory.kernel α β }

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

theorem ProbabilityTheory.kernel.fst_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) (a : α) : ↑(ProbabilityTheory.kernel.fst κ) a = MeasureTheory.Measure.map Prod.fst (↑κ a)

theorem ProbabilityTheory.kernel.fst_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) (a : α) {s : Set β} (hs : MeasurableSet s) : ↑↑(↑(ProbabilityTheory.kernel.fst κ) a) s = ↑↑(↑κ a) {p | p.fst ∈ s}

theorem ProbabilityTheory.kernel.lintegral_fst {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) (a : α) {g : β → ENNReal} (hg : Measurable g) : ∫⁻ (c : β), g c ∂↑(ProbabilityTheory.kernel.fst κ) a = ∫⁻ (bc : β × γ), g bc.fst ∂↑κ a

instance ProbabilityTheory.kernel.IsMarkovKernel.fst {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) [ProbabilityTheory.IsMarkovKernel κ] : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.fst κ)

instance ProbabilityTheory.kernel.IsFiniteKernel.fst {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.fst κ)

instance ProbabilityTheory.kernel.IsSFiniteKernel.fst {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) [ProbabilityTheory.IsSFiniteKernel κ] : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.fst κ)

noncomputable def ProbabilityTheory.kernel.snd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) : { x // x ∈ ProbabilityTheory.kernel α γ }

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

theorem ProbabilityTheory.kernel.snd_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) (a : α) : ↑(ProbabilityTheory.kernel.snd κ) a = MeasureTheory.Measure.map Prod.snd (↑κ a)

theorem ProbabilityTheory.kernel.snd_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) (a : α) {s : Set γ} (hs : MeasurableSet s) : ↑↑(↑(ProbabilityTheory.kernel.snd κ) a) s = ↑↑(↑κ a) {p | p.snd ∈ s}

theorem ProbabilityTheory.kernel.lintegral_snd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) (a : α) {g : γ → ENNReal} (hg : Measurable g) : ∫⁻ (c : γ), g c ∂↑(ProbabilityTheory.kernel.snd κ) a = ∫⁻ (bc : β × γ), g bc.snd ∂↑κ a

instance ProbabilityTheory.kernel.IsMarkovKernel.snd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) [ProbabilityTheory.IsMarkovKernel κ] : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.snd κ)

instance ProbabilityTheory.kernel.IsFiniteKernel.snd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.snd κ)

instance ProbabilityTheory.kernel.IsSFiniteKernel.snd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α (β × γ) }) [ProbabilityTheory.IsSFiniteKernel κ] : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.snd κ)

Composition of two kernels

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

Composition of two kernels.

def ProbabilityTheory.«term_∘ₖ_» : Lean.TrailingParserDescr

theorem ProbabilityTheory.kernel.comp_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (η : { x // x ∈ ProbabilityTheory.kernel β γ }) (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (a : α) : ↑(ProbabilityTheory.kernel.comp η κ) a = MeasureTheory.Measure.bind (↑κ a) ↑η

theorem ProbabilityTheory.kernel.comp_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (η : { x // x ∈ ProbabilityTheory.kernel β γ }) (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (a : α) {s : Set γ} (hs : MeasurableSet s) : ↑↑(↑(ProbabilityTheory.kernel.comp η κ) a) s = ∫⁻ (b : β), ↑↑(↑η b) s ∂↑κ a

theorem ProbabilityTheory.kernel.comp_eq_snd_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (η : { x // x ∈ ProbabilityTheory.kernel β γ }) [ProbabilityTheory.IsSFiniteKernel η] (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] : ProbabilityTheory.kernel.comp η κ = ProbabilityTheory.kernel.snd (ProbabilityTheory.kernel.compProd κ (ProbabilityTheory.kernel.prodMkLeft α η))

theorem ProbabilityTheory.kernel.lintegral_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (η : { x // x ∈ ProbabilityTheory.kernel β γ }) (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (a : α) {g : γ → ENNReal} (hg : Measurable g) : ∫⁻ (c : γ), g c ∂↑(ProbabilityTheory.kernel.comp η κ) a = ∫⁻ (b : β), ∫⁻ (c : γ), g c ∂↑η b ∂↑κ a

instance ProbabilityTheory.kernel.IsMarkovKernel.comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (η : { x // x ∈ ProbabilityTheory.kernel β γ }) [ProbabilityTheory.IsMarkovKernel η] (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsMarkovKernel κ] : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.comp η κ)

instance ProbabilityTheory.kernel.IsFiniteKernel.comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (η : { x // x ∈ ProbabilityTheory.kernel β γ }) [ProbabilityTheory.IsFiniteKernel η] (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.comp η κ)

instance ProbabilityTheory.kernel.IsSFiniteKernel.comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (η : { x // x ∈ ProbabilityTheory.kernel β γ }) [ProbabilityTheory.IsSFiniteKernel η] (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.comp η κ)

theorem ProbabilityTheory.kernel.comp_assoc {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {δ : Type u_5} {mδ : MeasurableSpace δ} (ξ : { x // x ∈ ProbabilityTheory.kernel γ δ }) [ProbabilityTheory.IsSFiniteKernel ξ] (η : { x // x ∈ ProbabilityTheory.kernel β γ }) (κ : { x // x ∈ ProbabilityTheory.kernel α β }) : ProbabilityTheory.kernel.comp (ProbabilityTheory.kernel.comp ξ η) κ = ProbabilityTheory.kernel.comp ξ (ProbabilityTheory.kernel.comp η κ)

Composition of kernels is associative.

theorem ProbabilityTheory.kernel.deterministic_comp_eq_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : β → γ} (hf : Measurable f) (κ : { x // x ∈ ProbabilityTheory.kernel α β }) : ProbabilityTheory.kernel.comp (ProbabilityTheory.kernel.deterministic f hf) κ = ProbabilityTheory.kernel.map κ f hf

theorem ProbabilityTheory.kernel.comp_deterministic_eq_comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (hg : Measurable g) : ProbabilityTheory.kernel.comp κ (ProbabilityTheory.kernel.deterministic g hg) = ProbabilityTheory.kernel.comap κ g hg

Product of two kernels

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

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

def ProbabilityTheory.«term_×ₖ_» : Lean.TrailingParserDescr

theorem ProbabilityTheory.kernel.prod_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel α γ }) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {s : Set (β × γ)} (hs : MeasurableSet s) : ↑↑(↑(ProbabilityTheory.kernel.prod κ η) a) s = ∫⁻ (b : β), ↑↑(↑η a) {c | (b, c) ∈ s} ∂↑κ a

theorem ProbabilityTheory.kernel.lintegral_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsSFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel α γ }) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {g : β × γ → ENNReal} (hg : Measurable g) : ∫⁻ (c : β × γ), g c ∂↑(ProbabilityTheory.kernel.prod κ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂↑η a ∂↑κ a

instance ProbabilityTheory.kernel.IsMarkovKernel.prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsMarkovKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel α γ }) [ProbabilityTheory.IsMarkovKernel η] : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.kernel.prod κ η)

instance ProbabilityTheory.kernel.IsFiniteKernel.prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) [ProbabilityTheory.IsFiniteKernel κ] (η : { x // x ∈ ProbabilityTheory.kernel α γ }) [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.prod κ η)

instance ProbabilityTheory.kernel.IsSFiniteKernel.prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : { x // x ∈ ProbabilityTheory.kernel α β }) (η : { x // x ∈ ProbabilityTheory.kernel α γ }) : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.prod κ η)