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 [Kal21] 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 : β → γ) : Kernel α γ ∫⁻ c, g c ∂(map κ f 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α : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : 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.

Equations

• κ.compProdFun η a s = ∫⁻ (b : β), (η (a, b)) {c : γ | (b, c) ∈ s} ∂κ a

theorem ProbabilityTheory.Kernel.compProdFun_empty {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel (α × β) γ) (a : α) : κ.compProdFun η a ∅ = 0

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

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

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

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

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

@[deprecated ProbabilityTheory.Kernel.measurable_compProdFun (since := "2024-08-30")]

theorem ProbabilityTheory.Kernel.measurable_compProdFun_of_finite {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) [IsSFiniteKernel η] (hs : MeasurableSet s) : Measurable fun (a : α) => κ.compProdFun η a s

Alias of ProbabilityTheory.Kernel.measurable_compProdFun.

noncomputable def ProbabilityTheory.Kernel.compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {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.

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.

theorem ProbabilityTheory.Kernel.compProd_apply_eq_compProdFun {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) [IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) : ((κ.compProd η) a) s = κ.compProdFun η a s

theorem ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel (α × β) γ) (h : ¬IsSFiniteKernel κ) : κ.compProd η = 0

theorem ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel (α × β) γ) (h : ¬IsSFiniteKernel η) : κ.compProd η = 0

theorem ProbabilityTheory.Kernel.compProd_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (hs : MeasurableSet s) (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) [IsSFiniteKernel η] (a : α) : ((κ.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_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) [IsSFiniteKernel η] (a : α) (s : Set (β × γ)) : ∫⁻ (b : β), (η (a, b)) {c : γ | (b, c) ∈ s} ∂κ a ≤ ((κ.compProd η) a) s

@[simp]

theorem ProbabilityTheory.Kernel.compProd_zero_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) : compProd 0 κ = 0

@[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

theorem ProbabilityTheory.Kernel.compProd_preimage_fst {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {s : Set β} (hs : MeasurableSet s) (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel κ] [IsMarkovKernel η] (x : α) : ((κ.compProd η) x) (Prod.fst ⁻¹' s) = (κ x) s

theorem ProbabilityTheory.Kernel.compProd_deterministic_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {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

theorem ProbabilityTheory.Kernel.ae_kernel_lt_top {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {s : Set (β × γ)} {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel (α × β) γ} [IsSFiniteKernel η] (a : α) (h2s : ((κ.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_3} {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

theorem ProbabilityTheory.Kernel.ae_null_of_compProd_null {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {s : Set (β × γ)} {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel (α × β) γ} [IsSFiniteKernel η] {a : α} (h : ((κ.compProd η) a) s = 0) : (fun (b : β) => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0

theorem ProbabilityTheory.Kernel.ae_ae_of_ae_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel (α × β) γ} [IsSFiniteKernel η] {a : α} {p : β × γ → Prop} (h : ∀ᵐ (bc : β × γ) ∂(κ.compProd η) a, 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α : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {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

theorem ProbabilityTheory.Kernel.ae_compProd_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {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)

theorem ProbabilityTheory.Kernel.compProd_restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel (α × β) γ} [IsSFiniteKernel η] {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) : (κ.restrict hs).compProd (η.restrict ht) = (κ.compProd η).restrict ⋯

theorem ProbabilityTheory.Kernel.compProd_restrict_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel (α × β) γ} [IsSFiniteKernel η] {s : Set β} (hs : MeasurableSet s) : (κ.restrict hs).compProd η = (κ.compProd η).restrict ⋯

theorem ProbabilityTheory.Kernel.compProd_restrict_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel (α × β) γ} [IsSFiniteKernel η] {t : Set γ} (ht : MeasurableSet t) : κ.compProd (η.restrict ht) = (κ.compProd η).restrict ⋯

Lebesgue integral

theorem ProbabilityTheory.Kernel.lintegral_compProd' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {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.

theorem ProbabilityTheory.Kernel.lintegral_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {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.

theorem ProbabilityTheory.Kernel.lintegral_compProd₀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {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.

theorem ProbabilityTheory.Kernel.setLIntegral_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {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

@[deprecated ProbabilityTheory.Kernel.setLIntegral_compProd (since := "2024-06-29")]

theorem ProbabilityTheory.Kernel.set_lintegral_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {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

Alias of ProbabilityTheory.Kernel.setLIntegral_compProd.

theorem ProbabilityTheory.Kernel.setLIntegral_compProd_univ_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {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

@[deprecated ProbabilityTheory.Kernel.setLIntegral_compProd_univ_right (since := "2024-06-29")]

theorem ProbabilityTheory.Kernel.set_lintegral_compProd_univ_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {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

Alias of ProbabilityTheory.Kernel.setLIntegral_compProd_univ_right.

theorem ProbabilityTheory.Kernel.setLIntegral_compProd_univ_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {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

@[deprecated ProbabilityTheory.Kernel.setLIntegral_compProd_univ_left (since := "2024-06-29")]

theorem ProbabilityTheory.Kernel.set_lintegral_compProd_univ_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {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

Alias of ProbabilityTheory.Kernel.setLIntegral_compProd_univ_left.

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

theorem ProbabilityTheory.Kernel.compProd_eq_sum_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) [IsSFiniteKernel η] : κ.compProd η = Kernel.sum fun (n : ℕ) => Kernel.sum fun (m : ℕ) => (κ.seq n).compProd (η.seq m)

theorem ProbabilityTheory.Kernel.compProd_eq_sum_compProd_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) : κ.compProd η = Kernel.sum fun (n : ℕ) => (κ.seq n).compProd η

theorem ProbabilityTheory.Kernel.compProd_eq_sum_compProd_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel η] : κ.compProd η = Kernel.sum fun (n : ℕ) => κ.compProd (η.seq n)

instance ProbabilityTheory.Kernel.IsMarkovKernel.compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsMarkovKernel κ] (η : Kernel (α × β) γ) [IsMarkovKernel η] : IsMarkovKernel (κ.compProd η)

theorem ProbabilityTheory.Kernel.compProd_apply_univ_le {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel (α × β) γ) [IsFiniteKernel η] (a : α) : ((κ.compProd η) a) Set.univ ≤ (κ a) Set.univ * IsFiniteKernel.bound η

instance ProbabilityTheory.Kernel.IsFiniteKernel.compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsFiniteKernel κ] (η : Kernel (α × β) γ) [IsFiniteKernel η] : IsFiniteKernel (κ.compProd η)

instance ProbabilityTheory.Kernel.IsSFiniteKernel.compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel (α × β) γ) : IsSFiniteKernel (κ.compProd η)

theorem ProbabilityTheory.Kernel.compProd_add_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (μ κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel μ] [IsSFiniteKernel κ] [IsSFiniteKernel η] : (μ + κ).compProd η = μ.compProd η + κ.compProd η

theorem ProbabilityTheory.Kernel.compProd_add_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (μ : Kernel α β) (κ η : Kernel (α × β) γ) [IsSFiniteKernel μ] [IsSFiniteKernel κ] [IsSFiniteKernel η] : μ.compProd (κ + η) = μ.compProd κ + μ.compProd η

theorem ProbabilityTheory.Kernel.comapRight_compProd_id_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {δ : Type u_4} {mδ : MeasurableSpace δ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) [IsSFiniteKernel η] {f : δ → γ} (hf : MeasurableEmbedding f) : (κ.compProd η).comapRight ⋯ = κ.compProd (η.comapRight hf)

map, comap

noncomputable def ProbabilityTheory.Kernel.mapOfMeasurable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) (f : β → γ) (hf : Measurable f) : Kernel α γ

The pushforward of a kernel along a measurable function. This is an implementation detail, use map κ f instead.

Equations

• κ.mapOfMeasurable f hf = { toFun := fun (a : α) => MeasureTheory.Measure.map f (κ a), measurable' := ⋯ }

noncomputable def ProbabilityTheory.Kernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} [MeasurableSpace γ] (κ : Kernel α β) (f : β → γ) : Kernel α γ

The pushforward of a kernel along a function. If the function is not measurable, we use zero instead. This choice of junk value ensures that typeclass inference can infer that the map of a kernel satisfying IsZeroOrMarkovKernel again satisfies this property.

Equations

• κ.map f = if hf : Measurable f then κ.mapOfMeasurable f hf else 0

theorem ProbabilityTheory.Kernel.map_of_not_measurable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) {f : β → γ} (hf : ¬Measurable f) : κ.map f = 0

@[simp]

theorem ProbabilityTheory.Kernel.mapOfMeasurable_eq_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) {f : β → γ} (hf : Measurable f) : κ.mapOfMeasurable f hf = κ.map f

theorem ProbabilityTheory.Kernel.map_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {f : β → γ} (κ : Kernel α β) (hf : Measurable f) (a : α) : (κ.map f) a = MeasureTheory.Measure.map f (κ a)

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

@[simp]

theorem ProbabilityTheory.Kernel.map_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {f : β → γ} : map 0 f = 0

@[simp]

theorem ProbabilityTheory.Kernel.map_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : κ.map id = κ

@[simp]

theorem ProbabilityTheory.Kernel.map_id' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : (κ.map fun (a : β) => a) = κ

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

theorem ProbabilityTheory.Kernel.sum_map_seq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] (f : β → γ) : (Kernel.sum fun (n : ℕ) => (κ.seq n).map f) = κ.map f

theorem ProbabilityTheory.Kernel.IsMarkovKernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {f : β → γ} (κ : Kernel α β) [IsMarkovKernel κ] (hf : Measurable f) : IsMarkovKernel (κ.map f)

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsZeroOrMarkovKernel κ] (f : β → γ) : IsZeroOrMarkovKernel (κ.map f)

instance ProbabilityTheory.Kernel.IsFiniteKernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsFiniteKernel κ] (f : β → γ) : IsFiniteKernel (κ.map f)

instance ProbabilityTheory.Kernel.IsSFiniteKernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] (f : β → γ) : IsSFiniteKernel (κ.map f)

@[simp]

theorem ProbabilityTheory.Kernel.map_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure α) {f : α → β} (hf : Measurable f) : (const γ μ).map f = const γ (MeasureTheory.Measure.map f μ)

def ProbabilityTheory.Kernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) (g : γ → α) (hg : Measurable g) : 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.

Equations

• κ.comap g hg = { toFun := fun (a : γ) => κ (g a), measurable' := ⋯ }

@[simp]

theorem ProbabilityTheory.Kernel.coe_comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) (g : γ → α) (hg : Measurable g) : ⇑(κ.comap g hg) = ⇑κ ∘ g

theorem ProbabilityTheory.Kernel.comap_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {g : γ → α} (κ : Kernel α β) (hg : Measurable g) (c : γ) : (κ.comap g hg) c = κ (g c)

theorem ProbabilityTheory.Kernel.comap_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {g : γ → α} (κ : Kernel α β) (hg : Measurable g) (c : γ) (s : Set β) : ((κ.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_3} {mγ : MeasurableSpace γ} {g : γ → α} (hg : Measurable g) : comap 0 g hg = 0

@[simp]

theorem ProbabilityTheory.Kernel.comap_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : κ.comap id ⋯ = κ

@[simp]

theorem ProbabilityTheory.Kernel.comap_id' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : κ.comap (fun (a : α) => a) ⋯ = κ

theorem ProbabilityTheory.Kernel.lintegral_comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {g : γ → α} (κ : Kernel α β) (hg : Measurable g) (c : γ) (g' : β → ENNReal) : ∫⁻ (b : β), g' b ∂(κ.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_3} {mγ : MeasurableSpace γ} {g : γ → α} (κ : Kernel α β) [IsSFiniteKernel κ] (hg : Measurable g) : (Kernel.sum fun (n : ℕ) => (κ.seq n).comap g hg) = κ.comap g hg

instance ProbabilityTheory.Kernel.IsMarkovKernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {g : γ → α} (κ : Kernel α β) [IsMarkovKernel κ] (hg : Measurable g) : IsMarkovKernel (κ.comap g hg)

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {g : γ → α} (κ : Kernel α β) [IsZeroOrMarkovKernel κ] (hg : Measurable g) : IsZeroOrMarkovKernel (κ.comap g hg)

instance ProbabilityTheory.Kernel.IsFiniteKernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {g : γ → α} (κ : Kernel α β) [IsFiniteKernel κ] (hg : Measurable g) : IsFiniteKernel (κ.comap g hg)

instance ProbabilityTheory.Kernel.IsSFiniteKernel.comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {g : γ → α} (κ : Kernel α β) [IsSFiniteKernel κ] (hg : Measurable g) : IsSFiniteKernel (κ.comap g hg)

theorem ProbabilityTheory.Kernel.comap_map_comm {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {δ : Type u_4} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel β γ) {f : α → β} {g : γ → δ} (hf : Measurable f) (hg : Measurable g) : (κ.map g).comap f hf = (κ.comap f hf).map g

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

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

Equations

• ProbabilityTheory.Kernel.prodMkLeft γ κ = κ.comap Prod.snd ⋯

def ProbabilityTheory.Kernel.prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (γ : Type u_4) [MeasurableSpace γ] (κ : Kernel α β) : Kernel (α × γ) β

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

Equations

• ProbabilityTheory.Kernel.prodMkRight γ κ = κ.comap Prod.fst ⋯

@[simp]

theorem ProbabilityTheory.Kernel.prodMkLeft_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) (ca : γ × α) : (prodMkLeft γ κ) ca = κ ca.2

@[simp]

theorem ProbabilityTheory.Kernel.prodMkRight_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) (ca : α × γ) : (prodMkRight γ κ) ca = κ ca.1

theorem ProbabilityTheory.Kernel.prodMkLeft_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) (ca : γ × α) (s : Set β) : ((prodMkLeft γ κ) ca) s = (κ ca.2) s

theorem ProbabilityTheory.Kernel.prodMkRight_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) (ca : α × γ) (s : Set β) : ((prodMkRight γ κ) ca) s = (κ ca.1) s

@[simp]

theorem ProbabilityTheory.Kernel.prodMkLeft_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} : prodMkLeft α 0 = 0

@[simp]

theorem ProbabilityTheory.Kernel.prodMkRight_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} : prodMkRight α 0 = 0

@[simp]

theorem ProbabilityTheory.Kernel.prodMkLeft_add {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ η : Kernel α β) : prodMkLeft γ (κ + η) = prodMkLeft γ κ + prodMkLeft γ η

@[simp]

theorem ProbabilityTheory.Kernel.prodMkRight_add {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ η : Kernel α β) : prodMkRight γ (κ + η) = prodMkRight γ κ + prodMkRight γ η

theorem ProbabilityTheory.Kernel.lintegral_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) (ca : γ × α) (g : β → ENNReal) : ∫⁻ (b : β), g b ∂(prodMkLeft γ κ) ca = ∫⁻ (b : β), g b ∂κ ca.2

theorem ProbabilityTheory.Kernel.lintegral_prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) (ca : α × γ) (g : β → ENNReal) : ∫⁻ (b : β), g b ∂(prodMkRight γ κ) ca = ∫⁻ (b : β), g b ∂κ ca.1

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

instance ProbabilityTheory.Kernel.IsMarkovKernel.prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsMarkovKernel κ] : IsMarkovKernel (Kernel.prodMkRight γ κ)

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel (Kernel.prodMkLeft γ κ)

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel (Kernel.prodMkRight γ κ)

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

instance ProbabilityTheory.Kernel.IsFiniteKernel.prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsFiniteKernel κ] : IsFiniteKernel (Kernel.prodMkRight γ κ)

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

instance ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] : IsSFiniteKernel (Kernel.prodMkRight γ κ)

theorem ProbabilityTheory.Kernel.isSFiniteKernel_prodMkLeft_unit {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} : IsSFiniteKernel (prodMkLeft Unit κ) ↔ IsSFiniteKernel κ

theorem ProbabilityTheory.Kernel.isSFiniteKernel_prodMkRight_unit {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} : IsSFiniteKernel (prodMkRight Unit κ) ↔ IsSFiniteKernel κ

theorem ProbabilityTheory.Kernel.map_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {δ : Type u_3} {mδ : MeasurableSpace δ} (γ : Type u_5) [MeasurableSpace γ] (κ : Kernel α β) (f : β → δ) : (prodMkLeft γ κ).map f = prodMkLeft γ (κ.map f)

theorem ProbabilityTheory.Kernel.map_prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {δ : Type u_3} {mδ : MeasurableSpace δ} (κ : Kernel α β) (γ : Type u_5) {mγ : MeasurableSpace γ} (f : β → δ) : (prodMkRight γ κ).map f = prodMkRight γ (κ.map f)

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

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

Equations

• κ.swapLeft = κ.comap Prod.swap ⋯

@[simp]

theorem ProbabilityTheory.Kernel.swapLeft_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : β × α) : κ.swapLeft a = κ a.swap

theorem ProbabilityTheory.Kernel.swapLeft_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : β × α) (s : Set γ) : (κ.swapLeft a) s = (κ a.swap) s

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

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

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

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

@[simp]

theorem ProbabilityTheory.Kernel.swapLeft_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) (γ : Type u_5) {x✝ : MeasurableSpace γ} : (prodMkLeft γ κ).swapLeft = prodMkRight γ κ

@[simp]

theorem ProbabilityTheory.Kernel.swapLeft_prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) (γ : Type u_5) {x✝ : MeasurableSpace γ} : (prodMkRight γ κ).swapLeft = prodMkLeft γ κ

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

Define a Kernel α (γ × β) from a Kernel α (β × γ) by taking the map of Prod.swap. We use mapOfMeasurable in the definition for better defeqs.

Equations

• κ.swapRight = κ.mapOfMeasurable Prod.swap ⋯

theorem ProbabilityTheory.Kernel.swapRight_eq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) : κ.swapRight = κ.map Prod.swap

theorem ProbabilityTheory.Kernel.swapRight_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (a : α) : κ.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 γ} (κ : Kernel α (β × γ)) (a : α) {s : Set (γ × β)} (hs : MeasurableSet s) : (κ.swapRight a) s = (κ a) {p : β × γ | p.swap ∈ s}

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

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

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel κ.swapRight

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

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

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

Define a Kernel α β from a Kernel α (β × γ) by taking the map of the first projection. We use mapOfMeasurable for better defeqs.

Equations

• κ.fst = κ.mapOfMeasurable Prod.fst ⋯

theorem ProbabilityTheory.Kernel.fst_eq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) : κ.fst = κ.map Prod.fst

theorem ProbabilityTheory.Kernel.fst_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (a : α) : κ.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 γ} (κ : Kernel α (β × γ)) (a : α) {s : Set β} (hs : MeasurableSet s) : (κ.fst a) s = (κ a) {p : β × γ | p.1 ∈ s}

@[simp]

theorem ProbabilityTheory.Kernel.fst_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} : fst 0 = 0

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

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

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.fst {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel κ.fst

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

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

@[instance 100]

instance ProbabilityTheory.Kernel.isFiniteKernel_of_isFiniteKernel_fst {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : Kernel α (β × γ)} [h : IsFiniteKernel κ.fst] : IsFiniteKernel κ

theorem ProbabilityTheory.Kernel.fst_map_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {δ : Type u_3} {mδ : MeasurableSpace δ} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) {f : β → γ} {g : β → δ} (hg : Measurable g) : (κ.map fun (x : β) => (f x, g x)).fst = κ.map f

theorem ProbabilityTheory.Kernel.fst_map_id_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) {γ : Type u_5} {mγ : MeasurableSpace γ} {f : β → γ} (hf : Measurable f) : (κ.map fun (a : β) => (a, f a)).fst = κ

theorem ProbabilityTheory.Kernel.fst_compProd_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {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 = κ.

@[simp]

theorem ProbabilityTheory.Kernel.fst_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel κ] [IsMarkovKernel η] : (κ.compProd η).fst = κ

theorem ProbabilityTheory.Kernel.fst_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (δ : Type u_5) [MeasurableSpace δ] (κ : Kernel α (β × γ)) : (prodMkLeft δ κ).fst = prodMkLeft δ κ.fst

theorem ProbabilityTheory.Kernel.fst_prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (δ : Type u_5) [MeasurableSpace δ] : (prodMkRight δ κ).fst = prodMkRight δ κ.fst

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

Define a Kernel α γ from a Kernel α (β × γ) by taking the map of the second projection. We use mapOfMeasurable for better defeqs.

Equations

• κ.snd = κ.mapOfMeasurable Prod.snd ⋯

theorem ProbabilityTheory.Kernel.snd_eq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) : κ.snd = κ.map Prod.snd

theorem ProbabilityTheory.Kernel.snd_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (a : α) : κ.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 γ} (κ : Kernel α (β × γ)) (a : α) {s : Set γ} (hs : MeasurableSet s) : (κ.snd a) s = (κ a) {p : β × γ | p.2 ∈ s}

@[simp]

theorem ProbabilityTheory.Kernel.snd_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} : snd 0 = 0

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

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

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.snd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel κ.snd

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

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

@[instance 100]

instance ProbabilityTheory.Kernel.isFiniteKernel_of_isFiniteKernel_snd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : Kernel α (β × γ)} [h : IsFiniteKernel κ.snd] : IsFiniteKernel κ

theorem ProbabilityTheory.Kernel.snd_map_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {δ : Type u_3} {mδ : MeasurableSpace δ} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) {f : β → γ} {g : β → δ} (hf : Measurable f) : (κ.map fun (x : β) => (f x, g x)).snd = κ.map g

theorem ProbabilityTheory.Kernel.snd_map_prod_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) {γ : Type u_5} {mγ : MeasurableSpace γ} {f : β → γ} (hf : Measurable f) : (κ.map fun (a : β) => (f a, a)).snd = κ

theorem ProbabilityTheory.Kernel.snd_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (δ : Type u_5) [MeasurableSpace δ] (κ : Kernel α (β × γ)) : (prodMkLeft δ κ).snd = prodMkLeft δ κ.snd

theorem ProbabilityTheory.Kernel.snd_prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) (δ : Type u_5) [MeasurableSpace δ] : (prodMkRight δ κ).snd = prodMkRight δ κ.snd

@[simp]

theorem ProbabilityTheory.Kernel.fst_swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) : κ.swapRight.fst = κ.snd

@[simp]

theorem ProbabilityTheory.Kernel.snd_swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α (β × γ)) : κ.swapRight.snd = κ.fst

noncomputable def ProbabilityTheory.Kernel.sectL {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) : Kernel α γ

Define a Kernel α γ from a Kernel (α × β) γ by taking the comap of fun a ↦ (a, b) for a given b : β.

Equations

• κ.sectL b = κ.comap (fun (a : α) => (a, b)) ⋯

@[simp]

theorem ProbabilityTheory.Kernel.sectL_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) (a : α) : (κ.sectL b) a = κ (a, b)

@[simp]

theorem ProbabilityTheory.Kernel.sectL_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (b : β) : sectL 0 b = 0

instance ProbabilityTheory.Kernel.instIsMarkovKernelSectLOfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) [IsMarkovKernel κ] : IsMarkovKernel (κ.sectL b)

instance ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelSectLOfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel (κ.sectL b)

instance ProbabilityTheory.Kernel.instIsFiniteKernelSectLOfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) [IsFiniteKernel κ] : IsFiniteKernel (κ.sectL b)

instance ProbabilityTheory.Kernel.instIsSFiniteKernelSectLOfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) [IsSFiniteKernel κ] : IsSFiniteKernel (κ.sectL b)

instance ProbabilityTheory.Kernel.instNeZeroMeasureCoeSectLOfProdMk {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((κ.sectL b) a)

@[instance 100]

instance ProbabilityTheory.Kernel.instIsMarkovKernelProdOfSectL {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {κ : Kernel (α × β) γ} [∀ (b : β), IsMarkovKernel (κ.sectL b)] : IsMarkovKernel κ

theorem ProbabilityTheory.Kernel.comap_sectL {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {δ : Type u_4} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel (α × β) γ) (b : β) {f : δ → α} (hf : Measurable f) : (κ.sectL b).comap f hf = κ.comap (fun (d : δ) => (f d, b)) ⋯

@[simp]

theorem ProbabilityTheory.Kernel.sectL_prodMkLeft {β : Type u_2} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (α : Type u_5) [MeasurableSpace α] (κ : Kernel β γ) (a : α) {b : β} : ((prodMkLeft α κ).sectL b) a = κ b

@[simp]

theorem ProbabilityTheory.Kernel.sectL_prodMkRight {α : Type u_1} {mα : MeasurableSpace α} {γ : Type u_3} {mγ : MeasurableSpace γ} (β : Type u_5) [MeasurableSpace β] (κ : Kernel α γ) (b : β) : (prodMkRight β κ).sectL b = κ

noncomputable def ProbabilityTheory.Kernel.sectR {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) : Kernel β γ

Define a Kernel β γ from a Kernel (α × β) γ by taking the comap of fun b ↦ (a, b) for a given a : α.

Equations

• κ.sectR a = κ.comap (fun (b : β) => (a, b)) ⋯

@[simp]

theorem ProbabilityTheory.Kernel.sectR_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (b : β) (a : α) : (κ.sectR a) b = κ (a, b)

@[simp]

theorem ProbabilityTheory.Kernel.sectR_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (a : α) : sectR 0 a = 0

instance ProbabilityTheory.Kernel.instIsMarkovKernelSectROfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) [IsMarkovKernel κ] : IsMarkovKernel (κ.sectR a)

instance ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelSectROfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel (κ.sectR a)

instance ProbabilityTheory.Kernel.instIsFiniteKernelSectROfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) [IsFiniteKernel κ] : IsFiniteKernel (κ.sectR a)

instance ProbabilityTheory.Kernel.instIsSFiniteKernelSectROfProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) [IsSFiniteKernel κ] : IsSFiniteKernel (κ.sectR a)

instance ProbabilityTheory.Kernel.instNeZeroMeasureCoeSectROfProdMk {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((κ.sectR a) b)

@[instance 100]

instance ProbabilityTheory.Kernel.instIsMarkovKernelProdOfSectR {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {κ : Kernel (α × β) γ} [∀ (b : α), IsMarkovKernel (κ.sectR b)] : IsMarkovKernel κ

theorem ProbabilityTheory.Kernel.comap_sectR {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {δ : Type u_4} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel (α × β) γ) (a : α) {f : δ → β} (hf : Measurable f) : (κ.sectR a).comap f hf = κ.comap (fun (d : δ) => (a, f d)) ⋯

@[simp]

theorem ProbabilityTheory.Kernel.sectR_prodMkLeft {β : Type u_2} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (α : Type u_5) [MeasurableSpace α] (κ : Kernel β γ) (a : α) : (prodMkLeft α κ).sectR a = κ

@[simp]

theorem ProbabilityTheory.Kernel.sectR_prodMkRight {α : Type u_1} {mα : MeasurableSpace α} {γ : Type u_3} {mγ : MeasurableSpace γ} (β : Type u_5) [MeasurableSpace β] (κ : Kernel α γ) (b : β) {a : α} : ((prodMkRight β κ).sectR a) b = κ a

@[simp]

theorem ProbabilityTheory.Kernel.sectL_swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) : κ.swapLeft.sectL = κ.sectR

@[simp]

theorem ProbabilityTheory.Kernel.sectR_swapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel (α × β) γ) : κ.swapLeft.sectR = κ.sectL

Composition of two kernels

noncomputable def ProbabilityTheory.Kernel.comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (η : Kernel β γ) (κ : Kernel α β) : Kernel α γ

Composition of two kernels.

Equations

• η.comp κ = { toFun := fun (a : α) => (κ a).bind ⇑η, measurable' := ⋯ }

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

Composition of two kernels.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Kernel.comp_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (η : Kernel β γ) (κ : Kernel α β) (a : α) : (η.comp κ) a = (κ a).bind ⇑η

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

@[simp]

theorem ProbabilityTheory.Kernel.zero_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) : comp 0 κ = 0

@[simp]

theorem ProbabilityTheory.Kernel.comp_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel β γ) : κ.comp 0 = 0

theorem ProbabilityTheory.Kernel.comp_eq_snd_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (η : Kernel β γ) [IsSFiniteKernel η] (κ : Kernel α β) [IsSFiniteKernel κ] : η.comp κ = (κ.compProd (prodMkLeft α η)).snd

theorem ProbabilityTheory.Kernel.lintegral_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (η : Kernel β γ) (κ : Kernel α β) (a : α) {g : γ → ENNReal} (hg : Measurable g) : ∫⁻ (c : γ), g c ∂(η.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_3} {mγ : MeasurableSpace γ} (η : Kernel β γ) [IsMarkovKernel η] (κ : Kernel α β) [IsMarkovKernel κ] : IsMarkovKernel (η.comp κ)

instance ProbabilityTheory.Kernel.IsFiniteKernel.comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (η : Kernel β γ) [IsFiniteKernel η] (κ : Kernel α β) [IsFiniteKernel κ] : IsFiniteKernel (η.comp κ)

instance ProbabilityTheory.Kernel.IsSFiniteKernel.comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (η : Kernel β γ) [IsSFiniteKernel η] (κ : Kernel α β) [IsSFiniteKernel κ] : IsSFiniteKernel (η.comp κ)

theorem ProbabilityTheory.Kernel.comp_assoc {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {δ : Type u_5} {mδ : MeasurableSpace δ} (ξ : Kernel γ δ) [IsSFiniteKernel ξ] (η : Kernel β γ) (κ : Kernel α β) : (ξ.comp η).comp κ = ξ.comp (η.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_3} {mγ : MeasurableSpace γ} {f : β → γ} (hf : Measurable f) (κ : Kernel α β) : (deterministic f hf).comp κ = κ.map f

theorem ProbabilityTheory.Kernel.comp_deterministic_eq_comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {g : γ → α} (κ : Kernel α β) (hg : Measurable g) : κ.comp (deterministic g hg) = κ.comap g hg

theorem ProbabilityTheory.Kernel.deterministic_comp_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {f : β → γ} {g : γ → α} (hf : Measurable f) (hg : Measurable g) : (deterministic g hg).comp (deterministic f hf) = deterministic (g ∘ f) ⋯

@[simp]

theorem ProbabilityTheory.Kernel.comp_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : κ.comp Kernel.id = κ

@[simp]

theorem ProbabilityTheory.Kernel.id_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : Kernel.id.comp κ = κ

@[simp]

theorem ProbabilityTheory.Kernel.comp_discard {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [IsMarkovKernel κ] : (discard β).comp κ = discard α

@[simp]

theorem ProbabilityTheory.Kernel.swap_copy {α : Type u_1} {mα : MeasurableSpace α} : (swap α α).comp (copy α) = copy α

@[simp]

theorem ProbabilityTheory.Kernel.swap_swap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : (swap α β).comp (swap β α) = Kernel.id

theorem ProbabilityTheory.Kernel.swap_comp_eq_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {κ : Kernel α (β × γ)} : (swap β γ).comp κ = κ.map Prod.swap

theorem ProbabilityTheory.Kernel.const_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure γ) (κ : Kernel α β) : ⇑((const β μ).comp κ) = fun (a : α) => (κ a) Set.univ • μ

@[simp]

theorem ProbabilityTheory.Kernel.const_comp' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure γ) (κ : Kernel α β) [IsMarkovKernel κ] : (const β μ).comp κ = const α μ

theorem ProbabilityTheory.Kernel.map_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {δ : Type u_4} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) (η : Kernel β γ) (f : γ → δ) : (η.comp κ).map f = (η.map f).comp κ

theorem ProbabilityTheory.Kernel.fst_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {δ : Type u_4} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) (η : Kernel β (γ × δ)) : (η.comp κ).fst = η.fst.comp κ

theorem ProbabilityTheory.Kernel.snd_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {δ : Type u_4} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) (η : Kernel β (γ × δ)) : (η.comp κ).snd = η.snd.comp κ

@[simp]

theorem ProbabilityTheory.Kernel.snd_compProd_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel β γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] : (κ.compProd (prodMkLeft α η)).snd = η.comp κ

Product of two kernels

noncomputable def ProbabilityTheory.Kernel.prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel α γ) : Kernel α (β × γ)

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

Equations

• κ.prod η = κ.compProd (ProbabilityTheory.Kernel.prodMkLeft β η).swapLeft

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

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

Equations

• One or more equations did not get rendered due to their size.

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

theorem ProbabilityTheory.Kernel.prod_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] (a : α) : (κ.prod η) a = (κ a).prod (η a)

theorem ProbabilityTheory.Kernel.prod_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure β) [MeasureTheory.SFinite μ] (ν : MeasureTheory.Measure γ) [MeasureTheory.SFinite ν] : (const α μ).prod (const α ν) = const α (μ.prod ν)

theorem ProbabilityTheory.Kernel.lintegral_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] (a : α) {g : β × γ → ENNReal} (hg : Measurable g) : ∫⁻ (c : β × γ), g c ∂(κ.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_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsMarkovKernel κ] (η : Kernel α γ) [IsMarkovKernel η] : IsMarkovKernel (κ.prod η)

instance ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [h : IsZeroOrMarkovKernel κ] (η : Kernel α γ) [IsZeroOrMarkovKernel η] : IsZeroOrMarkovKernel (κ.prod η)

instance ProbabilityTheory.Kernel.IsFiniteKernel.prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsFiniteKernel κ] (η : Kernel α γ) [IsFiniteKernel η] : IsFiniteKernel (κ.prod η)

instance ProbabilityTheory.Kernel.IsSFiniteKernel.prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel α γ) : IsSFiniteKernel (κ.prod η)

@[simp]

theorem ProbabilityTheory.Kernel.fst_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsMarkovKernel η] : (κ.prod η).fst = κ

@[simp]

theorem ProbabilityTheory.Kernel.snd_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsMarkovKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] : (κ.prod η).snd = η

theorem ProbabilityTheory.Kernel.comap_prod_swap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {δ : Type u_4} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) (η : Kernel γ δ) [IsSFiniteKernel κ] [IsSFiniteKernel η] : ((prodMkRight α η).prod (prodMkLeft γ κ)).comap Prod.swap ⋯ = ((prodMkRight γ κ).prod (prodMkLeft α η)).map Prod.swap

theorem ProbabilityTheory.Kernel.map_prod_swap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel α γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] : (κ.prod η).map Prod.swap = η.prod κ

@[simp]

theorem ProbabilityTheory.Kernel.swap_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel α γ} [IsSFiniteKernel η] : (swap β γ).comp (κ.prod η) = η.prod κ

theorem ProbabilityTheory.Kernel.deterministic_prod_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} {f : α → β} {g : α → γ} (hf : Measurable f) (hg : Measurable g) : (deterministic f hf).prod (deterministic g hg) = deterministic (fun (a : α) => (f a, g a)) ⋯

theorem ProbabilityTheory.Kernel.compProd_prodMkLeft_eq_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel β γ) [IsSFiniteKernel η] : κ.compProd (prodMkLeft α η) = (Kernel.id.prod η).comp κ