The two-sided Bernoulli foundation: an invertible shift base

The suspension/flow construction (Oseledets/Continuous/Suspension*.lean) requires an invertible base automorphism T : X ≃ᵐ X. The on-main one-sided Bernoulli shift (Oseledets/Multifractal/SymbolicDimensionBernoulli.lean) is non-invertible. This file builds the two-sided analogue: the full shift over the index type ℤ, equipped with the i.i.d. (Bernoulli) product measure, with the left shift packaged as a MeasurableEquiv.

The construction mirrors the one-sided foundation node for node, over ℤ instead of ℕ.

• The bi-infinite shift space BiShift α₀ := ∀ _ : ℤ, α₀ with its product MeasurableSpace.
• The shift map biShiftMap x n = x (n + 1) and its measurability.
• The invertible shift biShiftEquiv : BiShift α₀ ≃ᵐ BiShift α₀, built as an explicit MeasurableEquiv.mk: the forward map n ↦ x (n + 1), the inverse n ↦ x (n - 1), with the two round-trip identities closing by (n + 1) - 1 = n and (n - 1) + 1 = n on ℤ.
• The Bernoulli measure bernZ ν := Measure.infinitePi (fun _ : ℤ => ν), a probability measure.
• Measure preservation measurePreserving_biShiftEquiv_bernZ: the shift preserves bernZ ν, proved exactly as in the one-sided case (preimage_biShiftMap_pi re-indexes a box by n ↦ n + 1, then both sides evaluate by infinitePi_pi to the same finite product of ν-masses).
• Cylinder mass bernZ_pi_eq_prod: the cylinder-mass factorization bernZ ν (Set.pi ↑s t) = ∏ i ∈ s, ν (t i), the key handle for the entropy identification.
• The coordinate-0 partition coordPartitionZ.

The single-symbol Shannon entropy Hnu (alphabet-only) is reused unchanged from the one-sided file; there is deliberately no two-sided HnuZ.

The bi-infinite shift space and the shift map

@[reducible, inline]

abbrev Oseledets.Multifractal.BiShift (α₀ : Type u_2) : Type u_2

The two-sided full shift space over the alphabet α₀: bi-infinite sequences ℤ → α₀. It carries the product MeasurableSpace.

Equations

• Oseledets.Multifractal.BiShift α₀ = (ℤ → α₀)

def Oseledets.Multifractal.biShiftMap {α₀ : Type u_1} : BiShift α₀ → BiShift α₀

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

Equations

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

theorem Oseledets.Multifractal.measurable_biShiftMap {α₀ : Type u_1} [MeasurableSpace α₀] : Measurable biShiftMap

The two-sided shift map is measurable: each output coordinate is a measurable coordinate projection of the input.

The invertible shift

def Oseledets.Multifractal.biShiftEquiv {α₀ : Type u_1} [MeasurableSpace α₀] : BiShift α₀ ≃ᵐ BiShift α₀

The invertible left shift on the two-sided full shift, as a MeasurableEquiv. The forward map is n ↦ x (n + 1) and the inverse is n ↦ x (n - 1); on ℤ the round trips close by (n + 1) - 1 = n and (n - 1) + 1 = n.

Equations

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

@[simp]

theorem Oseledets.Multifractal.biShiftEquiv_apply {α₀ : Type u_1} [MeasurableSpace α₀] (x : BiShift α₀) : biShiftEquiv x = biShiftMap x

theorem Oseledets.Multifractal.coe_biShiftEquiv {α₀ : Type u_1} [MeasurableSpace α₀] : ⇑biShiftEquiv = biShiftMap

The coercion of biShiftEquiv is definitionally the shift map biShiftMap.

@[simp]

theorem Oseledets.Multifractal.biShiftEquiv_symm_apply {α₀ : Type u_1} [MeasurableSpace α₀] (x : BiShift α₀) (n : ℤ) : biShiftEquiv.symm x n = x (n - 1)

The two-sided Bernoulli measure

noncomputable def Oseledets.Multifractal.bernZ {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) : MeasureTheory.Measure (BiShift α₀)

The two-sided Bernoulli (i.i.d.) measure on the full shift BiShift α₀: the infinite product of the single-symbol law ν over all integer coordinates.

Equations

• Oseledets.Multifractal.bernZ ν = MeasureTheory.Measure.infinitePi fun (x : ℤ) => ν

instance Oseledets.Multifractal.instIsProbabilityMeasureBernZ {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.IsProbabilityMeasure (bernZ ν)

The two-sided Bernoulli measure is a probability measure. (The global instance on infinitePi does not fire through the bernZ definition, so it is provided explicitly.)

Measure preservation

def Oseledets.Multifractal.shiftEmbZ : ℤ ↪ ℤ

The coordinate-shift embedding n ↦ n + 1 of ℤ into itself. Used to re-index a measurable box under the shift preimage.

Equations

• Oseledets.Multifractal.shiftEmbZ = { toFun := fun (n : ℤ) => n + 1, inj' := Oseledets.Multifractal.shiftEmbZ._proof_1 }

theorem Oseledets.Multifractal.preimage_biShiftMap_pi {α₀ : Type u_1} (s : Finset ℤ) (t : ℤ → Set α₀) : biShiftMap ⁻¹' (↑s).pi t = (↑(Finset.map shiftEmbZ s)).pi fun (n : ℤ) => t (n - 1)

Box preimage. The biShiftMap-preimage of a measurable box Set.pi ↑s t is the box over the re-indexed support s.map shiftEmbZ with the symbol sets shifted by one: biShiftMap ⁻¹' (Set.pi ↑s t) = Set.pi ↑(s.map shiftEmbZ) (fun n => t (n - 1)).

theorem Oseledets.Multifractal.measurePreserving_biShiftEquiv_bernZ {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.MeasurePreserving (⇑biShiftEquiv) (bernZ ν) (bernZ ν)

Measure preservation. The invertible left shift preserves the two-sided Bernoulli measure bernZ ν. The preimage of a box re-indexes by n ↦ n + 1 (preimage_biShiftMap_pi); both sides evaluate by infinitePi_pi to the same finite product of ν-masses, since every marginal is the same ν and Finset.prod_map absorbs the injective reindex.

Cylinder mass

theorem Oseledets.Multifractal.bernZ_pi_eq_prod {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] (s : Finset ℤ) (t : ℤ → Set α₀) (ht : ∀ (i : ℤ), MeasurableSet (t i)) : (bernZ ν) ((↑s).pi t) = ∏ i ∈ s, ν (t i)

Cylinder-mass factorization. The two-sided Bernoulli mass of a measurable box Set.pi ↑s t is the finite product of the single-symbol masses ν (t i) over the support s. This is the key handle the entropy identification consumes.

The coordinate-0 partition

def Oseledets.Multifractal.coordPartitionZ {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure (BiShift α₀)) : Entropy.MeasurePartition ν α₀

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

Equations

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