Ionescu-Tulcea theorem #
This file proves the Ionescu-Tulcea theorem. 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 will take the trajectory up to time a as input and outputs
the distribution of the trajectory on X (a + 1) × ... × X (b + 1).
The Ionescu-Tulcea theorem tells us that these compositions can be extended into a
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.
In this file we construct this "limit" kernel given the family κ. More precisely, for any a : ℕ,
we construct the kernel traj κ a : Kernel (Π i : Iic a, X i) (Π n, X n), which takes as input
the trajectory in X 0 × ... × X a and outputs the distribution of the whole trajectory. The name
traj thus stands for "trajectory". We build a kernel with output in Π n, X n instead of
Π i > a, X i to make manipulations easier. The first coordinates are deterministic.
We also provide tools to compute integrals against traj κ a and an expression for the conditional
expectation.
Main definition #
traj κ a: a kernel fromΠ i : Iic a, X itoΠ n, X nwhich takes as input a trajectory up to timeaand outputs the distribution of the trajectory obtained by iterating the kernelsκ. Its existence is given by the Ionescu-Tulcea theorem.
Main statements #
eq_traj: Uniqueness oftraj: to check thatη = traj κ ait is enough to show that the restriction ofηto variables≤ bispartialTraj κ a b.traj_comp_partialTraj: Given the distribution up to timea,partialTraj κ a bgives the distribution of the trajectory up to timeb, and composing this withtraj κ bgives the distribution of the whole trajectory.condExp_traj: Ifa ≤ b, the conditional expectation offwith respect totraj κ agiven the information up to timebis obtained by integratingfagainsttraj κ b.
Implementation notes #
The kernel traj κ a is built using the Carathéodory extension theorem. First we build a projective
family of measures using inducedFamily and partialTraj κ a. Then we build a
MeasureTheory.AddContent on MeasureTheory.measurableCylinders called trajContent using
projectiveFamilyContent. Finally we prove trajContent_tendsto_zero which implies the
σ-additivity of the content, allowing to turn it into a measure.
References #
We follow the proof of Theorem 8.24 in O. Kallenberg, Foundations of Modern Probability. For a more detailed proof in the case of constant kernels (i.e. measures), see Proposition 10.6.1 in D. L. Cohn, Measure Theory.
Tags #
Ionescu-Tulcea theorem
This function takes as input a tuple (x_₀, ..., x_ₐ) and ind a function which
given (y_₀, ...,y_ₙ) outputs x_{n+1} : X (n + 1), and it builds an element of Π n, X n
by starting with (x_₀, ..., x_ₐ) and then iterating ind.
Equations
- iterateInduction x ind 0 = x ⟨0, ⋯⟩
- iterateInduction x ind k.succ = if h : k + 1 ≤ a then x ⟨k + 1, ⋯⟩ else ind k fun (i : { x : ℕ // x ∈ Finset.Iic k }) => iterateInduction x ind ↑i
Instances For
To check that a measure ν is the projective limit of a projective family of measures indexed
by Finset ℕ, it is enough to check on intervals of the form Iic n, where n is larger than
a given integer.
To check that a measure ν is the projective limit of a projective family of measures indexed
by Finset ℕ, it is enough to check on intervals of the form Iic n.
Given a family of measures μ : (n : ℕ) → Measure (Π i : Iic n, X i), we can define a family
of measures indexed by Finset ℕ by projecting the measures.
Equations
- MeasureTheory.inducedFamily μ S = MeasureTheory.Measure.map (Finset.restrict₂ ⋯) (μ (S.sup id))
Instances For
Given a family of measures μ : (n : ℕ) → Measure (Π i : Iic n, X i), the induced family
equals μ over the intervals Iic n.
Given a family of measures μ : (n : ℕ) → Measure (Π i : Iic n, X i), the induced family
will be projective only if μ is projective, in the sense that if a ≤ b, then projecting
μ b gives μ a.
Given a family of kernels κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1)), and the
trajectory up to time a we can construct an additive content over cylinders. It corresponds
to composing the kernels, starting at time a + 1.
Instances For
The trajContent κ x₀ of a cylinder indexed by first coordinates is given by partialTraj.
The trajContent of a cylinder is equal to the integral of its indicator function against
partialTraj.
This is an auxiliary result for trajContent_tendsto_zero. Consider f a sequence of bounded
measurable functions such that f n depends only on the first coordinates up to a n.
Assume that when integrating f n against partialTraj (k + 1) (a n), one gets a non-increasing
sequence of functions wich converges to l.
Assume then that there exists ε and y : Π i : Iic k, X i such that
when integrating f n against partialTraj k (a n) y, you get something at least
ε for all n. Then there exists z such that this remains true when integrating
f against partialTraj (k + 1) (a n) (update y (k + 1) z).
This is the key theorem to prove the existence of the traj:
the trajContent of a decreasing sequence of cylinders with empty intersection
converges to 0.
This implies the σ-additivity of trajContent
(see addContent_iUnion_eq_sum_of_tendsto_zero),
which allows to extend it to the σ-algebra by Carathéodory's theorem.
The trajContent is sigma-subadditive.
This function is the kernel given by the Ionescu-Tulcea theorem. It is shown belown that it
is measurable and turned into a true kernel in Kernel.traj.
Equations
- ProbabilityTheory.Kernel.trajFun κ a x₀ = (ProbabilityTheory.Kernel.trajContent κ x₀).measure ⋯ ⋯ ⋯
Instances For
Ionescu-Tulcea Theorem : Given a family of kernels κ n taking variables in Iic n with
value in X (n + 1), the kernel traj κ a takes a variable x depending on the
variables i ≤ a and associates to it a kernel on trajectories depending on all variables,
where the entries with index ≤ a are those of x, and then one follows iteratively the
kernels κ a, then κ (a + 1), and so on.
The fact that such a kernel exists on infinite trajectories is not obvious, and is the content of the Ionescu-Tulcea theorem.
Equations
- ProbabilityTheory.Kernel.traj κ a = { toFun := ProbabilityTheory.Kernel.trajFun κ a, measurable' := ⋯ }
Instances For
To check that η = traj κ a it is enough to show that the restriction of η to variables ≤ b
is partialTraj κ a b for any b ≥ n.
To check that η = traj κ a it is enough to show that the restriction of η to variables ≤ b
is partialTraj κ a b.
Given the distribution up to tome a, partialTraj κ a b gives the distribution
of the trajectory up to time b, and composing this with traj κ b gives the distribution
of the whole trajectory.
This theorem shows that traj κ n is, up to an equivalence, the product of
a determinstic kernel with another kernel. This is an intermediate result to compute integrals
with respect to this kernel.
When computing ∫ x, f x ∂traj κ n x₀, because the trajectory up to time n is
determined by x₀ we can replace x by updateFinset x (Iic a) x₀.