Relative Kolmogorov–Sinai entropy via the Fekete limit #
This file builds the conditional (relative) Kolmogorov–Sinai entropy ladder, a faithful mirror
of the absolute ladder of Oseledets.Entropy.KSEntropy and Oseledets.Entropy.KSEntropyBounds.
Given a sub-σ-algebra 𝒜 ≤ mα and the conditional Shannon entropy condEntropy μ 𝒜 s of
Oseledets.Entropy.CondPartition, the relative entropy h(α, T | 𝒜) of a measure-preserving
transformation T relative to a finite measurable partition α is the Fekete limit of the
conditional iterated-join entropy sequence.
The construction reuses the flat Fin n-indexed iterated join ksJoin verbatim; only the entropy
functional changes from entropy to condEntropy μ 𝒜. Subadditivity is the conditional mirror of
ksEntropySeq_subadditive: the (n + m)-join reindexes (via ksJoinCells_append) to the join of
the n-fold join with the Tⁿ-pullback of the m-fold join, and the conditional join
subadditivity condEntropy_join_le bounds it by the sum of the two conditional entropies. The
second summand H(T⁻ⁿ(m-join) | 𝒜) is identified with H(m-join | 𝒜) by conditioning monotonicity
(condEntropy_mono_of_le, conditioning on the finer 𝒜 ≥ comap (Tⁿ) 𝒜 only decreases entropy)
followed by the joint pull-back condEntropy_comap_pullback, which evaluates
H(T⁻ⁿ(m-join) | comap (Tⁿ) 𝒜) = H(m-join | 𝒜). This route needs only the one-sided
forward-invariance hypothesis comap T 𝒜 ≤ 𝒜 (iterated to comap (Tⁿ) 𝒜 ≤ 𝒜 via
comap_iterate_le), which is therefore the single invariance hypothesis threaded through everything
from subadditivity onward — strictly weaker than the two-sided hypotheses of
condEntropy_pullback_iterate.
Main definitions #
Oseledets.Entropy.condKsEntropySeq: the conditional iterated-join entropy sequencen ↦ H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α | 𝒜).Oseledets.Entropy.condKsEntropyPartition: the relative Kolmogorov–Sinai entropyh(α, T | 𝒜), the Fekete limit.
Main results #
Oseledets.Entropy.condKsEntropySeq_subadditive: subadditivity of the conditional sequence.Oseledets.Entropy.condKsSubadditive: the sequence is aSubadditivesequence.Oseledets.Entropy.tendsto_condKsEntropySeq: convergence to the Fekete limit.Oseledets.Entropy.condKsEntropyPartition_le_condEntropy:h(α, T | 𝒜) ≤ H(α | 𝒜).Oseledets.Entropy.condKsEntropyPartition_bot: conditioning on⊥recoversh(α, T).
References #
- François Le Maître, Notes on the Kolmogorov–Sinai theorem (2017), §1.
- Peter Walters, An Introduction to Ergodic Theory, Springer GTM 79, Chapter 4.
Equal subadditive sequences have equal Fekete limits. Since Subadditive.lim u is defined
as sInf ((fun n => u n / n) '' Ici 1), depending only on the underlying sequence u and not on
the subadditivity proof, two subadditive sequences that agree as functions have equal limits.
The conditional iterated-join entropy sequence n ↦ H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α | 𝒜): the conditional
Shannon entropy condEntropy μ 𝒜 of the flat Fin-indexed join ksJoin hT P n. Its Fekete limit
is the relative Kolmogorov–Sinai entropy h(α, T | 𝒜).
Equations
- Oseledets.Entropy.condKsEntropySeq 𝒜 hT P n = Oseledets.Entropy.condEntropy μ 𝒜 (Oseledets.Entropy.ksJoin hT P n).cells
Instances For
The conditional iterated-join entropy is nonnegative: its integrand is pointwise nonnegative
because each conditional cell probability lies in [0, 1] (condEntropy_nonneg).
The flat n = 0 conditional join entropy is 0: the 0-fold join is the trivial one-cell
partition whose only cell (the empty intersection) is the whole space, and for every ω the Markov
kernel gives it conditional probability 1, with negMulLog 1 = 0; the integrand vanishes.
The single-step conditional iterated-join entropy equals the conditional Shannon entropy of the
partition itself: condKsEntropySeq 𝒜 hT P 1 = H(α | 𝒜). The 1-fold join is α reindexed by the
equivalence (Fin 1 → ι) ≃ ι (each cell at f : Fin 1 → ι is T⁰⁻¹(α_{f 0}) = α_{f 0}); the
conditional entropy is invariant under this reindexing of the index type.
One-sided forward-invariance iterates. If comap T 𝒜 ≤ 𝒜 (every 𝒜-set is, as a set, a
T-preimage of an 𝒜-set), then comap (T^[n]) 𝒜 ≤ 𝒜 for every n. The base case is
comap id 𝒜 = 𝒜 (MeasurableSpace.comap_id); the inductive step writes T^[n+1] = T ∘ T^[n]
(Function.iterate_succ'), factors the comap as comap (T^[n]) (comap T 𝒜)
(MeasurableSpace.comap_comp), and chains comap_mono hinv with the inductive hypothesis.
Subadditivity of the conditional iterated-join entropy (the Fekete inequality):
H(⋁ₖ₌₀ⁿ⁺ᵐ⁻¹ T⁻ᵏ α | 𝒜) ≤ H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α | 𝒜) + H(⋁ₖ₌₀ᵐ⁻¹ T⁻ᵏ α | 𝒜). Reindexing the
(n + m)-fold join by Fin.appendEquiv exhibits it as the join of the n-fold join with the
Tⁿ-pullback of the m-fold join (ksJoinCells_append); the conditional join subadditivity
condEntropy_join_le bounds it by the sum of the two conditional entropies. The second summand
H(T⁻ⁿ(m-join) | 𝒜) is identified with H(m-join | 𝒜) in two steps: conditioning monotonicity
condEntropy_mono_of_le against the finer 𝒜 ≥ comap (Tⁿ) 𝒜 (using comap_iterate_le hinv) only
decreases entropy, and the joint pull-back condEntropy_comap_pullback then evaluates
H(T⁻ⁿ(m-join) | comap (Tⁿ) 𝒜) = H(m-join | 𝒜). This needs only the one-sided forward-invariance
hypothesis hinv : comap T 𝒜 ≤ 𝒜.
The conditional iterated-join entropy sequence is a Subadditive sequence in the sense of
Fekete's lemma: u (k + l) ≤ u k + u l. This is condKsEntropySeq_subadditive repackaged.
The relative Kolmogorov–Sinai entropy h(α, T | 𝒜) of a measure-preserving transformation
T relative to a finite measurable partition α and a sub-σ-algebra 𝒜, defined as the Fekete
limit limₙ (1 / n) · H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α | 𝒜) of the subadditive conditional iterated-join entropy
sequence.
Equations
- Oseledets.Entropy.condKsEntropyPartition hm hT hinv P = ⋯.lim
Instances For
Fekete convergence to the relative Kolmogorov–Sinai entropy. The averaged conditional
iterated-join entropies (1 / n) · H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α | 𝒜) converge to h(α, T | 𝒜). The
boundedness-below hypothesis of Fekete's lemma is discharged from the nonnegativity of the
conditional entropies: each condKsEntropySeq n / n is at least 0.
The conditional iterated-join entropy grows at most linearly: condKsEntropySeq 𝒜 hT P n ≤ n • H(α | 𝒜). This is the subadditive estimate u n ≤ n • u 1, proved by induction from
condKsEntropySeq_subadditive, with the single step condKsEntropySeq 1 = H(α | 𝒜) substituted via
condKsEntropySeq_one.
Nonnegativity of the relative Kolmogorov–Sinai entropy: 0 ≤ h(α, T | 𝒜). Each averaged
conditional iterated-join entropy condKsEntropySeq n / n is nonnegative, and the bound passes to
the Fekete limit.
Upper bound of the relative Kolmogorov–Sinai entropy by the conditional partition entropy:
h(α, T | 𝒜) ≤ H(α | 𝒜). From the linear bound condKsEntropySeq n ≤ n • H(α | 𝒜)
(condKsEntropySeq_le_nsmul), dividing by n ≥ 1 gives condKsEntropySeq n / n ≤ H(α | 𝒜)
eventually; this passes to the Fekete limit.
The conditional iterated-join entropy at the trivial σ-algebra ⊥ equals the absolute
iterated-join entropy: condEntropy μ ⊥ of any cell family is the ordinary entropy μ of that
family (condEntropy_bot), and the cells of ksJoin hT P n are measurable.
The relative entropy at ⊥ recovers the absolute entropy:
h(α, T | ⊥) = h(α, T). The two iterated-join entropy sequences agree as functions of n
(condKsEntropySeq_bot), so the two subadditive sequences are equal and hence have equal Fekete
limits (Subadditive.lim_congr). The one-sided forward-invariance hypothesis for ⊥ is discharged
internally: comap T ⊥ = ⊥ (MeasurableSpace.comap_bot), so comap T ⊥ ≤ ⊥ holds reflexively.