Additive content built from a projective family of measures #
Let P be a projective family of measures on a family of measurable spaces indexed by ι.
That is, for each finite set I of indices, P I is a measure on Π j : I, α j, and for J ⊆ I,
the projection from Π i : I, α i to Π i : J, α i maps P I to P J.
We build an additive content projectiveFamilyContent on the measurable cylinders, by setting
projectiveFamilyContent s = P I S for s = cylinder I S, where I is a finite set of indices
and S is a measurable set in Π i : I, α i.
This content will be used to define the projective limit of the family of measures P.
For a countable index set and a projective family given by a sequence of kernels,
the projective limit is given by the Ionescu-Tulcea theorem.
For an arbitrary index set but under topological conditions on the spaces, this is the result of
the Kolmogorov extension theorem.
(both results are not yet in Mathlib)
Main definitions #
projectiveFamilyContent: additive content on the measurable cylinders, defined from a projective family of measures.
For P a family of measures, with P J a measure on Π j : J, α j, we define a function
projectiveFamilyFun P s by setting it to P I S if s = cylinder I S for a measurable S and
to 0 if s is not a measurable cylinder.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For P a projective family of measures, we define an additive content on the measurable
cylinders, by setting projectiveFamilyContent s = P I S for s = cylinder I S, where I is
a finite set of indices and S is a measurable set in Π i : I, α i.