Documentation

Oseledets.Examples.Rokhlin.DoublingEquality

Rokhlin's entropy equality for the doubling map #

This module assembles the concrete realization of Pesin's entropy equality on a real expanding system: for the doubling map T : y ↦ 2 • y on UnitAddCircle and the binary generating partition α = {[0,1/2), [1/2,1)}, h(α, T) = log 2 = ∫ log|det D(2x)| dμ = ∫ log 2 dμ.

The entropy side is ksEntropyPartition_doublingMap_eq_log_two, obtained by feeding the join-cell measure volume_binJoinCell (every n-fold-join cell has volume 2⁻ⁿ) into the abstract uniform-join reduction ksEntropyPartition_of_uniform. The integral side is integral_log_det_doublingMap_eq_log_two, whose integrand is the genuine log-determinant Real.log |doublingGen.det| of the doubling map's derivative generator doublingGen = !![2] (the matrix of DT, defined in Oseledets.Examples.Elementary). Since doublingGen.det = 2 (det_doublingGen, a 1 × 1 determinant), the Jacobian is the constant 2 — the doubling map is uniformly expanding — so log|det DT| = log 2 integrates against the probability measure to log 2. Their agreement is the headline rokhlin_equality_doublingMap, which therefore genuinely reads h(α, T) = ∫ log|det DT|: replacing the integrand by an arbitrary constant would break it, because the constant 2 is fixed by the derivative det.

Unlike the EuclideanSpace-framed Margulis–Ruelle inequality h ≤ ∑ λᵢ⁺, this is the genuine Pesin/Rokhlin equality h = ∫ log|det DT|, realized on a real expanding system.

Main results #

References #

The binary partition of the unit circle #

source
theorem Oseledets.Examples.Rokhlin.disjoint_binCell {i j : Fin 2} (hij : i ≠ j) :
Disjoint (binCell i) (binCell j)

The binary cells are pairwise disjoint (hence a.e.-disjoint): via mem_binCell_iff a point's membership in binCell i is determined by which half of [0,1) its representative rep lies in, and the two halves binLift 0 = [0,1/2), binLift 1 = [1/2,1) are disjoint.

source
theorem Oseledets.Examples.Rokhlin.aedisjoint_binCell :
Pairwise (Function.onFun (MeasureTheory.AEDisjoint MeasureTheory.volume) binCell)

The binary cells are pairwise almost-everywhere disjoint (they are in fact genuinely disjoint; see disjoint_binCell).

source
theorem Oseledets.Examples.Rokhlin.cover_binCell :
⋃ (i : Fin 2), binCell i = Set.univ

The binary cells cover the circle: every point's representative rep y ∈ [0,1) lies in one of the two halves [0,1/2) or [1/2,1), so y lies in binCell 0 or binCell 1.

source
noncomputable def Oseledets.Examples.Rokhlin.binPartition :
Entropy.MeasurePartition MeasureTheory.volume (Fin 2)

The binary partition {[0,1/2), [1/2,1)} of the unit circle, as a MeasurePartition for the volume (Haar) measure.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Oseledets.Examples.Rokhlin.binPartition_cells :
    binPartition.cells = binCell

    The entropy side: h(α, T) = log 2 #

    source
    theorem Oseledets.Examples.Rokhlin.uniform_binJoin (n : ℕ) (f : Fin n → Fin 2) :
    MeasureTheory.volume ((Entropy.ksJoin ⋯ binPartition n).cells f) = (↑(Fintype.card (Fin 2)) ^ n)⁻¹

    Every n-fold-join cell of binPartition under the doubling map has volume (2 ^ n)⁻¹. This restates volume_binJoinCell for the bundled partition, matching the hypothesis shape of ksEntropyPartition_of_uniform (with Fintype.card (Fin 2) = 2).

    source
    theorem Oseledets.Examples.Rokhlin.ksEntropyPartition_doublingMap_eq_log_two :
    Entropy.ksEntropyPartition ⋯ binPartition = Real.log 2

    Rokhlin equality, entropy side: h(α, T) = log 2. The partition-relative Kolmogorov–Sinai entropy of the binary partition under the doubling map is Real.log 2. The n-fold join is the uniform partition into 2ⁿ dyadic arcs of equal measure 2⁻ⁿ (uniform_binJoin), so the abstract uniform-join reduction ksEntropyPartition_of_uniform gives h(α, T) = log (card (Fin 2)) = log 2.

    The integral side: ∫ log|det DT| dμ = log 2 #

    source
    theorem Oseledets.Examples.Rokhlin.det_doublingGen :
    doublingGen.det = 2

    The determinant of the doubling map's derivative generator is 2. The matrix of DT for the doubling map x ↦ 2x is the 1 × 1 generator doublingGen = !![2] (Oseledets.Examples.Elementary), whose determinant is its single entry, 2.

    source
    theorem Oseledets.Examples.Rokhlin.integral_log_det_doublingMap_eq_log_two :
    ∫ (x : UnitAddCircle), Real.log |doublingGen.det| = Real.log 2

    Rokhlin equality, integral side: ∫ log|det DT| dμ = log 2. The integrand is the genuine log-determinant Real.log |doublingGen.det| of the doubling map's derivative generator doublingGen = !![2] (the matrix of DT). Since doublingGen.det = 2 (det_doublingGen) the Jacobian |det DT| = 2 is the constant 2 — the doubling map is uniformly expanding — so the integrand is log 2. Integrating that constant against the probability measure volume on the unit circle gives (volume univ).real • log 2 = 1 · log 2 = log 2.

    The headline: entropy = integral #

    source
    theorem Oseledets.Examples.Rokhlin.rokhlin_equality_doublingMap :
    Entropy.ksEntropyPartition ⋯ binPartition = ∫ (x : UnitAddCircle), Real.log |doublingGen.det|

    Pesin/Rokhlin equality on the doubling map. The Kolmogorov–Sinai entropy of the binary partition under the doubling map equals ∫ log|det DT|, where the integrand Real.log |doublingGen.det| is the genuine log-determinant of the doubling map's derivative generator doublingGen = !![2] (the matrix of DT). Both sides are Real.log 2: the entropy is log 2 by the dyadic uniform-join count, and the Jacobian |det DT| = 2 is the constant 2 (det_doublingGen) because the doubling map is uniformly expanding. This is the concrete realization of Pesin's equality h = ∫ log|det DT| on a real expanding system that the EuclideanSpace-framed Margulis–Ruelle inequality cannot give; because the integrand is a genuine determinant of the derivative, the statement is not invariant under replacing it by an arbitrary constant.