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

Main statements

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

Notations

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

Composition-Product of kernels

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

noncomputable def ProbabilityTheory.Kernel.compProdFun {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : 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.

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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) (a : α) : κ.compProdFun η a ∅ = 0

theorem ProbabilityTheory.Kernel.compProdFun_iUnion {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (f : ℕ → Set (β × γ)) (hf_meas : ∀ (i : ℕ), MeasurableSet (f i)) (hf_disj : Pairwise (Disjoint on 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_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) : κ.compProdFun η a s = ∑' (n : ℕ) (m : ℕ), (κ.seq n).compProdFun (η.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 (β × γ)} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsFiniteKernel η] (hs : MeasurableSet s) : Measurable fun (a : α) => κ.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 (β × γ)} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (hs : MeasurableSet s) : Measurable fun (a : α) => κ.compProdFun η a s

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

Composition-Product of kernels. For s-finite kernels, it satisfies ∫⁻ bc, f bc ∂(compProd κ η a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a) (see ProbabilityTheory.Kernel.lintegral_compProd). If either of the kernels is not s-finite, compProd is given the junk value 0.

Equations

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

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

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_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) (h : ¬ProbabilityTheory.IsSFiniteKernel κ) : κ.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 γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) (h : ¬ProbabilityTheory.IsSFiniteKernel η) : κ.compProd η = 0

theorem ProbabilityTheory.Kernel.compProd_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) : ((κ.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 γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) : ProbabilityTheory.Kernel.compProd 0 κ = 0

@[simp]

theorem ProbabilityTheory.Kernel.compProd_zero_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) (γ : Type u_5) [MeasurableSpace γ] : κ.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 (β × γ)} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {a : α} {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_4} {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : 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 ∂(κ.compProd η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a

@[deprecated ProbabilityTheory.Kernel.setLIntegral_compProd]

theorem ProbabilityTheory.Kernel.set_lintegral_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : 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 ∂(κ.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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.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]

theorem ProbabilityTheory.Kernel.set_lintegral_compProd_univ_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.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]

theorem ProbabilityTheory.Kernel.set_lintegral_compProd_univ_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} {s : Set (β × γ)} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] : κ.compProd η = ProbabilityTheory.Kernel.sum fun (n : ℕ) => ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) : κ.compProd η = ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] : κ.compProd η = ProbabilityTheory.Kernel.sum fun (n : ℕ) => κ.compProd (η.seq n)

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

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.Kernel.compProd_apply_univ_le {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsFiniteKernel η] (a : α) : ((κ.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 γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.IsFiniteKernel (κ.compProd η)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

map, comap

noncomputable def ProbabilityTheory.Kernel.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (f : β → γ) (hf : Measurable f) : 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.

Equations

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

theorem ProbabilityTheory.Kernel.map_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : β → γ} (κ : ProbabilityTheory.Kernel α β) (hf : Measurable f) (a : α) : (κ.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 : β → γ} (κ : ProbabilityTheory.Kernel α β) (hf : Measurable f) (a : α) {s : Set γ} (hs : MeasurableSet s) : ((κ.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

@[simp]

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

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

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

Equations

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

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

@[simp]

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

@[simp]

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

theorem ProbabilityTheory.Kernel.lintegral_comap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (hg : Measurable g) : (ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} {g : γ → α} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ] (hg : Measurable g) : ProbabilityTheory.IsMarkovKernel (κ.comap g hg)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

def ProbabilityTheory.Kernel.prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (γ : Type u_5) [MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α β) : ProbabilityTheory.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_5) [MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α β) : ProbabilityTheory.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_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (ca : γ × α) : (ProbabilityTheory.Kernel.prodMkLeft γ κ) ca = κ ca.2

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

theorem ProbabilityTheory.Kernel.map_prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {δ : Type u_4} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β) (γ : Type u_6) [MeasurableSpace γ] {f : β → δ} (hf : Measurable f) : (ProbabilityTheory.Kernel.prodMkRight γ κ).map f hf = ProbabilityTheory.Kernel.prodMkRight γ (κ.map f hf)

def ProbabilityTheory.Kernel.swapLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) : ProbabilityTheory.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_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (a : β × α) : κ.swapLeft a = κ a.swap

theorem ProbabilityTheory.Kernel.swapLeft_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.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_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.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_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsMarkovKernel κ] : ProbabilityTheory.IsMarkovKernel κ.swapLeft

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

theorem ProbabilityTheory.Kernel.swapLeft_prodMkLeft {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) (γ : Type u_6) [MeasurableSpace γ] : (ProbabilityTheory.Kernel.prodMkLeft γ κ).swapLeft = ProbabilityTheory.Kernel.prodMkRight γ κ

@[simp]

theorem ProbabilityTheory.Kernel.swapLeft_prodMkRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) (γ : Type u_6) [MeasurableSpace γ] : (ProbabilityTheory.Kernel.prodMkRight γ κ).swapLeft = ProbabilityTheory.Kernel.prodMkLeft γ κ

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

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

Equations

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

theorem ProbabilityTheory.Kernel.swapRight_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.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_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.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_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.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_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) [ProbabilityTheory.IsMarkovKernel κ] : ProbabilityTheory.IsMarkovKernel κ.swapRight

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• κ.fst = κ.map Prod.fst ⋯

theorem ProbabilityTheory.Kernel.fst_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.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_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.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_5} {mγ : MeasurableSpace γ} : ProbabilityTheory.Kernel.fst 0 = 0

theorem ProbabilityTheory.Kernel.lintegral_fst {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.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_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) [ProbabilityTheory.IsMarkovKernel κ] : ProbabilityTheory.IsMarkovKernel κ.fst

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

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

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

@[simp]

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

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

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

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

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

Equations

• κ.snd = κ.map Prod.snd ⋯

theorem ProbabilityTheory.Kernel.snd_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.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_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.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_5} {mγ : MeasurableSpace γ} : ProbabilityTheory.Kernel.snd 0 = 0

theorem ProbabilityTheory.Kernel.lintegral_snd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.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_5} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) [ProbabilityTheory.IsMarkovKernel κ] : ProbabilityTheory.IsMarkovKernel κ.snd

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

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

theorem ProbabilityTheory.Kernel.snd_map_prod_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) {γ : Type u_6} {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_5} {mγ : MeasurableSpace γ} (δ : Type u_6) [MeasurableSpace δ] (κ : ProbabilityTheory.Kernel α (β × γ)) : (ProbabilityTheory.Kernel.prodMkLeft δ κ).snd = ProbabilityTheory.Kernel.prodMkLeft δ κ.snd

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

@[simp]

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

@[simp]

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

Composition of two kernels

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

Composition of two kernels.

Equations

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

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

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_4} {mγ : MeasurableSpace γ} (η : ProbabilityTheory.Kernel β γ) (κ : ProbabilityTheory.Kernel α β) (a : α) : (η.comp κ) a = (κ a).bind ⇑η

theorem ProbabilityTheory.Kernel.comp_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (η : ProbabilityTheory.Kernel β γ) (κ : ProbabilityTheory.Kernel α β) (a : α) {s : Set γ} (hs : MeasurableSet s) : ((η.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 γ} (η : ProbabilityTheory.Kernel β γ) [ProbabilityTheory.IsSFiniteKernel η] (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] : η.comp κ = (κ.compProd (ProbabilityTheory.Kernel.prodMkLeft α η)).snd

theorem ProbabilityTheory.Kernel.lintegral_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (η : ProbabilityTheory.Kernel β γ) (κ : ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} (η : ProbabilityTheory.Kernel β γ) [ProbabilityTheory.IsMarkovKernel η] (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ] : ProbabilityTheory.IsMarkovKernel (η.comp κ)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 δ} (ξ : ProbabilityTheory.Kernel γ δ) [ProbabilityTheory.IsSFiniteKernel ξ] (η : ProbabilityTheory.Kernel β γ) (κ : ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} {f : β → γ} (hf : Measurable f) (κ : ProbabilityTheory.Kernel α β) : (ProbabilityTheory.Kernel.deterministic f hf).comp κ = κ.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 : γ → α} (κ : ProbabilityTheory.Kernel α β) (hg : Measurable g) : κ.comp (ProbabilityTheory.Kernel.deterministic g hg) = κ.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 γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α γ) : ProbabilityTheory.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

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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) : (κ.prod η) a = (κ a).prod (η a)

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

theorem ProbabilityTheory.Kernel.lintegral_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.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_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ] (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsMarkovKernel η] : ProbabilityTheory.IsMarkovKernel (κ.prod η)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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