Consecutive composition of kernels #
This file is the first step towards Ionescu-Tulcea theorem, which allows for instance to construct
the product of an infinite family of probability measures. The idea of the statement is as follows:
consider a family of kernels κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1)).
One can interpret κ n as a kernel which takes as an input the trajectory of a point started in
X 0 and moving X 0 → X 1 → X 2 → ... → X n and which outputs the distribution of the next
position of the point in X (n + 1). If a b : ℕ and a < b, we can compose the kernels,
and κ a ⊗ₖ κ (a + 1) ⊗ₖ ... ⊗ₖ κ b takes the trajectory up to time a as input and outputs
the distribution of the trajectory in X (a + 1) × ... × X (b + 1).
The Ionescu-Tulcea theorem then tells us that these compositions can be extended into a kernel
η : Kernel (Π i : Iic a, X i) → Π n > a, X n which given the trajectory up to time a outputs
the distribution of the infinite trajectory started in X (a + 1). In other words this theorem
makes sense of composing infinitely many kernels together.
To be able to even state the theorem we want to take the composition-product
(see ProbabilityTheory.Kernel.compProd) of consecutive kernels.
This however is not straightforward.
Consider n : ℕ. We cannot write (κ n) ⊗ₖ (κ (n + 1)) directly, we need to first
introduce an equivalence to see κ (n + 1) as a kernel with codomain
(Π i : Iic n, X i) × X (n + 1), and we get a Kernel (Π i : Iic n, X i) (X (n + 1) × (X (n + 2)).
However we want to do multiple compostion at ones, i.e. write
(κ n) ⊗ₖ ... ⊗ₖ (κ m) for n < m. This requires even more equivalences to make sense of, and at
the end of the day we get kernels which still cannot be composed together.
To tackle this issue, we decide here to only consider kernels of the form
Kernel (Π i : Iic a, X i) (Π i : Iic b, X i). In other words these kernels take as input
a trajectory up to time a and output the distribution of the full trajectory up to time b.
This is captured in the definition partialTraj κ a b
(partialTraj stands for "partial trajectory").
The advantage of this approach is that it allows us to write for instance
partialTraj κ b c ∘ₖ partialTraj κ a b = partialTraj κ a c (see partialTraj_comp_partialTraj.)
In this file we therefore define this family of kernels and prove some properties of it.
In particular we provide at the end of the file some results to compute the integral of a function
against partialTraj κ a b, taking inspiration from MeasureTheory.lmarginal.
Main definitions #
partialTraj κ a b: Given the trajectory of a point up to timea, returns the distribution of the trajectory up to timeb.lmarginalPartialTraj κ a b f: The integral offagainstpartialTraj κ a b. This is essentially the integral offagainstκ (a + 1) ⊗ₖ ... ⊗ₖ κ bbut seen as depending on all the variables, mimickingMeasureTheory.lmarginal. This allows to writelmarginalPartialTraj κ b c (lmarginalPartialTraj κ a b f).
Main statements #
partialTraj_comp_partialTraj: ifa ≤ bandb ≤ cthenpartialTraj κ b c ∘ₖ partialTraj κ a b = partialTraj κ a c.lmarginalPartialTraj_self: ifa ≤ bandb ≤ cthenlmarginalPartialTraj κ b c (lmarginalPartialTraj κ a b f) = lmarginalPartialTraj κ a c.
Tags #
Ionescu-Tulcea theorem, composition of kernels
Definition of partialTraj #
Given a family of kernels κ n from X 0 × ... × X n to X (n + 1) for all n,
construct a kernel from X 0 × ... × X a to X 0 × ... × X b by iterating κ.
The idea is that the input is some trajectory up to time a, and the ouptut is the distribution
of the trajectory up to time b. In particular if b ≤ a, this is just a deterministic kernel
(see partialTraj_le). The name partialTraj stands for "partial trajectory".
This kernel can be extended into a kernel with codomain Π n, X n via the Ionescu-Tulcea theorem.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If b ≤ a, given the trajectory up to time a, the trajectory up to time b is
deterministic and is equal to the restriction of the trajectory up to time a.
Given the trajectory up to time a, partialTraj κ a b gives the distribution of
the trajectory up to time b. Then plugging this into partialTraj κ b c gives
the distribution of the trajectory up to time c.
This is a technical lemma saying that partialTraj κ a b consists of two independent parts, the
first one being the identity. It allows to compute integrals.
If we restrict the distribution of the trajectory up to time c to times ≤ b we get
the trajectory up to time b.
Same as partialTraj_comp_partialTraj but only assuming a ≤ b. It requires Markov kernels.
Same as partialTraj_comp_partialTraj but only assuming b ≤ c. It requires Markov kernels.
Integrating against partialTraj #
This function computes the integral of a function f against partialTraj,
and allows to view it as a function depending on all the variables.
This is inspired by MeasureTheory.lmarginal, to be able to write
lmarginalPartialTraj κ b c (lmarginalPartialTraj κ a b f) = lmarginalPartialTraj κ a c.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If b ≤ a, then integrating f against partialTraj κ a b does nothing.
Integrating f against partialTraj κ a b x is the same as integrating only over the variables
from x_{a+1} to x_b.
Integrating f against partialTraj κ a (a + 1) is the same as integrating against κ a.
Integrating f against partialTraj κ a b and then against partialTraj κ b c is the same
as integrating f against partialTraj κ a c.
Lemmas about lmarginalPartialTraj and DependsOn #
If f only depends on the variables up to rank a and a ≤ b, integrating f against
partialTraj κ b c does nothing.
If f only depends on the variables uo to rank a, integrating beyond rank a is the same
as integrating up to rank a.
If f only depends on variables up to rank b, its integral from a to b only depends on
variables up to rank a.