ProbabilityTheory.kernel.comp_assoc
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 γ δ))
[inst : ProbabilityTheory.IsSFiniteKernel ξ] (η : ↥(ProbabilityTheory.kernel β γ))
(κ : ↥(ProbabilityTheory.kernel α β)),
ProbabilityTheory.kernel.comp (ProbabilityTheory.kernel.comp ξ η) κ =
ProbabilityTheory.kernel.comp ξ (ProbabilityTheory.kernel.comp η κ)
The theorem `ProbabilityTheory.kernel.comp_assoc` states that the composition of probability kernels is associative. In other words, given three measurable spaces α, β, γ, and δ, and three corresponding probability kernels κ (from α to β), η (from β to γ), and ξ (from γ to δ), composing the kernels (ξ ∘ η) and κ is the same as composing ξ with (η ∘ κ). Here, the composition of kernels is understood as a kind of function composition, and the kernel from one space to another can be thought of as a generalization of the concept of a conditional probability. The property of associativity is crucial for the composition of functions, providing flexibility in the order of operations.
More concisely: Given probability kernels κ : α → β, η : β → γ, and ξ : γ → δ, the composition (ξ ∘ η) ∘ κ is equal to ξ ∘ (η ∘ κ) for measurable spaces α, β, γ, and δ.
|
ProbabilityTheory.kernel.lintegral_compProd
theorem ProbabilityTheory.kernel.lintegral_compProd :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
{mγ : MeasurableSpace γ} (κ : ↥(ProbabilityTheory.kernel α β)) [inst : ProbabilityTheory.IsSFiniteKernel κ]
(η : ↥(ProbabilityTheory.kernel (α × β) γ)) [inst : ProbabilityTheory.IsSFiniteKernel η] (a : α)
{f : β × γ → ENNReal},
Measurable f →
∫⁻ (bc : β × γ), f bc ∂(ProbabilityTheory.kernel.compProd κ η) a =
∫⁻ (b : β), ∫⁻ (c : γ), f (b, c) ∂η (a, b) ∂κ a
The theorem, `ProbabilityTheory.kernel.lintegral_compProd`, states that for any two kernels (which are a type of transition probability in a Markov chain) `κ` and `η`, where `κ` maps from a measurable space `α` to `β` and `η` maps from the product space of `α` and `β` to `γ`, if we have a function `f` mapping from the product space of `β` and `γ` to the extended nonnegative real numbers that is measurable, then the Lebesgue integral of `f` with respect to the composition-product of the kernels `κ` and `η` equals the iteration of the Lebesgue integrals of `f` over `γ` and `β` with respect to the kernels `η` and `κ` respectively. This theorem essentially provides a way to break down the Lebesgue integral of a function with respect to the composition of two kernels into more manageable parts.
More concisely: For measurable functions `f` from the product of two measurable spaces, the Lebesgue integral of `f` with respect to the composition of two kernels equals the iteration of the integrals with respect to each kernel.
|
ProbabilityTheory.kernel.measurable_compProdFun_of_finite
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 α β))
[inst : ProbabilityTheory.IsFiniteKernel κ] (η : ↥(ProbabilityTheory.kernel (α × β) γ))
[inst : ProbabilityTheory.IsFiniteKernel η],
MeasurableSet s → Measurable fun a => ProbabilityTheory.kernel.compProdFun κ η a s
This theorem, named `ProbabilityTheory.kernel.measurable_compProdFun_of_finite`, states that for any types `α`, `β`, and `γ` along with their associated measurable spaces `mα`, `mβ`, `mγ`, a set of pairs `s` in `β × γ`, and two kernels `κ` and `η` in the probability theory (with `κ` mapping from `α` to `β` and `η` mapping from `α × β` to `γ`, both of which are finite kernels), if `s` is a measurable set, then the function that maps `a` to the composition of the product function of `κ` and `η` with `a` and `s` is a measurable function.
In other words, under the above conditions, the composed function that involves kernels from the probability theory and their product function preserves the property of measurability.
More concisely: Given types `α`, `β`, `γ`, measurable spaces `mα`, `mβ`, `mγ`, a finite kernel `κ` from `α` to `β`, a finite kernel `η` from `α × β` to `γ`, and a measurable set `s` in `β × γ`, the function that maps `a` to `(κ ∘ π₁) (a, s) η` is measurable, where `π₁` is the projection function from `α × β` to `α`.
|
ProbabilityTheory.kernel.map_apply
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)
The theorem `ProbabilityTheory.kernel.map_apply` asserts that for all types `α`, `β`, and `γ`, along with their associated measurable spaces `mα`, `mβ`, and `mγ`, and for any function `f` from `β` to `γ` that is measurable, and for any element `κ` of the kernel of `α` and `β`, and any element `a` of type `α`, the application of the map function on the kernel `κ` with function `f` and element `a` is equal to the result of applying the measure-theory map function on `f` and `κ a`. In other words, it states that the mapping of a probability kernel coincides with the pushforward of the measure under the function `f`.
More concisely: Given measurable spaces `(α, mα)`, `(β, mβ)`, `(γ, mγ)`, a measurable function `f : β → γ`, a probability kernel `κ : ∀ a : α, MeasurableSpace γ × MeasurableSet (mγ) (f a)`, and an element `a : α`, we have `κ a = (f ∘ π₁) `^{-1} `[`La ⋈ MeasurableSet.image MeasurableSet.universe `] (mβ κ.proj₂ a)`, where `La` is the Lebesgue outer measure on `β`.
|
ProbabilityTheory.kernel.map_apply'
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 γ}, MeasurableSet s → ↑↑((ProbabilityTheory.kernel.map κ f hf) a) s = ↑↑(κ a) (f ⁻¹' s)
This theorem, named `ProbabilityTheory.kernel.map_apply'`, states that for any types `α`, `β` and `γ` with their respective measurable spaces `mα`, `mβ` and `mγ`, and any function `f` that maps `β` to `γ` and is measurable (the preimage of every measurable set is measurable), along with any element `a` of type `α` and any measurable set `s` of type `γ`, the application of the kernel map of `κ` (which is a measurable kernel from `α` to `β`) and `f` to `a` and `s` is equal to the application of `κ` to `a` and the preimage of `s` under `f`.
In simpler terms, this theorem relates the measure of the set obtained by mapping a measurable kernel through a measurable function to the measure of the preimage of that set under the original function.
More concisely: For any measurable kernels κ from type α to β and measurable functions f from β to γ, and for any a in α and measurable set s in γ, the application of κ to a and the preimage of s under f is equal to the application of κ to a and f to the measure of s.
|
ProbabilityTheory.kernel.lintegral_map
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},
Measurable g' → ∫⁻ (b : γ), g' b ∂(ProbabilityTheory.kernel.map κ f hf) a = ∫⁻ (a : β), g' (f a) ∂κ a
This theorem states that for any measurable spaces `α`, `β`, and `γ`, given a `κ` kernel from `α` to `β`, a measurable function `f` from `β` to `γ`, and a measurable function `g'` from `γ` to the extended nonnegative real numbers (usually denoted as `[0, ∞]`), the integral of `g'` with respect to the measure derived from mapping `κ` through `f` at a given point `a` in `α` is equal to the integral of the composition of `g'` and `f` with respect to `κ` at `a`. In other words, it asserts that the measure transformation by `f` can be interchanged with the process of integration. This is a version of the change of variables formula in the context of measure theory.
More concisely: For any measurable spaces `α`, `β`, and `γ`, given measurable functions `κ` from `α` to `β`, `f` from `β` to `γ`, and `g'` from `γ` to $[0, ∞]$, the integral of `g'` with respect to the pushforward measure of `κ` by `f` equals the integral of `g' ∘ f` with respect to `κ`.
|
ProbabilityTheory.kernel.lintegral_compProd'
theorem ProbabilityTheory.kernel.lintegral_compProd' :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
{mγ : MeasurableSpace γ} (κ : ↥(ProbabilityTheory.kernel α β)) [inst : ProbabilityTheory.IsSFiniteKernel κ]
(η : ↥(ProbabilityTheory.kernel (α × β) γ)) [inst : ProbabilityTheory.IsSFiniteKernel η] (a : α)
{f : β → γ → ENNReal},
Measurable (Function.uncurry f) →
∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(ProbabilityTheory.kernel.compProd κ η) a =
∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂η (a, b) ∂κ a
The theorem `ProbabilityTheory.kernel.lintegral_compProd'` states that for any given types `α`, `β`, and `γ` with their respective measurable spaces (`mα`, `mβ`, `mγ`), given two kernels `κ` and `η` from the probability theory where `κ` is a function from `α` to `β` and `η` is a function from the pair `(α, β)` to `γ`, and given a specific instance `a` of type `α`, and a measurable function `f` from `β` to `γ` that returns an extended nonnegative real number (`ENNReal`), then the Lebesgue integral of `f` with respect to the product of the composition of kernels `κ` and `η` at `a` is equal to the double Lebesgue integral of `f` at `(a, b)` with respect to the kernel `η` at `(a, b)` and the kernel `κ` at `a`. This result is essential in the field of probability theory, particularly in understanding the relationship between different probability measures.
More concisely: For measurable spaces (α, mα), (β, mβ), (γ, mγ), kernel η from (α × β) to γ, kernel κ from α to β, and measurable function f : β -> ENNReal, the Lebesgue integral of f compositions of κ and η at a in α equals the double Lebesgue integral of f at (a, b) in α × β with respect to η and κ.
|
ProbabilityTheory.kernel.comp_eq_snd_compProd
theorem ProbabilityTheory.kernel.comp_eq_snd_compProd :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
{mγ : MeasurableSpace γ} (η : ↥(ProbabilityTheory.kernel β γ)) [inst : ProbabilityTheory.IsSFiniteKernel η]
(κ : ↥(ProbabilityTheory.kernel α β)) [inst : ProbabilityTheory.IsSFiniteKernel κ],
ProbabilityTheory.kernel.comp η κ =
ProbabilityTheory.kernel.snd (ProbabilityTheory.kernel.compProd κ (ProbabilityTheory.kernel.prodMkLeft α η))
This theorem in probability theory, `ProbabilityTheory.kernel.comp_eq_snd_compProd`, states that for any measurable spaces `α`, `β`, and `γ`, and any σ-finite kernels `η` in `ProbabilityTheory.kernel β γ` and `κ` in `ProbabilityTheory.kernel α β`, the composition of the two kernels `η` and `κ` is equivalent to the kernel obtained by taking the second element from the product kernel of `κ` and the kernel obtained by changing the domain of `η` from `α` to `(γ × α)` (i.e., `ProbabilityTheory.kernel.prodMkLeft α η`). This is essentially a statement about the interchangeability of certain operations in the context of measure and probability theory.
More concisely: For any σ-finite measurable kernels η from β to γ and κ from α to β in probability theory, the composition of η and κ is equal to the product kernel of κ with η viewed as a kernel from α to γ.
|
ProbabilityTheory.kernel.lintegral_compProd₀
theorem ProbabilityTheory.kernel.lintegral_compProd₀ :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
{mγ : MeasurableSpace γ} (κ : ↥(ProbabilityTheory.kernel α β)) [inst : ProbabilityTheory.IsSFiniteKernel κ]
(η : ↥(ProbabilityTheory.kernel (α × β) γ)) [inst : ProbabilityTheory.IsSFiniteKernel η] (a : α)
{f : β × γ → ENNReal},
AEMeasurable f ((ProbabilityTheory.kernel.compProd κ η) a) →
∫⁻ (z : β × γ), f z ∂(ProbabilityTheory.kernel.compProd κ η) a =
∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a
This theorem, called `ProbabilityTheory.kernel.lintegral_compProd₀`, is about the Lebesgue integral against the composition-product of two kernels in probability theory. Specifically, for any types `α`, `β`, and `γ`, measurable spaces `mα`, `mβ`, and `mγ`, kernels `κ` and `η` (from `α` to `β` and from `α × β` to `γ` respectively), a variable `a` of type `α`, and a function `f` from `β × γ` to the extended nonnegative real numbers that is almost everywhere measurable with respect to the measure of the composition-product of `κ` and `η` at `a`, this theorem asserts the equality between two expressions of Lebesgue integrals. The left-hand side is the Lebesgue integral of `f` with respect to the measure of the composition-product of `κ` and `η` at `a`. The right-hand side is the iterated Lebesgue integral of `f`, first with respect to the measure of `η` at `(a, x)`, and then with respect to the measure of `κ` at `a`. This theorem is particularly relevant in situations where we are dealing with the composition of two kernels in the context of measure theory and probability.
More concisely: For measurable spaces `mα`, `mβ`, and `mγ`, kernels `κ` and `η`, a variable `a` of type `α`, and a function `f` from `β × γ` to the extended nonnegative real numbers that is almost everywhere measurable with respect to the measure of the composition-product of `κ` and `η` at `a`, the Lebesgue integral of `f` with respect to the composition-product of `κ` and `η` at `a` equals the iterated Lebesgue integral of `f` first with respect to `η` at `(a, x)` and then with respect to `κ` at `a`.
|