Ergodicity of the constant-roof Bernoulli suspension flow (and the time-1 failure)

This module completes the dynamical picture of the constant-roof (τ ≡ 1) suspension flow bernSuspensionFlow ν built in Oseledets.Multifractal.BernoulliSuspensionFlow. It establishes the sharp contrast between the full ℝ-flow and its time-1 map:

• The full ℝ-flow is ergodic iff the base shift is ergodic. A measurable set invariant under all time-t maps ζ_t (t ∈ ℝ) is null or conull, provided the two-sided Bernoulli base shift biShiftEquiv is ergodic for bernZ ν (ergodic_bernSuspensionFlow).

• The time-1 map is not ergodic. For the constant roof τ ≡ 1 the time-1 map of the flow is, on the fundamental box BiShift α₀ × [0, 1), the skew map (x, s) ↦ (T x, s): it leaves the section coordinate s untouched. Hence the saturated section set {[x, s] | s < 1/2} is a nontrivial time-1-invariant set, witnessing the failure of ergodicity (not_ergodic_bernSuspensionFlow_one).

Why the time-1 map fails but the full flow succeeds

The eigenfunction g(x, s) = e^{2π i s} on the suspension is a (non-constant) eigenfunction of the time-1 map with eigenvalue 1: g ∘ ζ_1 = g, because ζ_1 [x, s] = [x, s + 1] = [T x, s] only re-bases the height, leaving e^{2π i s} fixed. A non-constant time-1-invariant function blocks ergodicity of ζ_1. The full flow, by contrast, moves the section coordinate continuously, so g ∘ ζ_t = e^{2π i t} g is a genuine (non-trivial) eigenfunction of the flow's generator — there is no non-constant function invariant under all ζ_t. This is the constant-roof special-flow dichotomy of Cornfeld–Fomin–Sinai (Ergodic Theory, Springer 1982, Ch. 11): a special flow under a constant roof is ergodic iff its base map is ergodic, even though no power (in particular the time-1 map) of such a flow is ever ergodic.

Proof of the flow ergodicity

The crux is purely the all-translation invariance, requiring no circle ergodicity. Let A ⊆ SuspensionSpace be invariant under every ζ_t. Lifting to the box BiShift α₀ × ℝ through the quotient map π = suspensionMk:

1. All vertical translations fix the lift. For every t and (x, s), π (x, s) ∈ A ↔ ζ_t (π (x, s)) ∈ A ↔ π (x, s + t) ∈ A, using π ∘ S_t = ζ_t ∘ π and ζ_t ⁻¹' A = A. Taking t = s from base height 0, membership of π (x, s) in A depends only on the base point x, through B := {x | π (x, 0) ∈ A}. So the lift is the cylinder B ×ˢ univ.

2. The base set is shift-invariant. The generator G (x, s) = (T x, s − 1) keeps π fixed (π (G p) = π p), so π (x, s) ∈ A ↔ π (T x, s − 1) ∈ A, i.e. x ∈ B ↔ T x ∈ B. Thus biShiftEquiv ⁻¹' B = B.

3. Apply base ergodicity. B is measurable and shift-invariant, so bernZ ν B ∈ {0, 1} by hbase. The constant-roof box mass is μ̂ A = (bernZ ν × volume) (B ×ˢ Ico 0 1) = bernZ ν B · 1, so μ̂ A ∈ {0, 1}.

Main results

• Oseledets.Multifractal.suspensionMeasure_eq_bernZ_base_of_flowInvariant: for a flow-invariant measurable A, μ̂ A = bernZ ν B with B = {x | π (x, 0) ∈ A} the (shift-invariant) base set.
• Oseledets.Multifractal.ergodic_bernSuspensionFlow: the conditional flow ergodicity — every all-t-invariant measurable set is null or conull, given base ergodicity.
• Oseledets.Multifractal.not_ergodic_bernSuspensionFlow_one: the time-1 map is not ergodic (the saturated section set {[x, s] | s < 1/2} is a nontrivial invariant set).

The generator fixes the quotient projection

theorem Oseledets.Multifractal.suspensionMk_suspensionGen {α₀ : Type u_1} [MeasurableSpace α₀] (p : BiShift α₀ × ℝ) : suspensionMk biShiftEquiv ⋯ ((suspensionGen biShiftEquiv ⋯) p) = suspensionMk biShiftEquiv ⋯ p

The orbit generator G (x, s) = (T x, s − τ x) keeps the quotient projection fixed: suspensionMk (suspensionGen p) = suspensionMk p, since p and G p = (-1) •ᵥ⁻¹ … lie in the same ℤ-orbit. (Here specialised to G p = suspensionAct 1 p.)

The base set of a flow-invariant set and its shift-invariance

def Oseledets.Multifractal.flowInvariantBase {α₀ : Type u_1} [MeasurableSpace α₀] (A : Set (SuspensionSpace biShiftEquiv ⋯)) : Set (BiShift α₀)

The base set of a measurable set A on the suspension: the points x whose height-0 representative [x, 0] lies in A. For a flow-invariant A this is the cylinder base (mem_suspensionMk_iff_mem_base) and is shift-invariant (base_set_shift_invariant).

Equations

• Oseledets.Multifractal.flowInvariantBase A = {x : Oseledets.Multifractal.BiShift α₀ | Oseledets.suspensionMk Oseledets.Multifractal.biShiftEquiv ⋯ (x, 0) ∈ A}

@[simp]

theorem Oseledets.Multifractal.mem_flowInvariantBase {α₀ : Type u_1} [MeasurableSpace α₀] {A : Set (SuspensionSpace biShiftEquiv ⋯)} (x : BiShift α₀) : x ∈ flowInvariantBase A ↔ suspensionMk biShiftEquiv ⋯ (x, 0) ∈ A

theorem Oseledets.Multifractal.measurableSet_flowInvariantBase {α₀ : Type u_1} [MeasurableSpace α₀] {A : Set (SuspensionSpace biShiftEquiv ⋯)} (hA : MeasurableSet A) : MeasurableSet (flowInvariantBase A)

The base set is measurable: it is the preimage of A along the measurable composite x ↦ suspensionMk (x, 0).

theorem Oseledets.Multifractal.mem_suspensionMk_iff_mem_base {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] {A : Set (SuspensionSpace biShiftEquiv ⋯)} (hinv : ∀ (t : ℝ), (bernSuspensionFlow ν).toFun t ⁻¹' A = A) (x : BiShift α₀) (s : ℝ) : suspensionMk biShiftEquiv ⋯ (x, s) ∈ A ↔ x ∈ flowInvariantBase A

Cylinder structure of a flow-invariant set. For an A invariant under every time-t map of the flow, membership of [x, s] in A depends only on the base point x (through the base set), for every height s: [x, s] ∈ A ↔ x ∈ flowInvariantBase A.

Using the descent commutation ζ_t ∘ π = π ∘ S_t (suspensionFlowMap_mk) and the invariance ζ_s ⁻¹' A = A, the height s can be translated away to the base height 0: [x, s] = ζ_s [x, 0] ∈ A ↔ [x, 0] ∈ A.

theorem Oseledets.Multifractal.base_set_shift_invariant {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] {A : Set (SuspensionSpace biShiftEquiv ⋯)} (hinv : ∀ (t : ℝ), (bernSuspensionFlow ν).toFun t ⁻¹' A = A) : ⇑biShiftEquiv ⁻¹' flowInvariantBase A = flowInvariantBase A

Shift-invariance of the base set. For a flow-invariant A, the base set is invariant under the two-sided Bernoulli shift: biShiftEquiv ⁻¹' (flowInvariantBase A) = flowInvariantBase A.

The orbit generator G (x, s) = (T x, s − 1) keeps the quotient projection fixed (suspensionMk_suspensionGen), so [T x, −1] = [x, 0]. Specialising the cylinder identity mem_suspensionMk_iff_mem_base at (T x, −1) gives T x ∈ base ↔ [T x, −1] ∈ A ↔ [x, 0] ∈ A ↔ x ∈ base.

The suspension mass of a flow-invariant set

theorem Oseledets.Multifractal.suspensionMeasure_eq_bernZ_base_of_flowInvariant {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] {A : Set (SuspensionSpace biShiftEquiv ⋯)} (hA : MeasurableSet A) (hinv : ∀ (t : ℝ), (bernSuspensionFlow ν).toFun t ⁻¹' A = A) : (suspensionMeasure biShiftEquiv ⋯ (bernZ ν)) A = (bernZ ν) (flowInvariantBase A)

The constant-roof mass of a flow-invariant set is the base mass. For a flow-invariant measurable A, the suspension probability μ̂ A equals bernZ ν of the base set B = flowInvariantBase A.

For τ ≡ 1 the box is BiShift α₀ × [0, 1) and μ̂ = μ̂₀ (suspensionMeasure_oneRoof_eq). The preimage of A through the quotient, intersected with the box, equals B ×ˢ Ico 0 1 by the cylinder identity mem_suspensionMk_iff_mem_base (membership depends only on the base point), so the product mass is bernZ ν B · volume (Ico 0 1) = bernZ ν B · 1.

The conditional flow ergodicity (T2)

theorem Oseledets.Multifractal.ergodic_bernSuspensionFlow {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] (hbase : Ergodic (⇑biShiftEquiv) (bernZ ν)) {A : Set (SuspensionSpace biShiftEquiv ⋯)} (hA : MeasurableSet A) (hinv : ∀ (t : ℝ), (bernSuspensionFlow ν).toFun t ⁻¹' A = A) : (suspensionMeasure biShiftEquiv ⋯ (bernZ ν)) A = 0 ∨ (suspensionMeasure biShiftEquiv ⋯ (bernZ ν)) A = 1

Ergodicity of the constant-roof Bernoulli suspension flow (conditional on base ergodicity).

Given that the two-sided Bernoulli shift biShiftEquiv is ergodic for bernZ ν (hbase), every measurable set A invariant under all time-t maps of the suspension flow is null or conull: μ̂ A = 0 ∨ μ̂ A = 1.

By suspensionMeasure_eq_bernZ_base_of_flowInvariant the mass μ̂ A equals bernZ ν B for the base set B = flowInvariantBase A, which is measurable (measurableSet_flowInvariantBase) and shift-invariant (base_set_shift_invariant); base ergodicity's zero-one law (PreErgodic.prob_eq_zero_or_one) gives bernZ ν B ∈ {0, 1}.

The time-1 map is NOT ergodic (P1)

theorem Oseledets.Multifractal.roofSum_oneRoof {α₀ : Type u_1} [MeasurableSpace α₀] (n : ℤ) (x : BiShift α₀) : roofSum biShiftEquiv ⋯ n x = ↑n

The constant roof has integer roof sums: roofSum n x = n for τ ≡ 1. Each lap step adds τ (·) = 1, so the integer roof sum telescopes to n.

noncomputable def Oseledets.Multifractal.fractHeight {α₀ : Type u_1} [MeasurableSpace α₀] : SuspensionSpace biShiftEquiv ⋯ → ℝ

The fractional height descends to the suspension quotient: the orbit-invariant value Int.fract s of a representative's height. Well-defined because the orbit generator subtracts the integer roof 1 from the height (and a general orbit element subtracts the integer n), leaving Int.fract unchanged.

Equations

• Oseledets.Multifractal.fractHeight = Quotient.lift (fun (p : Oseledets.Multifractal.BiShift α₀ × ℝ) => Int.fract p.2) ⋯

@[simp]

theorem Oseledets.Multifractal.fractHeight_mk {α₀ : Type u_1} [MeasurableSpace α₀] (p : BiShift α₀ × ℝ) : fractHeight (suspensionMk biShiftEquiv ⋯ p) = Int.fract p.2

theorem Oseledets.Multifractal.measurable_fractHeight {α₀ : Type u_1} [MeasurableSpace α₀] : Measurable fractHeight

The fractional-height descent is measurable: out of the quotient it is the descent of the measurable map p ↦ Int.fract p.2.

def Oseledets.Multifractal.sectionHalf {α₀ : Type u_1} [MeasurableSpace α₀] : Set (SuspensionSpace biShiftEquiv ⋯)

The saturated section set {q | fractHeight q < 1/2} on the suspension: the orbit-invariant descent of the half-open height slab {[x, s] | Int.fract s < 1/2}. For the constant roof it is a nontrivial time-1-invariant set, the witness to the failure of time-1 ergodicity.

Equations

• Oseledets.Multifractal.sectionHalf = Oseledets.Multifractal.fractHeight ⁻¹' Set.Iio (1 / 2)

theorem Oseledets.Multifractal.measurableSet_sectionHalf {α₀ : Type u_1} [MeasurableSpace α₀] : MeasurableSet sectionHalf

The section set is measurable: it is the preimage of Iio (1/2) along the measurable fractional-height descent.

theorem Oseledets.Multifractal.sectionHalf_flow_one_invariant {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : (bernSuspensionFlow ν).toFun 1 ⁻¹' sectionHalf = sectionHalf

The section set is ζ_1-invariant. The time-1 map adds 1 to the representative's height, which leaves Int.fract unchanged (Int.fract_add_one); hence fractHeight ∘ ζ_1 = fractHeight, so the preimage {fractHeight < 1/2} is ζ_1-invariant.

theorem Oseledets.Multifractal.suspensionMeasure_sectionHalf {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : (suspensionMeasure biShiftEquiv ⋯ (bernZ ν)) sectionHalf = 1 / 2

The section set has mass 1/2. For τ ≡ 1 the box is BiShift α₀ × [0, 1) and μ̂ = μ̂₀; the preimage of sectionHalf through the quotient intersected with the box is the half-box BiShift α₀ × [0, 1/2) (on the box Int.fract s = s), of product mass bernZ ν univ · volume (Ico 0 (1/2)) = 1 · (1/2).

theorem Oseledets.Multifractal.not_ergodic_bernSuspensionFlow_one {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : ¬Ergodic ((bernSuspensionFlow ν).toFun 1) (suspensionMeasure biShiftEquiv ⋯ (bernZ ν))

The time-1 map of the constant-roof Bernoulli suspension flow is not ergodic.

For τ ≡ 1 the time-1 map is ζ_1 [x, s] = [x, s + 1] = [T x, s]: it fixes the fractional part of the height. Hence the saturated section set sectionHalf = {q | fractHeight q < 1/2} is ζ_1-invariant (sectionHalf_flow_one_invariant), measurable (measurableSet_sectionHalf), and has mass 1/2 (suspensionMeasure_sectionHalf) — strictly between 0 and 1. So the zero-one law fails: ζ_1 is not ergodic.

This is the honest obstruction documented in the module header: the eigenfunction e^{2π i s} of the flow generator descends to a non-constant ζ_1-invariant function (eigenvalue e^{2π i · 1} = 1), so no constant-roof special flow's time-1 map is ever ergodic.

Unconditional flow ergodicity (the base hypothesis discharged)

theorem Oseledets.Multifractal.ergodic_bernSuspensionFlow_uncond {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] {A : Set (SuspensionSpace biShiftEquiv ⋯)} (hA : MeasurableSet A) (hinv : ∀ (t : ℝ), (bernSuspensionFlow ν).toFun t ⁻¹' A = A) : (suspensionMeasure biShiftEquiv ⋯ (bernZ ν)) A = 0 ∨ (suspensionMeasure biShiftEquiv ⋯ (bernZ ν)) A = 1

The constant-roof Bernoulli suspension flow is ergodic, unconditionally. Discharges the base-ergodicity hypothesis of ergodic_bernSuspensionFlow with the proved two-sided Bernoulli ergodicity (ergodic_biShiftEquiv_bernZ, the mixing/cylinder-approximation keystone): every measurable set invariant under all time-t maps of the flow is null or conull. The time-1 map stays non-ergodic (not_ergodic_bernSuspensionFlow_one) — only the full flow is ergodic.