Frozen-factor product entropy: h(T × id) = h(T) #
For a measure-preserving system (X, T, μ) on a standard-Borel space and a standard-Borel
probability space (Y, ν), the frozen product transformation T × id on (X × Y, μ ⊗ ν) has the
same Kolmogorov–Sinai entropy as the base system:
h(T × id) = h(T) (Oseledets.Entropy.ksEntropy_prod_id_eq).
This is Walters' product-entropy theorem (Walters, An Introduction to Ergodic Theory,
Theorem 4.23), the final assembly of GitHub issue #20. It is proved by le_antisymm from the two
inequalities, each supplied by an already-proved sub-lemma module:
- the free bound
h(T) ≤ h(T × id)(ksEntropy_le_prod, the projection factor map); - the reverse bound
h(T × id) ≤ h(T), the genuine content, assembled here from Le Maître's inequality (7) (ksEntropyPartition_le_add_condEntropy), the rectangle-entropy identity (ksEntropyPartition_rectangle_eq), and the conditional-entropy refinement-to-zero glue (tendsto_condEntropy_genJoin_seq_zero).
The reverse bound #
ksEntropy (T × id) is the supremum over finite partitions P of X × Y of the partition
entropies h(P, T × id). For each P we squeeze with an increasing rectangle sequence
rectₘ = ξₘ ⊠ ηₘ, where ξₘ and ηₘ are the standard countably-generated atom partitions of
X and Y (MeasurableSpace.countablePartition). Le Maître's inequality gives
h(P, T × id) ≤ h(rectₘ, T × id) + H(P | σ(rectₘ)); the rectangle identity rewrites
h(rectₘ, T × id) = h(ξₘ, T) ≤ h(T); and the rectangle σ-algebras saturate m(X × Y), so the
static conditional entropies H(P | σ(rectₘ)) tend to 0. The limit is taken on ℝ (EReal
addition is not jointly continuous), handling h(T) = ⊤ separately by le_top.
Main results #
Oseledets.Entropy.ksEntropy_prod_id_eq:h(T × id) = h(T).
References #
- Peter Walters, An Introduction to Ergodic Theory, GTM 79, Springer (1982), Theorem 4.23.
- François Le Maître, Notes on the Kolmogorov–Sinai theorem (2017), §1–2.
Fintype on a countably-generated finite partition. Each countablePartition α n is a finite
set of sets (finite_countablePartition); we promote that Finite-ness to a Fintype so the set
can index a MeasurePartition.
Equations
The countably-generated atom partition of a standard-Borel space, packaged as a
MeasurePartition indexed by the (finite) set countablePartition α n itself. Its cells are the
atoms (Subtype.val); they are measurable, genuinely disjoint and cover the space.
Equations
- Oseledets.Entropy.cgPart α μ n = { cells := Subtype.val, measurable := ⋯, aedisjoint := ⋯, cover := ⋯ }
Instances For
cgPart α μ n generates the same σ-algebra as countablePartition α n.
The same atom partition, reindexed to a Fin-indexed partition (so it can feed le_ksEntropy,
whose supremum ranges over Fin-indexed partitions).
Equations
- Oseledets.Entropy.cgFin α μ n = (Oseledets.Entropy.cgPart α μ n).reindex (Fintype.equivFin ↑(MeasurableSpace.countablePartition α n)).symm
Instances For
The Fin-reindexed atom partition generates the same σ-algebra as countablePartition.
The generated σ-algebras of countablePartition are increasing in refinement.
The countably-generated atom partitions saturate the ambient σ-algebra:
⨆ n, σ(countablePartition α n) = mα.
Rectangle σ-algebra. For partitions ξ of (X, μ) and η of (Y, ν), the σ-algebra
generated by the rectangle partition (fst⁻¹ ξ) ∨ (snd⁻¹ η) of X × Y is the join of the pulled-
back coordinate σ-algebras comap fst σ(ξ) ⊔ comap snd σ(η). The ≤ step writes each rectangle
ξᵢ × ηⱼ = fst⁻¹ ξᵢ ∩ snd⁻¹ ηⱼ; the ≥ direction writes each fst⁻¹ ξᵢ = ⋃ⱼ ξᵢ × ηⱼ using that
η covers Y (and symmetrically for snd).
The Fin-indexed rectangle sequence feeding the conditional-entropy glue: the rectangle
partition ξₙ ⊠ ηₙ (atom partitions of X and Y), reindexed to a Fin-indexed partition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The σ-algebra of the reindexed rectangle equals that of the (non-reindexed) rectangle join.
The rectangle σ-algebra in coordinate form: comap fst σ(ξₙ) ⊔ comap snd σ(ηₙ).
The rectangle σ-algebras form an increasing chain.
The rectangle σ-algebras saturate the product σ-algebra m(X × Y).
Per-partition reverse bound. For each finite partition P of X × Y with nonempty index,
h(P, T × id) ≤ h(T). The argument squeezes via the rectangle sequence: Le Maître's inequality
bounds h(P, T × id) by h(ξₙ, T) + H(P | σ(rectₙ)), the first term is ≤ h(T), and the second
tends to 0.
Walters' product-entropy theorem (frozen identity factor): h(T × id) = h(T).
The free bound h(T) ≤ h(T × id) is ksEntropy_le_prod (the base is a factor of the product). The
reverse bound h(T × id) ≤ h(T) is ksEntropyPartition_prod_le for each finite partition P
of X × Y: partitions over an empty index do not exist on the nonempty space X × Y, so the
supremum reduces to the per-partition bounds.