Positive metric entropy of the constant-roof suspension flow over a Bernoulli base

This module defines the metric (Kolmogorov–Sinai) entropy of a measure-preserving flow as the entropy of its time-1 map (the canonical Sinai definition), and proves the headline result of issue #19: the constant-roof (τ ≡ 1) suspension flow of the two-sided asymmetric Bernoulli shift has positive metric entropy.

Construction

The base system is the invertible two-sided Bernoulli shift biShiftEquiv on BiShift α₀ with the i.i.d. measure bernZ ν. With the constant roof τ ≡ 1 the suspension space is BiShift α₀ × ℝ modulo the orbit relation (x, s) ∼ (T x, s − 1), and the suspension flow is the time-translation ζ_t [x, s] = [x, s + t]. The time-1 map of this flow factors onto the base shift via the projection to the fundamental-domain representative's first coordinate

π [x, s] := (T^{⌊s⌋}) x (for τ ≡ 1, ⌊s⌋ is the unique lap index),

realised concretely as the orbit-invariant descent of (x, s) ↦ baseIter T hτ ⌊s⌋ x. This π is measurable, measure-preserving (π_* μ̂ = bernZ ν, since for τ ≡ 1 the box is BiShift α₀ × [0, 1) and π ∘ suspensionMk = fst on it), and intertwines the time-1 flow with the base shift (π ∘ ζ_1 = biShiftEquiv ∘ π). It is therefore a factor map, so the factor- relative entropy invariance factor_relative_eq transports the positive base partition entropy Hnu ν to a lower bound on the flow's entropy.

Main definitions

• Oseledets.MeasurePreservingFlow.ksEntropy: the metric entropy of a measure-preserving flow, defined as the Kolmogorov–Sinai entropy of its time-1 map.
• Oseledets.Multifractal.suspensionBaseProj: the factor map π to the base shift.
• Oseledets.Multifractal.coordPartitionZFin: the time-0 coordinate partition reindexed to a Fin (Fintype.card α₀)-indexed partition (so it enters the Fin-indexed system entropy iSup).

Main results

• Oseledets.Multifractal.measurePreserving_suspensionBaseProj: π preserves the suspension probability measure, pushing it to bernZ ν.
• Oseledets.Multifractal.suspensionBaseProj_comp_flow: the intertwining π ∘ ζ_1 = T ∘ π.
• Oseledets.Multifractal.suspensionFlow_bernZ_ksEntropy_pos: the constant-roof Bernoulli suspension flow has strictly positive metric entropy.

noncomputable def Oseledets.MeasurePreservingFlow.ksEntropy {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] (φ : MeasurePreservingFlow μ) : EReal

The metric (Kolmogorov–Sinai) entropy of a measure-preserving flow φ, defined as the Kolmogorov–Sinai entropy of its time-1 map φ 1 (the canonical Sinai definition: the entropy of a flow is the entropy of any one of its non-trivial time-t maps, normalised; we take t = 1).

Equations

• φ.ksEntropy = Oseledets.Entropy.ksEntropy ⋯

Reindexing a partition along an equivalence of the index type

theorem Oseledets.Entropy.ksJoinCells_reindex {α : Type u_2} {ι : Type u_3} {κ : Type u_4} (cells : ι → Set α) (e : κ ≃ ι) (T : α → α) (n : ℕ) (f : Fin n → κ) : ksJoinCells (fun (k : κ) => cells (e k)) T n f = ksJoinCells cells T n fun (i : Fin n) => e (f i)

The n-fold join cells of a reindexed partition are those of the original, reindexed at the level of the join index Fin n → κ ≃ Fin n → ι by post-composition with e.

theorem Oseledets.Entropy.ksEntropySeq_reindex {α : Type u_2} [MeasurableSpace α] {ι : Type u_3} {κ : Type u_4} [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) (e : κ ≃ ι) (n : ℕ) : ksEntropySeq hT (P.reindex e) n = ksEntropySeq hT P n

Reindexing invariance of the iterated-join entropy. Reindexing a partition along an equivalence of index types leaves every iterated-join entropy ksEntropySeq unchanged: the join cells are merely reindexed by Fin n → κ ≃ Fin n → ι, which permutes the summands.

theorem Oseledets.Entropy.ksEntropyPartition_reindex {α : Type u_2} [MeasurableSpace α] {ι : Type u_3} {κ : Type u_4} [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) (e : κ ≃ ι) : ksEntropyPartition hT (P.reindex e) = ksEntropyPartition hT P

Reindexing invariance of the partition Kolmogorov–Sinai entropy. The KS entropy h(α, T) of a partition relative to T is unchanged when the partition's index type is reindexed along an equivalence: the underlying subadditive sequences agree as functions of n, hence so do their Fekete limits.

The base projection π for the constant roof

theorem Oseledets.Multifractal.baseIter_succ {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℤ) (x : X) : baseIter T hτ (n + 1) x = baseIter T hτ n (T x)

The base shift advances baseIter by one lap while moving the base point by T: baseIter T hτ (n + 1) x = baseIter T hτ n (T x). (The first coordinate of the suspension action is independent of the height coordinate, so suspensionAct (n+1) (x, 0) and suspensionAct n (T x, ·) have the same first coordinate.)

theorem Oseledets.Multifractal.baseIter_succ' {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℤ) (x : X) : baseIter T hτ (n + 1) x = T (baseIter T hτ n x)

The other lap-advance identity: baseIter T hτ (n + 1) x = T (baseIter T hτ n x). (Here the generator is applied after the n-th iterate, moving the resulting base point by T.)

noncomputable def Oseledets.Multifractal.suspensionBaseProjRaw {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (p : X × ℝ) : X

The raw base projection on X × ℝ for the constant roof τ ≡ 1: send (x, s) to the first coordinate of its fundamental-domain representative, which is baseIter T hτ ⌊s⌋ x (since ⌊s⌋ is the unique lap index). This descends through the suspension orbit quotient.

Equations

• Oseledets.Multifractal.suspensionBaseProjRaw T hτ p = Oseledets.baseIter T hτ ⌊p.2⌋ p.1

@[simp]

theorem Oseledets.Multifractal.suspensionBaseProjRaw_apply {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (p : X × ℝ) : suspensionBaseProjRaw T hτ p = baseIter T hτ ⌊p.2⌋ p.1

theorem Oseledets.Multifractal.suspensionBaseProjRaw_gen {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (hτ1 : τ = fun (x : X) => 1) (p : X × ℝ) : suspensionBaseProjRaw T hτ ((suspensionGen T hτ) p) = suspensionBaseProjRaw T hτ p

For the constant roof τ ≡ 1, the raw base projection is invariant along the suspension orbit generator G (x, s) = (T x, s − 1): baseIter ⌊s⌋ x = baseIter ⌊s − 1⌋ (T x).

theorem Oseledets.Multifractal.measurable_suspensionBaseProjRaw {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) : Measurable (suspensionBaseProjRaw T hτ)

The raw base projection is measurable. It is the composite of the measurable iterate (x, n) ↦ baseIter T hτ n x (each lap fixed; ℤ countable) with the measurable index map (x, s) ↦ (x, ⌊s⌋).

@[reducible, inline]

abbrev Oseledets.Multifractal.oneRoof {α₀ : Type u_2} : BiShift α₀ → ℝ

The constant roof τ ≡ 1 for the Bernoulli suspension.

Equations

• Oseledets.Multifractal.oneRoof x✝ = 1

theorem Oseledets.Multifractal.measurable_oneRoof {α₀ : Type u_2} [MeasurableSpace α₀] : Measurable oneRoof

theorem Oseledets.Multifractal.oneRoof_le {α₀ : Type u_2} (x : BiShift α₀) : 1 ≤ oneRoof x

noncomputable def Oseledets.Multifractal.bernSuspensionFlow {α₀ : Type u_2} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : MeasurePreservingFlow (suspensionMeasure biShiftEquiv ⋯ (bernZ ν))

The constant-roof Bernoulli suspension flow: the time-translation flow on the suspension of the two-sided shift biShiftEquiv over bernZ ν, with roof τ ≡ 1.

Equations

• Oseledets.Multifractal.bernSuspensionFlow ν = Oseledets.suspensionFlow Oseledets.Multifractal.biShiftEquiv ⋯ ⋯ ⋯ Oseledets.Multifractal.bernSuspensionFlow._proof_2

@[simp]

theorem Oseledets.Multifractal.bernSuspensionFlow_apply {α₀ : Type u_2} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] (t : ℝ) : (bernSuspensionFlow ν).toFun t = suspensionFlowMap biShiftEquiv ⋯ t

theorem Oseledets.Multifractal.integral_oneRoof {α₀ : Type u_2} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : ∫ (x : BiShift α₀), oneRoof x ∂bernZ ν = 1

The integral of the constant roof τ ≡ 1 against bernZ ν is 1.

theorem Oseledets.Multifractal.suspensionMeasure_oneRoof_eq {α₀ : Type u_2} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : suspensionMeasure biShiftEquiv ⋯ (bernZ ν) = suspensionMeasure₀ biShiftEquiv ⋯ (bernZ ν)

For τ ≡ 1 the normalising constant is 1, so the suspension probability measure coincides with the raw pushforward measure suspensionMeasure₀.

instance Oseledets.Multifractal.instIsProbabilityMeasureSuspensionMeasureBernZ {α₀ : Type u_2} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.IsProbabilityMeasure (suspensionMeasure biShiftEquiv ⋯ (bernZ ν))

The suspension probability measure is a probability measure.

The base projection as a factor map

noncomputable def Oseledets.Multifractal.suspensionBaseProj {α₀ : Type u_2} [MeasurableSpace α₀] : SuspensionSpace biShiftEquiv ⋯ → BiShift α₀

The base projection π : SuspensionSpace → BiShift α₀ of the constant-roof Bernoulli suspension: the orbit-invariant descent of (x, s) ↦ baseIter ⌊s⌋ x. On the fundamental domain BiShift α₀ × [0, 1) it is the first coordinate; it intertwines the time-1 flow with the base shift.

Equations

• Oseledets.Multifractal.suspensionBaseProj = Quotient.lift (Oseledets.Multifractal.suspensionBaseProjRaw Oseledets.Multifractal.biShiftEquiv ⋯) ⋯

@[simp]

theorem Oseledets.Multifractal.suspensionBaseProj_mk {α₀ : Type u_2} [MeasurableSpace α₀] (p : BiShift α₀ × ℝ) : suspensionBaseProj (suspensionMk biShiftEquiv ⋯ p) = suspensionBaseProjRaw biShiftEquiv ⋯ p

theorem Oseledets.Multifractal.measurable_suspensionBaseProj {α₀ : Type u_2} [MeasurableSpace α₀] : Measurable suspensionBaseProj

The base projection is measurable.

theorem Oseledets.Multifractal.suspensionBaseProj_comp_mk_on_domain {α₀ : Type u_2} [MeasurableSpace α₀] {p : BiShift α₀ × ℝ} (hp : p ∈ suspensionDomain oneRoof) : suspensionBaseProj (suspensionMk biShiftEquiv ⋯ p) = p.1

On the fundamental domain BiShift α₀ × [0, 1), the composite π ∘ suspensionMk is the first coordinate: there ⌊s⌋ = 0, so baseIter 0 x = x.

theorem Oseledets.Multifractal.measurePreserving_suspensionBaseProj {α₀ : Type u_2} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.MeasurePreserving suspensionBaseProj (suspensionMeasure biShiftEquiv ⋯ (bernZ ν)) (bernZ ν)

The base projection preserves the suspension measure, pushing it to bernZ ν. For τ ≡ 1 the box is BiShift α₀ × [0, 1), on which π ∘ suspensionMk = fst; pulling a measurable target set E back through the box gives (bernZ ν × volume) (E × [0, 1)) = bernZ ν E · 1 = bernZ ν E.

theorem Oseledets.Multifractal.suspensionBaseProj_comp_flow {α₀ : Type u_2} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : suspensionBaseProj ∘ (bernSuspensionFlow ν).toFun 1 = ⇑biShiftEquiv ∘ suspensionBaseProj

The base projection intertwines the time-1 flow with the base shift. For τ ≡ 1, ζ_1 [x, s] = [x, s + 1] = [T x, s], so π ∘ ζ_1 = biShiftEquiv ∘ π: pointwise on representatives, baseIter ⌊s + 1⌋ x = baseIter (⌊s⌋ + 1) x = biShiftMap (baseIter ⌊s⌋ x).

The base partition reindexed to a Fin-indexed partition

Positive metric entropy of the suspension flow

theorem Oseledets.Multifractal.suspensionFlow_bernZ_ksEntropy_pos {α₀ : Type u_2} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] [Fintype α₀] [MeasurableSingletonClass α₀] {i j : α₀} (hij : i ≠ j) (hi : 0 < (ν {i}).toReal) (hj : 0 < (ν {j}).toReal) : 0 < (bernSuspensionFlow ν).ksEntropy

The constant-roof Bernoulli suspension flow has positive metric entropy.

For the two-sided asymmetric Bernoulli shift charging two distinct symbols i ≠ j with positive mass, the single-symbol Shannon entropy Hnu ν is strictly positive (Hnu_pos). The base projection π is a factor map from the time-1 flow map onto the base shift, so the factor-relative entropy invariance factor_relative_eq carries the partition entropy of the base coordinate partition (equal to Hnu ν by hypothesis hbase) onto the pulled-back partition for the flow, which is bounded above by the flow's metric entropy via le_ksEntropy.

The base partition-entropy identification = Hnu ν is supplied by the companion two-sided-Bernoulli entropy module (ksEntropyPartition_coordPartitionZFin_bernZ_eq), so this statement is unconditional.