The symbolic side of the entropy–dimension identity on the full shift

For an ergodic shift-invariant probability measure μ on the one-sided full shift Shift α₀ := ∀ _ : ℕ, α₀ over a finite alphabet, equipped with Mathlib's PiNat ultrametric (dist x y = (1/2) ^ firstDiff x y), this file builds the symbolic side of the foliation-free analogue of the expanding-Pesin / Ledrappier–Young identity:

the pointwise dimension exists μ-a.e. and equals h / log 2, where h is the Kolmogorov–Sinai entropy of the time-0 coordinate partition.

The construction proceeds in four nodes.

• A0 (setup). The shift map, its measurability, the time-0 coordinate partition, and the registration of PiNat.metricSpace as a local instance (it is deliberately not a global Mathlib instance).
• A1 (atom = cylinder). The n-step join atom atomOf of the coordinate partition equals the length-n PiNat cylinder, hence a closed ball of radius (1/2) ^ n. Consequently the mass of that ball equals the mass of the atom.
• A2 (SMB on dyadic radii). Combining A1 with the unconditional pointwise Shannon–McMillan–Breiman theorem (ae_tendsto_div_infoFun_self), the dyadic mass quotient log μ.real(B(x,(1/2)^n)) / log ((1/2)^n) converges μ-a.e. to h / log 2.
• A3 (dyadic → continuum). In the ultrametric PiNat, the closed ball is constant on each dyadic gap (1/2)^(n+1) ≤ r < (1/2)^n, so the continuum quotient is squeezed between its two dyadic endpoint values. Since log r → -∞ as r → 0⁺, the squeeze closes and the continuum limit equals the dyadic one. This is a pure ultrametric sandwich — no covering or doubling theory.

The dimension assembly (A5/A6) and the Bernoulli witness (A7) are separate, later nodes.

Main results

• Oseledets.Multifractal.atomOf_coordPartition_eq_cylinder
• Oseledets.Multifractal.closedBall_eq_atomOf
• Oseledets.Multifractal.ae_tendsto_logMass_div_dyadic
• Oseledets.Multifractal.ae_tendsto_logMass_div_continuum

References

• L. Barreira, Dimension and Recurrence in Hyperbolic Dynamics, Birkhäuser (2008), Ch. 4.
• T. Downarowicz, Entropy in Dynamical Systems, Cambridge Univ. Press (2011).

A0 — setup

@[reducible, inline]

abbrev Oseledets.Multifractal.Shift (α₀ : Type u_1) : Type u_1

The one-sided full shift space over the alphabet α₀: bi-infinite-to-the-right sequences ℕ → α₀. We give it the PiNat ultrametric as a local instance below.

Equations

• Oseledets.Multifractal.Shift α₀ = (ℕ → α₀)

def Oseledets.Multifractal.shiftMap {α₀ : Type u_1} : Shift α₀ → Shift α₀

The left shift map on the one-sided full shift: (shiftMap x) n = x (n + 1).

Equations

• Oseledets.Multifractal.shiftMap x n = x (n + 1)

theorem Oseledets.Multifractal.measurable_shiftMap {α₀ : Type u_1} [MeasurableSpace α₀] : Measurable shiftMap

The shift map is measurable: each coordinate of its output is a (measurable) coordinate projection of its input.

theorem Oseledets.Multifractal.shiftMap_iterate_apply {α₀ : Type u_1} (k : ℕ) (x : Shift α₀) (n : ℕ) : shiftMap^[k] x n = x (n + k)

The k-th iterate of the shift advances every index by k: shiftMap^[k] x n = x (n + k).

def Oseledets.Multifractal.coordPartition {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (μ : MeasureTheory.Measure (Shift α₀)) : Entropy.MeasurePartition μ α₀

The time-0 coordinate partition of the full shift: the cell at i is the clopen set {x | x 0 = i} of sequences starting with the symbol i. The cells are pairwise disjoint and cover the whole space, so they form a genuine measurable partition.

Equations

• Oseledets.Multifractal.coordPartition μ = { cells := fun (i : α₀) => {x : Oseledets.Multifractal.Shift α₀ | x 0 = i}, measurable := ⋯, aedisjoint := ⋯, cover := ⋯ }

A1 — the join atom is the cylinder

theorem Oseledets.Multifractal.itinerary_coordPartition_eq {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {μ : MeasureTheory.Measure (Shift α₀)} (hσmp : MeasureTheory.MeasurePreserving shiftMap μ μ) (n : ℕ) (x : Shift α₀) (k : Fin n) : Krieger.itinerary hσmp (coordPartition μ) n x k = x ↑k

The k-th itinerary symbol of x (for the coordinate partition) is just the k-th coordinate of x. Because the coordinate cells are genuinely disjoint, the least-index selector is forced to pick the coordinate x k — the itinerary inequality becomes an equality.

theorem Oseledets.Multifractal.mem_atom_coord_iff {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {μ : MeasureTheory.Measure (Shift α₀)} (hσmp : MeasureTheory.MeasurePreserving shiftMap μ μ) (n : ℕ) (x y : Shift α₀) (k : Fin n) : y ∈ shiftMap^[↑k] ⁻¹' (coordPartition μ).cells (Krieger.itinerary hσmp (coordPartition μ) n x k) ↔ y ↑k = x ↑k

Membership in the k-th preimage cell of the join atom is just y k = x k: indeed the cell is {z | z 0 = x k} (using itinerary_coordPartition_eq) and (shiftMap^[k] y) 0 = y k.

theorem Oseledets.Multifractal.atomOf_coordPartition_eq_cylinder {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {μ : MeasureTheory.Measure (Shift α₀)} (hσmp : MeasureTheory.MeasurePreserving shiftMap μ μ) (n : ℕ) (x : Shift α₀) : Krieger.atomOf hσmp (coordPartition μ) n x = PiNat.cylinder x n

A1 (atom = cylinder). The n-step join atom of x for the coordinate partition is exactly the length-n PiNat cylinder around x.

theorem Oseledets.Multifractal.cylinder_eq_closedBall {α₀ : Type u_1} [TopologicalSpace α₀] [DiscreteTopology α₀] (n : ℕ) (x : Shift α₀) : PiNat.cylinder x n = Metric.closedBall x ((1 / 2) ^ n)

The length-n cylinder is the closed ball of radius (1/2)^n: in the PiNat ultrametric, y ∈ cylinder x n ↔ dist x y ≤ (1/2)^n.

theorem Oseledets.Multifractal.closedBall_eq_atomOf {α₀ : Type u_1} [Fintype α₀] [TopologicalSpace α₀] [DiscreteTopology α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {μ : MeasureTheory.Measure (Shift α₀)} (hσmp : MeasureTheory.MeasurePreserving shiftMap μ μ) (n : ℕ) (x : Shift α₀) : Metric.closedBall x ((1 / 2) ^ n) = Krieger.atomOf hσmp (coordPartition μ) n x

A1 corollary (ball = atom). The closed ball of dyadic radius (1/2)^n is the n-step join atom, so its mass equals the atom mass.

A2 — pointwise SMB on dyadic radii

theorem Oseledets.Multifractal.logMass_div_dyadic_eq {α₀ : Type u_1} [Fintype α₀] [TopologicalSpace α₀] [DiscreteTopology α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {μ : MeasureTheory.Measure (Shift α₀)} (hσmp : MeasureTheory.MeasurePreserving shiftMap μ μ) (n : ℕ) (hn : 1 ≤ n) (x : Shift α₀) : Real.log (μ.real (Metric.closedBall x ((1 / 2) ^ n))) / Real.log ((1 / 2) ^ n) = Krieger.infoFun hσmp (coordPartition μ) n x / ↑n / Real.log 2

The dyadic mass quotient is, for n ≥ 1, exactly (infoFunₙ x / n) / log 2: the numerator log μ.real(B(x,(1/2)^n)) = -infoFunₙ(x) (A1) and the denominator log ((1/2)^n) = -n·log 2.

theorem Oseledets.Multifractal.ae_tendsto_logMass_div_dyadic {α₀ : Type u_1} [Fintype α₀] [Nonempty α₀] [TopologicalSpace α₀] [DiscreteTopology α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {μ : MeasureTheory.Measure (Shift α₀)} [MeasureTheory.IsProbabilityMeasure μ] (hσ : Ergodic shiftMap μ) : ∀ᵐ (x : Shift α₀) ∂μ, Filter.Tendsto (fun (n : ℕ) => Real.log (μ.real (Metric.closedBall x ((1 / 2) ^ n))) / Real.log ((1 / 2) ^ n)) Filter.atTop (nhds (Entropy.ksEntropyPartition ⋯ (coordPartition μ) / Real.log 2))

A2 (pointwise SMB on dyadic radii). The dyadic mass quotient log μ.real(B(x,(1/2)^n)) / log ((1/2)^n) converges μ-a.e. to h / log 2, where h is the Kolmogorov–Sinai entropy of the coordinate partition.

A3 — dyadic → continuum interpolation

theorem Oseledets.Multifractal.closedBall_eq_of_mem_gap {α₀ : Type u_1} [TopologicalSpace α₀] [DiscreteTopology α₀] {M : ℕ} (hM : 1 ≤ M) {r : ℝ} (x : Shift α₀) (hlo : (1 / 2) ^ M ≤ r) (hhi : r < (1 / 2) ^ (M - 1)) : Metric.closedBall x r = Metric.closedBall x ((1 / 2) ^ M)

Ball constancy on a dyadic gap. In the PiNat ultrametric every distance lies in {0} ∪ {(1/2)^m}, so a closed ball whose radius r lies in the dyadic gap (1/2)^M ≤ r < (1/2)^(M-1) coincides with the dyadic ball B(x,(1/2)^M).

noncomputable def Oseledets.Multifractal.dyadicIdx (r : ℝ) : ℕ

The dyadic scale index of a radius r: the least M with (1/2)^M ≤ r, packaged as ⌈log r / log (1/2)⌉₊. For r ∈ (0,1) it satisfies (1/2)^M ≤ r < (1/2)^(M-1).

Equations

• Oseledets.Multifractal.dyadicIdx r = ⌈Real.log r / Real.log (1 / 2)⌉₊

theorem Oseledets.Multifractal.dyadicIdx_spec {r : ℝ} (hr0 : 0 < r) (hr1 : r < 1) : 1 ≤ dyadicIdx r ∧ (1 / 2) ^ dyadicIdx r ≤ r ∧ r < (1 / 2) ^ (dyadicIdx r - 1)

For 0 < r < 1, the dyadic index M := dyadicIdx r brackets r: (1/2)^M ≤ r < (1/2)^(M-1) and M ≥ 1. This is the bracketing that makes the ball constant on the gap.

theorem Oseledets.Multifractal.logMass_div_continuum_bounds {α₀ : Type u_1} [TopologicalSpace α₀] [DiscreteTopology α₀] [MeasurableSpace α₀] {μ : MeasureTheory.Measure (Shift α₀)} [MeasureTheory.IsProbabilityMeasure μ] (x : Shift α₀) {r : ℝ} (hr0 : 0 < r) (hr1 : r < 1) (hM2 : 2 ≤ dyadicIdx r) : have D := fun (n : ℕ) => Real.log (μ.real (Metric.closedBall x ((1 / 2) ^ n))) / Real.log ((1 / 2) ^ n); have M := dyadicIdx r; D M ≤ Real.log (μ.real (Metric.closedBall x r)) / Real.log r ∧ Real.log (μ.real (Metric.closedBall x r)) / Real.log r ≤ D M * (↑M / (↑M - 1))

The continuum mass quotient on a gap, written via the dyadic sequence value at M. For (1/2)^M ≤ r < (1/2)^(M-1) the numerator is the dyadic numerator a(M) ≤ 0 (ball constancy) and log r ∈ [-M·log 2, -(M-1)·log 2), giving a two-sided bound by the dyadic quotients.

theorem Oseledets.Multifractal.tendsto_dyadicIdx_nhdsGT_zero : Filter.Tendsto dyadicIdx (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

The dyadic index tends to infinity as the radius tends to 0 from the right: r → 0⁺ forces log r → -∞, hence log r / log (1/2) → +∞, and ⌈·⌉₊ preserves this.

theorem Oseledets.Multifractal.ae_tendsto_logMass_div_continuum {α₀ : Type u_1} [Fintype α₀] [Nonempty α₀] [TopologicalSpace α₀] [DiscreteTopology α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {μ : MeasureTheory.Measure (Shift α₀)} [MeasureTheory.IsProbabilityMeasure μ] (hσ : Ergodic shiftMap μ) : ∀ᵐ (x : Shift α₀) ∂μ, Filter.Tendsto (fun (r : ℝ) => Real.log (μ.real (Metric.closedBall x r)) / Real.log r) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Entropy.ksEntropyPartition ⋯ (coordPartition μ) / Real.log 2))

A3 (dyadic → continuum interpolation). The continuum pointwise dimension exists μ-a.e.: the mass quotient log μ.real(B(x,r)) / log r converges, as r → 0⁺, to h / log 2 where h is the Kolmogorov–Sinai entropy of the coordinate partition. The ultrametric makes the ball constant on each dyadic gap, so the continuum quotient is squeezed between two dyadic quotients, both of which converge to h / log 2 by the dyadic SMB (A2).

A5 — the conditional, per-partition entropy = Hausdorff-dimension headline

Feeding the μ-a.e. pointwise dimension limit (A3) into the metric-space Billingsley/Frostman bridge dimH_eq_of_localDimension_eq (Oseledets/Multifractal/HausdorffDimension.lean) yields the symbolic entropy = dimension identity on the explicit conull carrier set: the Hausdorff dimension of the full-measure set on which the pointwise dimension exists equals h / log 2, with h the Kolmogorov–Sinai entropy of the coordinate partition.

The hypotheses are honest conditionals: hσ : Ergodic shiftMap μ and hpos : 0 < h. Both are genuinely satisfiable — any non-degenerate Bernoulli (i.i.d.) measure on the full shift is ergodic shift-invariant with strictly positive entropy — so the result is non-vacuous (the shift is a compact phase space, unlike the non-compact EuclideanSpace expanding case). No formalized Bernoulli instance is claimed here; that witness is the separate later node A7. The dimension base is log 2, fixed by the PiNat ultrametric (dist x y = (1/2) ^ firstDiff x y); it is never a free log β.

theorem Oseledets.Multifractal.dimH_eq_ksEntropyPartition_div_log_two {α₀ : Type u_1} [Fintype α₀] [Nonempty α₀] [TopologicalSpace α₀] [DiscreteTopology α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {μ : MeasureTheory.Measure (Shift α₀)} [MeasureTheory.IsProbabilityMeasure μ] (hσ : Ergodic shiftMap μ) (hpos : 0 < Entropy.ksEntropyPartition ⋯ (coordPartition μ)) : ∃ (s : Set (Shift α₀)), μ sᶜ = 0 ∧ dimH s = ENNReal.ofReal (Entropy.ksEntropyPartition ⋯ (coordPartition μ) / Real.log 2)

A5 (per-partition entropy = Hausdorff dimension). For an ergodic shift-invariant probability measure μ on the full shift with positive Kolmogorov–Sinai entropy h of the coordinate partition, there is a full-measure carrier set s whose Hausdorff dimension is exactly h / log 2.

The set s is the conull set on which the pointwise dimension exists (from A3, ae_tendsto_logMass_div_continuum); the bridge dimH_eq_of_localDimension_eq converts the everywhere-on-s pointwise limit α := h / log 2 > 0 into dimH s = α.

A6 — partition independence ⇒ the genuine entropy = dimension headline

The coordinate partition is a generator for the shift: its forward-shiftMap-saturated σ-algebra is the whole product σ-algebra. The Kolmogorov–Sinai generator theorem then upgrades A5 to the partition-independent identity h_μ(σ) = ksEntropy = dimension · log 2.

theorem Oseledets.Multifractal.generatedSigmaAlgebra_coordPartition_eq {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {μ : MeasureTheory.Measure (Shift α₀)} : Entropy.generatedSigmaAlgebra μ (coordPartition μ) = MeasurableSpace.comap (fun (x : Shift α₀) => x 0) inferInstance

The σ-algebra generated by the coordinate partition is the 0-th coordinate σ-algebra comap (eval 0) m_{α₀}: the cells {x | x 0 = i} are exactly the singleton preimages of the 0-th projection, and over a finite alphabet a measurable subset of α₀ is a finite union of singletons, so the two generated σ-algebras coincide.

theorem Oseledets.Multifractal.coordPartition_isGenerating {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {μ : MeasureTheory.Measure (Shift α₀)} (_hσmp : MeasureTheory.MeasurePreserving shiftMap μ μ) : Entropy.IsGenerating μ shiftMap (coordPartition μ)

A6 generator fact. The coordinate partition is a generating partition for the shift: ⨆ n, comap (shiftMap^[n]) σ(coordPartition) = MeasurableSpace.pi. The pullback of the 0-th coordinate σ-algebra along shiftMap^[n] is the n-th coordinate σ-algebra (since (shiftMap^[n] x) 0 = x n), and the product σ-algebra is, by definition, the supremum of all the coordinate σ-algebras.

def Oseledets.Multifractal.coordPartitionFin {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (μ : MeasureTheory.Measure (Shift α₀)) : Entropy.MeasurePartition μ (Fin (Fintype.card α₀))

The coordinate partition reindexed onto Fin (card α₀) via (Fintype.equivFin α₀).symm. This is the canonical Fin-indexed presentation needed to feed coordPartition into the Fin n-indexed Kolmogorov–Sinai generator theorem.

Equations

• One or more equations did not get rendered due to their size.

theorem Oseledets.Multifractal.generatedSigmaAlgebra_coordPartitionFin_eq {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {μ : MeasureTheory.Measure (Shift α₀)} : Entropy.generatedSigmaAlgebra μ (coordPartitionFin μ) = Entropy.generatedSigmaAlgebra μ (coordPartition μ)

The σ-algebra generated by the reindexed coordinate partition equals that of the original: a bijective reindexing leaves the range of cells unchanged.

theorem Oseledets.Multifractal.ksEntropyPartition_coordPartitionFin_eq {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {μ : MeasureTheory.Measure (Shift α₀)} [MeasureTheory.IsProbabilityMeasure μ] (hσmp : MeasureTheory.MeasurePreserving shiftMap μ μ) : Entropy.ksEntropyPartition hσmp (coordPartitionFin μ) = Entropy.ksEntropyPartition hσmp (coordPartition μ)

Reindexing invariance of the partition-relative entropy. The reindexed coordinate partition has the same Kolmogorov–Sinai entropy as the original: the iterated-join entropy sequences agree (entropy_reindex along f ↦ e ∘ f), and the Fekete limit is determined by that sequence.

theorem Oseledets.Multifractal.dimH_eq_ksEntropy_div_log_two {α₀ : Type u_1} [Fintype α₀] [Nonempty α₀] [TopologicalSpace α₀] [DiscreteTopology α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {μ : MeasureTheory.Measure (Shift α₀)} [MeasureTheory.IsProbabilityMeasure μ] (hσ : Ergodic shiftMap μ) (hpos : 0 < Entropy.ksEntropyPartition ⋯ (coordPartition μ)) : ∃ (s : Set (Shift α₀)), μ sᶜ = 0 ∧ dimH s = ENNReal.ofReal ((Entropy.ksEntropy ⋯).toReal / Real.log 2)

A6 headline — the entropy = Hausdorff-dimension identity. For an ergodic shift-invariant probability measure μ on the full shift with positive Kolmogorov–Sinai entropy, there is a full-measure carrier set s whose Hausdorff dimension equals h_μ(σ) / log 2, with h_μ(σ) the partition-independent Kolmogorov–Sinai entropy of the system (ksEntropy).

This is the genuine h_μ(σ) = dimension · log 2 identity: the coordinate partition is a generator (coordPartition_isGenerating), so the Kolmogorov–Sinai generator theorem (ksEntropy_eq_ksEntropyPartition_of_generating) identifies the system entropy ksEntropy with the coordinate partition's entropy, which A5 ties to the dimension. The hypotheses (Ergodic shiftMap, positive entropy) are honest conditionals, satisfiable by any non-degenerate Bernoulli measure — the shift is compact, so the statement is non-vacuous (the Bernoulli witness is the later node A7); no instance is claimed here. The base log 2 is fixed by the PiNat ultrametric.