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.

Notations

• κ ×ₖ η = 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.

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_4} {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_4} {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_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 κ

@[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.comp_eq_snd_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (η : Kernel β γ) [IsSFiniteKernel η] (κ : Kernel α β) [IsSFiniteKernel κ] : η.comp κ = (κ.compProd (prodMkLeft α η)).snd

@[simp]

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

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

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 η)