Product and composition of kernels #
We define
- the composition-product
κ ⊗ₖ ηof two s-finite kernelsκ : kernel α βandη : kernel (α × β) γ, a kernel fromαtoβ × γ. - the map and comap of a kernel along a measurable function.
- the composition
η ∘ₖ κof kernelsκ : kernel α βandη : kernel β γ, kernel fromαtoγ. - the product
κ ×ₖ ηof s-finite kernelsκ : kernel α βandη : kernel α γ, a kernel fromαtoβ × γ.
A note on names:
The composition-product kernel α β → kernel (α × β) γ → kernel α (β × γ) is named composition in
[kallenberg2021] and product on the wikipedia article on transition kernels.
Most papers studying categories of kernels call composition the map we call composition. We adopt
that convention because it fits better with the use of the name comp elsewhere in mathlib.
Main definitions #
Kernels built from other kernels:
compProd (κ : kernel α β) (η : kernel (α × β) γ) : kernel α (β × γ): composition-product of 2 s-finite kernels. We define a notationκ ⊗ₖ η = compProd κ η.∫⁻ bc, f bc ∂((κ ⊗ₖ η) a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)map (κ : kernel α β) (f : β → γ) (hf : Measurable f) : kernel α γ∫⁻ c, g c ∂(map κ f hf a) = ∫⁻ b, g (f b) ∂(κ a)comap (κ : kernel α β) (f : γ → α) (hf : Measurable f) : kernel γ β∫⁻ b, g b ∂(comap κ f hf c) = ∫⁻ b, g b ∂(κ (f c))comp (η : kernel β γ) (κ : kernel α β) : kernel α γ: composition of 2 kernels. We define a notationη ∘ₖ κ = comp η κ.∫⁻ c, g c ∂((η ∘ₖ κ) a) = ∫⁻ b, ∫⁻ c, g c ∂(η b) ∂(κ a)prod (κ : kernel α β) (η : kernel α γ) : kernel α (β × γ): product of 2 s-finite kernels.∫⁻ bc, f bc ∂((κ ×ₖ η) a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η a) ∂(κ a)
Main statements #
lintegral_compProd,lintegral_map,lintegral_comap,lintegral_comp,lintegral_prod: Lebesgue integral of a function against a composition-product/map/comap/composition/product of kernels.- Instances of the form
<class>.<operation>where class is one ofIsMarkovKernel,IsFiniteKernel,IsSFiniteKerneland operation is one ofcompProd,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 (β × γ))
:
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
- ProbabilityTheory.kernel.compProdFun κ η a s = ∫⁻ (b : β), ↑↑(η (a, b)) {c : γ | (b, c) ∈ s} ∂κ a
Instances For
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 : α)
:
ProbabilityTheory.kernel.compProdFun κ η a ∅ = 0
theorem
ProbabilityTheory.kernel.compProdFun_iUnion
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α β))
(η : ↥(ProbabilityTheory.kernel (α × β) γ))
[ProbabilityTheory.IsSFiniteKernel η]
(a : α)
(f : ℕ → Set (β × γ))
(hf_meas : ∀ (i : ℕ), MeasurableSet (f i))
(hf_disj : Pairwise (Disjoint on f))
:
ProbabilityTheory.kernel.compProdFun κ η a (⋃ (i : ℕ), f i) = ∑' (i : ℕ), ProbabilityTheory.kernel.compProdFun κ η a (f i)
theorem
ProbabilityTheory.kernel.compProdFun_tsum_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
(κ : ↥(ProbabilityTheory.kernel α β))
(η : ↥(ProbabilityTheory.kernel (α × β) γ))
[ProbabilityTheory.IsSFiniteKernel η]
(a : α)
(hs : MeasurableSet s)
:
ProbabilityTheory.kernel.compProdFun κ η a s = ∑' (n : ℕ), ProbabilityTheory.kernel.compProdFun κ (ProbabilityTheory.kernel.seq η n) a s
theorem
ProbabilityTheory.kernel.compProdFun_tsum_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α β))
(η : ↥(ProbabilityTheory.kernel (α × β) γ))
[ProbabilityTheory.IsSFiniteKernel κ]
(a : α)
(s : Set (β × γ))
:
ProbabilityTheory.kernel.compProdFun κ η a s = ∑' (n : ℕ), ProbabilityTheory.kernel.compProdFun (ProbabilityTheory.kernel.seq κ n) η a s
theorem
ProbabilityTheory.kernel.compProdFun_eq_tsum
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ↥(ProbabilityTheory.kernel (α × β) γ))
[ProbabilityTheory.IsSFiniteKernel η]
(a : α)
(hs : MeasurableSet s)
:
ProbabilityTheory.kernel.compProdFun κ η a s = ∑' (n : ℕ) (m : ℕ),
ProbabilityTheory.kernel.compProdFun (ProbabilityTheory.kernel.seq κ n) (ProbabilityTheory.kernel.seq η m) a s
theorem
ProbabilityTheory.kernel.measurable_compProdFun_of_finite
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsFiniteKernel κ]
(η : ↥(ProbabilityTheory.kernel (α × β) γ))
[ProbabilityTheory.IsFiniteKernel η]
(hs : MeasurableSet s)
:
Measurable fun (a : α) => ProbabilityTheory.kernel.compProdFun κ η a s
Auxiliary lemma for measurable_compProdFun.
theorem
ProbabilityTheory.kernel.measurable_compProdFun
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ↥(ProbabilityTheory.kernel (α × β) γ))
[ProbabilityTheory.IsSFiniteKernel η]
(hs : MeasurableSet s)
:
Measurable fun (a : α) => ProbabilityTheory.kernel.compProdFun κ η a s
noncomputable def
ProbabilityTheory.kernel.compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(κ : ↥(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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
:
↑↑((ProbabilityTheory.kernel.compProd κ η) a) s = ProbabilityTheory.kernel.compProdFun κ η a s
theorem
ProbabilityTheory.kernel.compProd_of_not_isSFiniteKernel_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α β))
(η : ↥(ProbabilityTheory.kernel (α × β) γ))
(h : ¬ProbabilityTheory.IsSFiniteKernel κ)
:
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 η)
:
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)
:
↑↑((ProbabilityTheory.kernel.compProd κ η) a) s = ∫⁻ (b : β), ↑↑(η (a, b)) {c : γ | (b, c) ∈ s} ∂κ a
theorem
ProbabilityTheory.kernel.le_compProd_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ↥(ProbabilityTheory.kernel (α × β) γ))
[ProbabilityTheory.IsSFiniteKernel η]
(a : α)
(s : Set (β × γ))
:
∫⁻ (b : β), ↑↑(η (a, b)) {c : γ | (b, c) ∈ s} ∂κ a ≤ ↑↑((ProbabilityTheory.kernel.compProd κ η) a) s
@[simp]
theorem
ProbabilityTheory.kernel.compProd_zero_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel (α × β) γ))
:
@[simp]
theorem
ProbabilityTheory.kernel.compProd_zero_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
(γ : Type u_5)
[MeasurableSpace γ]
:
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 : ↑↑((ProbabilityTheory.kernel.compProd κ η) a) 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)
:
↑↑((ProbabilityTheory.kernel.compProd κ η) a) s = 0 ↔ (fun (b : β) => ↑↑(η (a, b)) (Prod.mk b ⁻¹' s)) =ᶠ[MeasureTheory.Measure.ae (κ a)] 0
theorem
ProbabilityTheory.kernel.ae_null_of_compProd_null
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
(h : ↑↑((ProbabilityTheory.kernel.compProd κ η) a) s = 0)
:
(fun (b : β) => ↑↑(η (a, b)) (Prod.mk b ⁻¹' s)) =ᶠ[MeasureTheory.Measure.ae (κ a)] 0
theorem
ProbabilityTheory.kernel.ae_ae_of_ae_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
{p : β × γ → Prop}
(h : ∀ᵐ (bc : β × γ) ∂(ProbabilityTheory.kernel.compProd κ η) a, p bc)
:
∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
theorem
ProbabilityTheory.kernel.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 : β × γ) ∂(ProbabilityTheory.kernel.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 : β × γ) ∂(ProbabilityTheory.kernel.compProd κ η) a, p bc) ↔ ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
theorem
ProbabilityTheory.kernel.compProd_restrict
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[ProbabilityTheory.IsSFiniteKernel η]
{s : Set β}
{t : Set γ}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
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)
:
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)
:
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 ∂(ProbabilityTheory.kernel.compProd κ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂η (a, b) ∂κ a
Lebesgue integral against the composition-product of two kernels.
theorem
ProbabilityTheory.kernel.lintegral_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ↥(ProbabilityTheory.kernel (α × β) γ))
[ProbabilityTheory.IsSFiniteKernel η]
(a : α)
{f : β × γ → ENNReal}
(hf : Measurable f)
:
∫⁻ (bc : β × γ), f bc ∂(ProbabilityTheory.kernel.compProd κ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c) ∂η (a, b) ∂κ a
Lebesgue integral against the composition-product of two kernels.
theorem
ProbabilityTheory.kernel.lintegral_compProd₀
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ↥(ProbabilityTheory.kernel (α × β) γ))
[ProbabilityTheory.IsSFiniteKernel η]
(a : α)
{f : β × γ → ENNReal}
(hf : AEMeasurable f ((ProbabilityTheory.kernel.compProd κ η) a))
:
∫⁻ (z : β × γ), f z ∂(ProbabilityTheory.kernel.compProd κ η) a = ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a
Lebesgue integral against the composition-product of two kernels.
theorem
ProbabilityTheory.kernel.set_lintegral_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(κ : ↥(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 ∂(ProbabilityTheory.kernel.compProd κ η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
theorem
ProbabilityTheory.kernel.set_lintegral_compProd_univ_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(κ : ↥(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 ∂(ProbabilityTheory.kernel.compProd κ η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a
theorem
ProbabilityTheory.kernel.set_lintegral_compProd_univ_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(κ : ↥(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 ∂(ProbabilityTheory.kernel.compProd κ η) a = ∫⁻ (x : β), ∫⁻ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
theorem
ProbabilityTheory.kernel.compProd_eq_tsum_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ↥(ProbabilityTheory.kernel (α × β) γ))
[ProbabilityTheory.IsSFiniteKernel η]
(a : α)
(hs : MeasurableSet s)
:
↑↑((ProbabilityTheory.kernel.compProd κ η) a) s = ∑' (n : ℕ) (m : ℕ),
↑↑((ProbabilityTheory.kernel.compProd (ProbabilityTheory.kernel.seq κ n) (ProbabilityTheory.kernel.seq η m)) a) s
theorem
ProbabilityTheory.kernel.compProd_eq_sum_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ↥(ProbabilityTheory.kernel (α × β) γ))
[ProbabilityTheory.IsSFiniteKernel η]
:
ProbabilityTheory.kernel.compProd κ η = ProbabilityTheory.kernel.sum fun (n : ℕ) =>
ProbabilityTheory.kernel.sum fun (m : ℕ) =>
ProbabilityTheory.kernel.compProd (ProbabilityTheory.kernel.seq κ n) (ProbabilityTheory.kernel.seq η m)
theorem
ProbabilityTheory.kernel.compProd_eq_sum_compProd_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ↥(ProbabilityTheory.kernel (α × β) γ))
:
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 η]
:
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 η]
:
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 : α)
:
↑↑((ProbabilityTheory.kernel.compProd κ η) a) Set.univ ≤ ↑↑(κ a) Set.univ * ProbabilityTheory.IsFiniteKernel.bound η
instance
ProbabilityTheory.kernel.IsFiniteKernel.compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsFiniteKernel κ]
(η : ↥(ProbabilityTheory.kernel (α × β) γ))
[ProbabilityTheory.IsFiniteKernel η]
:
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 (α × β) γ))
:
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 η]
:
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 η]
:
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)
:
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
- ProbabilityTheory.kernel.map κ f hf = { val := fun (a : α) => MeasureTheory.Measure.map f (κ a), property := ⋯ }
Instances For
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 : α)
:
(ProbabilityTheory.kernel.map κ f hf) a = MeasureTheory.Measure.map f (κ a)
theorem
ProbabilityTheory.kernel.map_apply'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{f : β → γ}
(κ : ↥(ProbabilityTheory.kernel α β))
(hf : Measurable f)
(a : α)
{s : Set γ}
(hs : MeasurableSet s)
:
↑↑((ProbabilityTheory.kernel.map κ f hf) a) s = ↑↑(κ a) (f ⁻¹' s)
@[simp]
theorem
ProbabilityTheory.kernel.map_zero
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{f : β → γ}
(hf : Measurable f)
:
ProbabilityTheory.kernel.map 0 f hf = 0
@[simp]
theorem
ProbabilityTheory.kernel.map_id
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
:
ProbabilityTheory.kernel.map κ id ⋯ = κ
@[simp]
theorem
ProbabilityTheory.kernel.map_id'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
:
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 ∂(ProbabilityTheory.kernel.map κ f hf) a = ∫⁻ (a : β), g' (f a) ∂κ a
theorem
ProbabilityTheory.kernel.sum_map_seq
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{f : β → γ}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
(hf : Measurable f)
:
(ProbabilityTheory.kernel.sum fun (n : ℕ) => ProbabilityTheory.kernel.map (ProbabilityTheory.kernel.seq κ n) f hf) = ProbabilityTheory.kernel.map κ f hf
instance
ProbabilityTheory.kernel.IsMarkovKernel.map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{f : β → γ}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsMarkovKernel κ]
(hf : Measurable f)
:
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)
:
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)
:
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)
:
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
- ProbabilityTheory.kernel.comap κ g hg = { val := fun (a : γ) => κ (g a), property := ⋯ }
Instances For
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 : γ)
:
(ProbabilityTheory.kernel.comap κ g hg) c = κ (g c)
theorem
ProbabilityTheory.kernel.comap_apply'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{g : γ → α}
(κ : ↥(ProbabilityTheory.kernel α β))
(hg : Measurable g)
(c : γ)
(s : Set β)
:
↑↑((ProbabilityTheory.kernel.comap κ g hg) c) s = ↑↑(κ (g c)) s
@[simp]
theorem
ProbabilityTheory.kernel.comap_zero
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{g : γ → α}
(hg : Measurable g)
:
ProbabilityTheory.kernel.comap 0 g hg = 0
@[simp]
theorem
ProbabilityTheory.kernel.comap_id
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
:
ProbabilityTheory.kernel.comap κ id ⋯ = κ
@[simp]
theorem
ProbabilityTheory.kernel.comap_id'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
:
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 ∂(ProbabilityTheory.kernel.comap κ g hg) c = ∫⁻ (b : β), g' b ∂κ (g c)
theorem
ProbabilityTheory.kernel.sum_comap_seq
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{g : γ → α}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
(hg : Measurable g)
:
(ProbabilityTheory.kernel.sum fun (n : ℕ) => ProbabilityTheory.kernel.comap (ProbabilityTheory.kernel.seq κ n) g hg) = ProbabilityTheory.kernel.comap κ g hg
instance
ProbabilityTheory.kernel.IsMarkovKernel.comap
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
{g : γ → α}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsMarkovKernel κ]
(hg : Measurable g)
:
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)
:
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)
:
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)
:
ProbabilityTheory.kernel.comap (ProbabilityTheory.kernel.map κ g hg) f hf = ProbabilityTheory.kernel.map (ProbabilityTheory.kernel.comap κ f hf) 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 γ κ = ProbabilityTheory.kernel.comap κ Prod.snd ⋯
Instances For
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 γ κ = ProbabilityTheory.kernel.comap κ Prod.fst ⋯
Instances For
@[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 γ}
:
@[simp]
theorem
ProbabilityTheory.kernel.prodMkRight_zero
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
:
@[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 α β))
:
@[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 α β))
:
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 κ]
:
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 κ]
:
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 κ]
:
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 κ]
:
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 κ]
:
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 κ]
:
Equations
- ⋯ = ⋯
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)
:
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)
:
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
- ProbabilityTheory.kernel.swapLeft κ = ProbabilityTheory.kernel.comap κ Prod.swap ⋯
Instances For
@[simp]
theorem
ProbabilityTheory.kernel.swapLeft_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel (α × β) γ))
(a : β × α)
:
(ProbabilityTheory.kernel.swapLeft κ) a = κ (Prod.swap a)
theorem
ProbabilityTheory.kernel.swapLeft_apply'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel (α × β) γ))
(a : β × α)
(s : Set γ)
:
↑↑((ProbabilityTheory.kernel.swapLeft κ) a) s = ↑↑(κ (Prod.swap a)) s
theorem
ProbabilityTheory.kernel.lintegral_swapLeft
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel (α × β) γ))
(a : β × α)
(g : γ → ENNReal)
:
∫⁻ (c : γ), g c ∂(ProbabilityTheory.kernel.swapLeft κ) a = ∫⁻ (c : γ), g c ∂κ (Prod.swap a)
instance
ProbabilityTheory.kernel.IsMarkovKernel.swapLeft
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel (α × β) γ))
[ProbabilityTheory.IsMarkovKernel κ]
:
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 κ]
:
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 κ]
:
Equations
- ⋯ = ⋯
@[simp]
theorem
ProbabilityTheory.kernel.swapLeft_prodMkLeft
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
(γ : Type u_6)
[MeasurableSpace γ]
:
@[simp]
theorem
ProbabilityTheory.kernel.swapLeft_prodMkRight
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
(γ : Type u_6)
[MeasurableSpace γ]
:
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
- ProbabilityTheory.kernel.swapRight κ = ProbabilityTheory.kernel.map κ Prod.swap ⋯
Instances For
theorem
ProbabilityTheory.kernel.swapRight_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α (β × γ)))
(a : α)
:
(ProbabilityTheory.kernel.swapRight κ) a = MeasureTheory.Measure.map Prod.swap (κ a)
theorem
ProbabilityTheory.kernel.swapRight_apply'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α (β × γ)))
(a : α)
{s : Set (γ × β)}
(hs : MeasurableSet s)
:
↑↑((ProbabilityTheory.kernel.swapRight κ) a) s = ↑↑(κ a) {p : β × γ | Prod.swap p ∈ s}
theorem
ProbabilityTheory.kernel.lintegral_swapRight
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α (β × γ)))
(a : α)
{g : γ × β → ENNReal}
(hg : Measurable g)
:
∫⁻ (c : γ × β), g c ∂(ProbabilityTheory.kernel.swapRight κ) a = ∫⁻ (bc : β × γ), g (Prod.swap bc) ∂κ a
instance
ProbabilityTheory.kernel.IsMarkovKernel.swapRight
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α (β × γ)))
[ProbabilityTheory.IsMarkovKernel κ]
:
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 κ]
:
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 κ]
:
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
- ProbabilityTheory.kernel.fst κ = ProbabilityTheory.kernel.map κ Prod.fst ⋯
Instances For
theorem
ProbabilityTheory.kernel.fst_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α (β × γ)))
(a : α)
:
(ProbabilityTheory.kernel.fst κ) a = MeasureTheory.Measure.map Prod.fst (κ a)
theorem
ProbabilityTheory.kernel.fst_apply'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α (β × γ)))
(a : α)
{s : Set β}
(hs : MeasurableSet s)
:
↑↑((ProbabilityTheory.kernel.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 γ}
:
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 ∂(ProbabilityTheory.kernel.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 κ]
:
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 κ]
:
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 κ]
:
Equations
- ⋯ = ⋯
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 (ProbabilityTheory.kernel.fst κ)]
:
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)
:
ProbabilityTheory.kernel.fst (ProbabilityTheory.kernel.map κ (fun (x : β) => (f x, g x)) ⋯) = ProbabilityTheory.kernel.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)
:
ProbabilityTheory.kernel.fst (ProbabilityTheory.kernel.map κ (fun (a : β) => (a, f a)) ⋯) = κ
@[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 η]
:
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 α (β × γ)))
:
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 δ]
:
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
- ProbabilityTheory.kernel.snd κ = ProbabilityTheory.kernel.map κ Prod.snd ⋯
Instances For
theorem
ProbabilityTheory.kernel.snd_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α (β × γ)))
(a : α)
:
(ProbabilityTheory.kernel.snd κ) a = MeasureTheory.Measure.map Prod.snd (κ a)
theorem
ProbabilityTheory.kernel.snd_apply'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α (β × γ)))
(a : α)
{s : Set γ}
(hs : MeasurableSet s)
:
↑↑((ProbabilityTheory.kernel.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 γ}
:
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 ∂(ProbabilityTheory.kernel.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 κ]
:
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 κ]
:
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 κ]
:
Equations
- ⋯ = ⋯
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 (ProbabilityTheory.kernel.snd κ)]
:
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)
:
ProbabilityTheory.kernel.snd (ProbabilityTheory.kernel.map κ (fun (x : β) => (f x, g x)) ⋯) = ProbabilityTheory.kernel.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)
:
ProbabilityTheory.kernel.snd (ProbabilityTheory.kernel.map κ (fun (a : β) => (f a, a)) ⋯) = κ
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 α (β × γ)))
:
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 δ]
:
@[simp]
theorem
ProbabilityTheory.kernel.fst_swapRight
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α (β × γ)))
:
@[simp]
theorem
ProbabilityTheory.kernel.snd_swapRight
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α (β × γ)))
:
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
- ProbabilityTheory.kernel.comp η κ = { val := fun (a : α) => MeasureTheory.Measure.bind (κ a) ⇑η, property := ⋯ }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 : α)
:
(ProbabilityTheory.kernel.comp η κ) a = MeasureTheory.Measure.bind (κ a) ⇑η
theorem
ProbabilityTheory.kernel.comp_apply'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(η : ↥(ProbabilityTheory.kernel β γ))
(κ : ↥(ProbabilityTheory.kernel α β))
(a : α)
{s : Set γ}
(hs : MeasurableSet s)
:
↑↑((ProbabilityTheory.kernel.comp η κ) a) s = ∫⁻ (b : β), ↑↑(η b) s ∂κ a
theorem
ProbabilityTheory.kernel.comp_eq_snd_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(η : ↥(ProbabilityTheory.kernel β γ))
[ProbabilityTheory.IsSFiniteKernel η]
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
:
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 ∂(ProbabilityTheory.kernel.comp η κ) a = ∫⁻ (b : β), ∫⁻ (c : γ), g c ∂η b ∂κ a
instance
ProbabilityTheory.kernel.IsMarkovKernel.comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(η : ↥(ProbabilityTheory.kernel β γ))
[ProbabilityTheory.IsMarkovKernel η]
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsMarkovKernel κ]
:
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 κ]
:
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 κ]
:
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 α β))
:
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 α β))
:
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)
:
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
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
:
↑↑((ProbabilityTheory.kernel.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 : α)
:
(ProbabilityTheory.kernel.prod κ η) a = MeasureTheory.Measure.prod (κ a) (η a)
theorem
ProbabilityTheory.kernel.prod_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
[MeasureTheory.SFinite μ]
(ν : MeasureTheory.Measure β)
[MeasureTheory.SFinite ν]
:
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 ∂(ProbabilityTheory.kernel.prod κ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂η a ∂κ a
instance
ProbabilityTheory.kernel.IsMarkovKernel.prod
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_4}
{mγ : MeasurableSpace γ}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsMarkovKernel κ]
(η : ↥(ProbabilityTheory.kernel α γ))
[ProbabilityTheory.IsMarkovKernel η]
:
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 η]
:
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 α γ))
:
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 η]
:
@[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 η]
: