The information function of the iterated join #
This file builds the information-function foundation for the Shannon–McMillan–Breiman upper bound (Algoet–Cover) that feeds Krieger's name-count argument (issue #15, milestone M2).
For a measure-preserving transformation T of a probability space (α, μ) and a finite
measurable partition P, every point x has an n-step itinerary f : Fin n → ι recording,
for each 0 ≤ k < n, which cell of P the iterate Tᵏ x lies in. The atom of x is the
cell ⋂ₖ T⁻ᵏ (P_{f k}) of the iterated join ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P that contains x, and the
information function is iₙ(x) = -log μ(atom of x), the surprise of learning the n-name of
x.
Because the cells of P may overlap on a μ-null set, a naive Classical.choose-itinerary is
not pointwise measurable. We therefore build the itinerary as a least-index selector: among the
(non-empty, since the cells cover) set of admissible codes we pick the smallest in a fixed
enumeration. This selector is genuinely measurable, so the atom map and the information function
are measurable on the nose; the least-index cell agrees μ-almost everywhere with the chosen cell
(the discarded part lies in a pairwise a.e.-disjoint union), so the information function integrates
to the join entropy H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P).
Main definitions #
Oseledets.Krieger.itinerary: then-step least-index codef : Fin n → ιof a point.Oseledets.Krieger.atomOf: the atom⋂ₖ T⁻ᵏ (P_{f k})of the iterated join containingx.Oseledets.Krieger.infoFun: the information functioniₙ(x) = -log μ(atom of x).
Main results #
Oseledets.Krieger.itinerary_spec:Tᵏ x ∈ P_{itinerary x k}for allk.Oseledets.Krieger.mem_atomOf:x ∈ atomOf x.Oseledets.Krieger.measurableSet_atomOf: the atom is measurable.Oseledets.Krieger.measurable_infoFun: the information function is measurable.Oseledets.Krieger.infoFun_nonneg: the information function is nonnegative.Oseledets.Krieger.integral_infoFun_eq:∫ iₙ dμ = H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P) = ksEntropySeq ….
References #
- P. Algoet and T. Cover, A sandwich proof of the Shannon–McMillan–Breiman theorem, Ann. Probab. 16 (1988), 899–909.
- T. Downarowicz, Entropy in Dynamical Systems, Cambridge Univ. Press (2011), Lemma 4.2.5.
The set of admissible n-codes of a point x: those f : Fin n → ι such that
x lies in the iterated-join cell at f, i.e. Tᵏ x ∈ P_{f k} for every k. This set is
non-empty for every x because the cells of P cover the whole space.
Equations
- Oseledets.Krieger.admissibleCodes hT P n x = {f : Fin n → ι | x ∈ (Oseledets.Entropy.ksJoin hT P n).cells f}
Instances For
Every point has an admissible code: choosing, at each coordinate k, the P-cell containing
Tᵏ x (possible because the cells cover) yields a code whose iterated-join cell contains x.
The fixed enumeration of the (finite) code type Fin n → ι, used to break ties in the
least-index itinerary selector. We linearly order the finite type by transporting the order of
Fin (card) along the canonical equivalence. This is kept a local instance so it does not leak a
LinearOrder (Fin n → ι) onto downstream files.
Equations
Instances For
The n-step itinerary of a point x: the least admissible code, i.e. the smallest
f : Fin n → ι (in the fixed enumeration) for which Tᵏ x ∈ P_{f k} for all k. Using the least
admissible code rather than an arbitrary Classical.choose makes the selector measurable: its
fibers are differences of the (measurable) iterated-join cells.
Equations
- Oseledets.Krieger.itinerary hT P n x = ⋯.toFinset.min' ⋯
Instances For
The itinerary is an admissible code: it lies in the admissible set of x.
Itinerary specification. For each k, the k-th iterate Tᵏ x lies in the P-cell
indexed by the k-th coordinate of the itinerary of x.
The itinerary of x is the least admissible code: no strictly smaller code is admissible.
The fiber of the itinerary over a code g is the cell at g with the strictly smaller cells
removed. This explicit description is the engine of the measurability of itinerary.
The atom of x (with respect to the n-fold iterated join ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P): the cell
⋂ₖ T⁻ᵏ (P_{itinerary x k}) of the join that contains x.
Equations
- Oseledets.Krieger.atomOf hT P n x = (Oseledets.Entropy.ksJoin hT P n).cells (Oseledets.Krieger.itinerary hT P n x)
Instances For
A point lies in its own atom.
The atom of x is a measurable set: it is a cell of the iterated-join partition.
The atom of x equals the iterated-join cell at the itinerary of x.
The itinerary fiber {x | itinerary x = g} is measurable: it is the difference of the
measurable cell at g and the (finite) union of the strictly smaller cells.
The information function iₙ(x) = -log μ(atom of x) of the iterated join
⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P: the surprise of learning the n-name of x. Its integral is the join entropy
H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P).
Equations
- Oseledets.Krieger.infoFun hT P n x = -Real.log (μ (Oseledets.Krieger.atomOf hT P n x)).toReal
Instances For
The information weight attached to a code g: -log μ(cell g). The information function is the
composite of this weight with the itinerary.
Equations
- Oseledets.Krieger.infoWeight hT P n g = -Real.log (μ ((Oseledets.Entropy.ksJoin hT P n).cells g)).toReal
Instances For
The information function factors through the itinerary: iₙ(x) = infoWeight (itinerary x).
The information function is a finite sum of indicators of the (pairwise disjoint, covering) itinerary fibers, weighted by the corresponding information weight. This is the simple-function form that drives both its measurability and the integral computation.
The information function is measurable: in its simple-function form it is a finite sum of indicators of the (measurable) itinerary fibers with constant values, each of which is measurable. This avoids equipping the finite code type with a measurable structure.
The information weight of any code is nonnegative: the cell measure is at most 1, so its
logarithm is nonpositive and its negation is nonnegative.
The information function is nonnegative: it is the information weight of the itinerary, and
every cell of a probability space has measure at most 1.
The itinerary fibers cover the whole space: every point has an itinerary.
The itinerary fiber over g is contained in the cell at g.
The difference between the cell at g and the itinerary fiber over g lies in the union of
the other cells, hence is μ-null (the cells are pairwise a.e.-disjoint). Consequently the
fiber has the same measure as the cell.
The information function is integrable: it is bounded (a finite combination of indicators of sets of finite measure) on a probability space.
The information function integrates to the join entropy. Following Algoet–Cover
(Downarowicz, Lemma 4.2.5), the average information ∫ iₙ dμ equals the Shannon entropy
H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ P) of the n-fold iterated join. The proof writes iₙ as a sum of indicators of
the itinerary fibers (infoFun_eq_sum_indicator), integrates termwise using that each fiber has
the same measure as the corresponding cell (measure_itinerary_fiber), and recognizes the summand
μ(cell g) · (-log μ(cell g)) as negMulLog (μ(cell g)).toReal.