Product and composition of kernels

We define the product κ ×ₖ η of s-finite kernels κ : Kernel α β and η : Kernel α γ, which is a kernel from α to β × γ.

Main definitions

• prod (κ : Kernel α β) (η : Kernel α γ) : Kernel α (β × γ): product of 2 s-finite kernels. ∫⁻ bc, f bc ∂((κ ×ₖ η) a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η a) ∂(κ a)

Main statements

• lintegral_prod: Lebesgue integral of a function against a product of kernels.
• Instances stating that IsMarkovKernel, IsZeroOrMarkovKernel, IsFiniteKernel and IsSFiniteKernel are stable by product.

Notation

• κ ×ₖ η = ProbabilityTheory.Kernel.prod κ η

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

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

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

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

theorem ProbabilityTheory.Kernel.parallelComp_comp_copy {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel α γ) : (κ.parallelComp η).comp (copy α) = κ.prod η

@[simp]

theorem ProbabilityTheory.Kernel.zero_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (η : Kernel α γ) : prod 0 η = 0

@[simp]

theorem ProbabilityTheory.Kernel.prod_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) : κ.prod 0 = 0

@[simp]

theorem ProbabilityTheory.Kernel.prod_of_not_isSFiniteKernel_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : Kernel α β} (η : Kernel α γ) (h : ¬IsSFiniteKernel κ) : κ.prod η = 0

@[simp]

theorem ProbabilityTheory.Kernel.prod_of_not_isSFiniteKernel_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) {η : Kernel α γ} (h : ¬IsSFiniteKernel η) : κ.prod η = 0

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

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

theorem ProbabilityTheory.Kernel.prod_apply_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : Kernel α β} {η : Kernel α γ} [IsSFiniteKernel κ] [IsSFiniteKernel η] {s : Set β} {t : Set γ} {a : α} : ((κ.prod η) a) (s ×ˢ t) = (κ a) s * (η a) t

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 ν] : (const α μ).prod (const α ν) = const α (μ.prod ν)

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

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

theorem ProbabilityTheory.Kernel.lintegral_deterministic_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : α → β} (hf : Measurable f) (κ : Kernel α γ) [IsSFiniteKernel κ] (a : α) {g : β × γ → ENNReal} (hg : Measurable g) : ∫⁻ (p : β × γ), g p ∂((deterministic f hf).prod κ) a = ∫⁻ (c : γ), g (f a, c) ∂κ a

theorem ProbabilityTheory.Kernel.lintegral_prod_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : α → γ} (hf : Measurable f) (κ : Kernel α β) [IsSFiniteKernel κ] (a : α) {g : β × γ → ENNReal} (hg : Measurable g) : ∫⁻ (p : β × γ), g p ∂(κ.prod (deterministic f hf)) a = ∫⁻ (b : β), g (b, f a) ∂κ a

theorem ProbabilityTheory.Kernel.lintegral_id_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ENNReal} (hf : Measurable f) (κ : Kernel α β) [IsSFiniteKernel κ] (a : α) : ∫⁻ (p : α × β), f p ∂(Kernel.id.prod κ) a = ∫⁻ (b : β), f (a, b) ∂κ a

theorem ProbabilityTheory.Kernel.lintegral_prod_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ENNReal} (hf : Measurable f) (κ : Kernel β α) [IsSFiniteKernel κ] (b : β) : ∫⁻ (p : α × β), f p ∂(κ.prod Kernel.id) b = ∫⁻ (a : α), f (a, b) ∂κ b

theorem ProbabilityTheory.Kernel.deterministic_prod_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : α → β} (mf : Measurable f) (κ : Kernel α γ) [IsSFiniteKernel κ] (a : α) {s : Set (β × γ)} (hs : MeasurableSet s) : (((deterministic f mf).prod κ) a) s = (κ a) (Prod.mk (f a) ⁻¹' s)

theorem ProbabilityTheory.Kernel.id_prod_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [IsSFiniteKernel κ] (a : α) {s : Set (α × β)} (hs : MeasurableSet s) : ((Kernel.id.prod κ) a) s = (κ a) (Prod.mk a ⁻¹' s)

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

@[simp]

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

theorem ProbabilityTheory.Kernel.comap_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel β γ) [IsSFiniteKernel κ] (η : Kernel β δ) [IsSFiniteKernel η] {f : α → β} (hf : Measurable f) : (κ.prod η).comap f hf = (κ.comap f hf).prod (η.comap f hf)

theorem ProbabilityTheory.Kernel.map_prod_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {ε : Type u_6} {mε : MeasurableSpace ε} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α δ) [IsSFiniteKernel η] {f : β → γ} (hf : Measurable f) {g : δ → ε} (hg : Measurable g) : (κ.map f).prod (η.map g) = (κ.prod η).map (Prod.map f g)

theorem ProbabilityTheory.Kernel.map_prod_eq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] {f : β → δ} (hf : Measurable f) : (κ.map f).prod η = (κ.prod η).map (Prod.map f id)

theorem ProbabilityTheory.Kernel.comap_prod_swap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} {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_4} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel α γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] : (κ.prod η).map Prod.swap = η.prod κ

theorem ProbabilityTheory.Kernel.prodComm_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel α γ} [IsSFiniteKernel η] : (κ.prod η).map ⇑MeasurableEquiv.prodComm = η.prod κ

@[simp]

theorem ProbabilityTheory.Kernel.swap_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {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_4} {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.id_prod_eq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : Kernel.id = (deterministic Prod.fst ⋯).prod (deterministic Prod.snd ⋯)

theorem ProbabilityTheory.Kernel.prodAssoc_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] (ξ : Kernel α δ) [IsSFiniteKernel ξ] : ((κ.prod ξ).prod η).map ⇑MeasurableEquiv.prodAssoc = κ.prod (ξ.prod η)

theorem ProbabilityTheory.Kernel.prodAssoc_symm_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] (ξ : Kernel α δ) [IsSFiniteKernel ξ] : (κ.prod (ξ.prod η)).map ⇑MeasurableEquiv.prodAssoc.symm = (κ.prod ξ).prod η

theorem ProbabilityTheory.Kernel.prod_const_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {δ : Type u_6} {mδ : MeasurableSpace δ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel β γ) [IsSFiniteKernel η] (μ : MeasureTheory.Measure δ) [MeasureTheory.SFinite μ] : (η.prod (const β μ)).comp κ = (η.comp κ).prod (const α μ)

theorem ProbabilityTheory.Kernel.const_prod_comp {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {δ : Type u_6} {mδ : MeasurableSpace δ} (κ : Kernel α β) [IsSFiniteKernel κ] (μ : MeasureTheory.Measure γ) [MeasureTheory.SFinite μ] (η : Kernel β δ) [IsSFiniteKernel η] : ((const β μ).prod η).comp κ = (const α μ).prod (η.comp κ)