The constant-roof Bernoulli suspension's time-1 map has entropy Hnu ν

This is the final fibre theorem of issue #20: the time-1 map of the constant-roof (τ ≡ 1) Bernoulli suspension flow has Kolmogorov–Sinai entropy exactly the per-symbol Shannon entropy Hnu ν:

ksEntropy ((bernSuspensionFlow ν).measurePreserving 1) = Hnu ν (Oseledets.Multifractal.ksEntropy_bernSuspensionFlow_one_eq_Hnu).

This is the Abramov-type identity for the constant roof, where the time-1 map of the suspension is measurably conjugate to the product of the base shift with the identity on the unit fibre. It upgrades the positivity result suspensionFlow_bernZ_ksEntropy_pos (issue #19) to the exact value.

Construction

For the constant roof the suspension space is measurably equivalent to the fundamental domain BiShift α₀ × ↥(Set.Ico (0 : ℝ) 1) via suspensionUnitMeasurableEquiv, with forward coordinate [x, s] ↦ (T^{⌊s⌋} x, Int.fract s). Under this equivalence:

• the time-1 map ζ_1 [x, s] = [x, s + 1] becomes the frozen product T × id (suspensionUnitEquiv_comp_flow), because ⌊s + 1⌋ = ⌊s⌋ + 1, Int.fract (s + 1) = Int.fract s and baseIter (⌊s⌋ + 1) x = T (baseIter ⌊s⌋ x);
• the suspension probability measure becomes the product bernZ ν × fibreMeasure, where fibreMeasure is Lebesgue measure on the unit fibre (a probability measure) (measurePreserving_suspensionUnitEquiv). This is proved through the inverse embedding (x, t) ↦ [x, t] of the box BiShift α₀ × [0, 1): pushing bernZ ν × fibreMeasure through it lands on (bernZ ν × volume)|_box, which is exactly the raw suspension measure (for τ ≡ 1 the normalisation is 1).

The entropy is then a clean three-step chain:

1. conjugacy invariance (ksEntropy_congr_of_conjugacy): h(ζ_1) = h(T × id);
2. frozen-factor product entropy (ksEntropy_prod_id_eq): h(T × id) = h(T);
3. two-sided Bernoulli system entropy (ksEntropy_biShiftEquiv_bernZ_eq): h(T) = Hnu ν.

Main results

• Oseledets.Multifractal.fibreMeasure: Lebesgue measure on ↥(Set.Ico (0 : ℝ) 1) (a probability measure).
• Oseledets.Multifractal.measurePreserving_suspensionUnitEquiv: the fundamental-domain equivalence sends the suspension measure to bernZ ν × fibreMeasure.
• Oseledets.Multifractal.suspensionUnitEquiv_comp_flow: the equivalence conjugates the time-1 map to the frozen product T × id.
• Oseledets.Multifractal.ksEntropy_bernSuspensionFlow_one_eq_Hnu: the headline identity.
• Oseledets.Multifractal.bernSuspensionFlow_ksEntropy_eq_Hnu: the flow-metric-entropy restatement.

References

• L. M. Abramov, On the entropy of a flow, Dokl. Akad. Nauk SSSR 128 (1959), 873–875.
• P. Walters, An Introduction to Ergodic Theory, GTM 79, Springer (1982), Theorem 4.23.

noncomputable def Oseledets.Multifractal.fibreMeasure : MeasureTheory.Measure ↑(Set.Ico 0 1)

Lebesgue measure on the unit fibre ↥(Set.Ico (0 : ℝ) 1), as the comap of volume along the subtype inclusion. Since volume (Ico 0 1) = 1 this is a probability measure.

Equations

• Oseledets.Multifractal.fibreMeasure = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume

instance Oseledets.Multifractal.instIsProbabilityMeasureFibreMeasure : MeasureTheory.IsProbabilityMeasure fibreMeasure

The unit-fibre measure is a probability measure (fibreMeasure univ = volume (Ico 0 1) = 1).

Measure preservation of the fundamental-domain equivalence

theorem Oseledets.Multifractal.map_suspensionUnitInv_eq {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.Measure.map (suspensionUnitInv biShiftEquiv ⋯) ((bernZ ν).prod fibreMeasure) = suspensionMeasure biShiftEquiv ⋯ (bernZ ν)

The inverse embedding (x, t) ↦ [x, t] of the box pushes bernZ ν × fibreMeasure to the suspension probability measure. Concretely suspensionUnitInv = suspensionMk ∘ (id × Subtype.val), so the pushforward factors as map suspensionMk ((bernZ ν) × (volume|_(Ico 0 1))) = map suspensionMk ((bernZ ν × volume)|_box) = suspensionMeasure₀ = suspensionMeasure (the last step uses that for τ ≡ 1 the normalisation is 1).

theorem Oseledets.Multifractal.measurePreserving_suspensionUnitEquiv {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.MeasurePreserving (⇑(suspensionUnitMeasurableEquiv biShiftEquiv ⋯ ⋯)) (suspensionMeasure biShiftEquiv ⋯ (bernZ ν)) ((bernZ ν).prod fibreMeasure)

The fundamental-domain equivalence is measure-preserving, sending the suspension probability measure to bernZ ν × fibreMeasure. Obtained by flipping the inverse-direction statement map_suspensionUnitInv_eq (a MeasurableEquiv is measure-preserving iff its inverse is).

The equivalence conjugates the time-1 map to the frozen product

theorem Oseledets.Multifractal.suspensionUnitEquiv_comp_flow {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : ⇑(suspensionUnitMeasurableEquiv biShiftEquiv ⋯ ⋯) ∘ (bernSuspensionFlow ν).toFun 1 = Prod.map (⇑biShiftEquiv) id ∘ ⇑(suspensionUnitMeasurableEquiv biShiftEquiv ⋯ ⋯)

The fundamental-domain equivalence conjugates the time-1 map to the frozen product T × id. For τ ≡ 1, ζ_1 [x, s] = [x, s + 1], and the equivalence maps [x, s] to (baseIter ⌊s⌋ x, Int.fract s); both sides of the conjugacy equation give (T (baseIter ⌊s⌋ x), Int.fract s) since ⌊s + 1⌋ = ⌊s⌋ + 1, Int.fract (s + 1) = Int.fract s and baseIter (⌊s⌋ + 1) x = T (baseIter ⌊s⌋ x).

The headline entropy identity

theorem Oseledets.Multifractal.ksEntropy_bernSuspensionFlow_one_eq_Hnu {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : Entropy.ksEntropy ⋯ = ↑(Hnu ν)

The constant-roof Bernoulli suspension's time-1 map has Kolmogorov–Sinai entropy Hnu ν.

The fundamental-domain equivalence suspensionUnitMeasurableEquiv conjugates the time-1 map to the frozen product biShiftEquiv × id on BiShift α₀ × ↥(Set.Ico 0 1), and maps the suspension measure to bernZ ν × fibreMeasure; hence by conjugacy invariance, the frozen-factor product identity h(T × id) = h(T), and the two-sided Bernoulli system entropy h(T) = Hnu ν, the time-1 map has entropy Hnu ν.

theorem Oseledets.Multifractal.bernSuspensionFlow_ksEntropy_eq_Hnu {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : (bernSuspensionFlow ν).ksEntropy = ↑(Hnu ν)

The constant-roof Bernoulli suspension flow has metric entropy Hnu ν. Restatement of ksEntropy_bernSuspensionFlow_one_eq_Hnu in terms of the flow's metric entropy (MeasurePreservingFlow.ksEntropy, the entropy of the time-1 map).