Documentation

Oseledets.Multifractal.BernoulliSuspensionWitness

The multifractal witness of the Bernoulli suspension flow (issue #19, deliverable (ii)) #

Issue #19 asks for two deliverables for the constant-roof (τ ≡ 1) suspension flow of the two-sided asymmetric Bernoulli shift:

The witness partition #

The witness is the base coordinate partition pulled back along the base projection (factor map) π := suspensionBaseProj:

P := (coordPartitionZFin (bernZ ν)).pulledBack (measurePreserving_suspensionBaseProj ν),

a Fin (Fintype.card α₀)-indexed measurable partition of the flow measure μ̂.

The mass identity (the crux) #

The load-bearing fact is that pulling the base coordinate partition back along the measure-preserving π does not change the cell masses: for each Fin-index j,

μ̂ (P.cells j) = bernZ ν ((coordPartitionZFin (bernZ ν)).cells j) = ν {(Fintype.equivFin α₀).symm j}.

The first equality is (measurePreserving_suspensionBaseProj ν).measure_preimage on the (measurable) cell; the second is the two-sided marginal identity measure_coordPartitionZ_cell_bernZ (the 0-th coordinate of an i.i.d. product is distributed as ν), reindexed by (Fintype.equivFin α₀).symm.

Main results #

The two-sided marginal identity #

source
theorem Oseledets.Multifractal.measure_coordPartitionZ_cell_bernZ {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] (a : α₀) :
(bernZ ν) ((coordPartitionZ (bernZ ν)).cells a) = ν {a}

Marginal identity for the coordinate partition of the two-sided Bernoulli measure. The mass that the two-sided i.i.d. product measure bernZ ν assigns to the 0-th coordinate cell (coordPartitionZ (bernZ ν)).cells a = {x | x 0 = a} is the single-symbol mass ν {a}. The cell is the measurable cylinder box Set.pi ↑({0} : Finset ℤ) (fun _ => {a}), whose bernZ ν-mass factorizes (bernZ_pi_eq_prod) to the single-coordinate product ∏ i ∈ {0}, ν {a} = ν {a}. This is the two-sided mirror of the one-sided measure_coordPartition_cell_bern.

The witness partition #

source
noncomputable def Oseledets.Multifractal.bernSuspensionWitness {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] :
Entropy.MeasurePartition (suspensionMeasure biShiftEquiv ⋯ (bernZ ν)) (Fin (Fintype.card α₀))

The witness partition of the constant-roof Bernoulli suspension flow's invariant measure μ̂ := suspensionMeasure biShiftEquiv measurable_oneRoof (bernZ ν): the base coordinate partition coordPartitionZFin (bernZ ν) pulled back along the base projection (factor map) π := suspensionBaseProj, which is measure-preserving onto bernZ ν (measurePreserving_suspensionBaseProj). Its cell at j : Fin (Fintype.card α₀) is π ⁻¹' ((coordPartitionZFin (bernZ ν)).cells j).

Equations
Instances For
    source
    theorem Oseledets.Multifractal.measure_bernSuspensionWitness_cell {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] (j : Fin (Fintype.card α₀)) :
    (suspensionMeasure biShiftEquiv ⋯ (bernZ ν)) ((bernSuspensionWitness ν).cells j) = ν {(Fintype.equivFin α₀).symm j}

    The mass identity (the crux). The μ̂-mass of the j-th witness cell equals the single-symbol mass ν {(Fintype.equivFin α₀).symm j} of the corresponding base symbol. The cell is the π-preimage of the base cell (pulledBack_cells); pulling it through the measure-preserving π (measure_preimage) gives the base mass bernZ ν ((coordPartitionZFin (bernZ ν)).cells j), which is the reindexed two-sided marginal identity measure_coordPartitionZ_cell_bernZ.

    source
    theorem Oseledets.Multifractal.measure_bernSuspensionWitness_cell_toReal {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] (j : Fin (Fintype.card α₀)) :
    ((suspensionMeasure biShiftEquiv ⋯ (bernZ ν)) ((bernSuspensionWitness ν).cells j)).toReal = (ν {(Fintype.equivFin α₀).symm j}).toReal

    The real-valued mass identity, the form consumed by IsHeterogeneous and the Rényi spectrum: (μ̂ (P.cells j)).toReal = (ν {(Fintype.equivFin α₀).symm j}).toReal.

    Heterogeneity of the witness #

    source
    theorem Oseledets.Multifractal.isHeterogeneous_bernSuspensionWitness {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] {i j : α₀} (_hij : i ≠ j) (hbias : ν {i} ≠ ν {j}) :
    IsHeterogeneous (suspensionMeasure biShiftEquiv ⋯ (bernZ ν)) (bernSuspensionWitness ν)

    The witness partition is heterogeneous. For a biased single-symbol law ν charging two distinct symbols i ≠ j with different masses (ν {i} ≠ ν {j}), the witness cells indexed by Fintype.equivFin α₀ i and Fintype.equivFin α₀ j carry masses ν {i} and ν {j} (the mass identity measure_bernSuspensionWitness_cell), which differ; hence IsHeterogeneous μ̂ (bernSuspensionWitness ν).

    The headline q-dependence (transfer route) #

    source
    theorem Oseledets.Multifractal.partitionFunctionMeasure_bernSuspensionWitness_eq {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] (q : ℝ) :
    partitionFunctionMeasure (suspensionMeasure biShiftEquiv ⋯ (bernZ ν)) (bernSuspensionWitness ν) q = partitionFunctionMeasure (bern ν) (coordPartition (bern ν)) q

    The cell-mass families of the flow witness and the one-sided base witness agree up to the α₀ ≃ Fin reindex. Both Rényi spectra depend only on the cell-mass family, and these agree (each cell carries a single-symbol mass ν {·}), so the flow's partition function at every q equals the one-sided base partition function partitionFunctionMeasure (bern ν) (coordPartition (bern ν)). The reindex Fintype.equivFin α₀ is summed away by Equiv.sum_comp.

    source
    theorem Oseledets.Multifractal.renyiDimFlow_bernSuspension_q_dependent {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] [DecidableEq α₀] {i j : α₀} (hij : i ≠ j) (huniv : Finset.univ = {i, j}) (hbias : (ν {i}).toReal ≠ (ν {j}).toReal) (hi : 0 < (ν {i}).toReal) (hj : 0 < (ν {j}).toReal) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) :
    ∃ (q₁ : ℝ) (q₂ : ℝ), renyiDimFlow (bernSuspensionFlow ν) (bernSuspensionWitness ν) ε q₁ ≠ renyiDimFlow (bernSuspensionFlow ν) (bernSuspensionWitness ν) ε q₂

    THE HEADLINE (deliverable (ii)): genuine q-dependence of the Bernoulli suspension flow's Rényi spectrum. For a scale 0 < ε < 1 and a biased 2-symbol law ν (exactly two symbols i ≠ j, both of positive mass, with (ν {i}).toReal ≠ (ν {j}).toReal), the Rényi (generalized) dimension of the flow's invariant measure μ̂ for the witness partition takes different values at two explicit exponents. Concretely D₀ = log 2 / (-log ε) (both atoms occupied) and D₁ = Hnu ν / (-log ε) (the information dimension), and these differ precisely because Hnu ν < log 2 — the strict bias bound Hnu_lt_log_two. This is the non-vacuous witness: the inequality is driven by the genuine bias of ν, not satisfied trivially.

    The proof transfers to the already-established one-sided base witness renyiDimMeasure_q_dependent_bern: since renyiDimFlow (bernSuspensionFlow ν) P ε q unfolds definitionally to renyiDimMeasure μ̂ P ε q, and renyiDimMeasure depends only on the cell-mass family — which agrees with that of bern ν up to the α₀ ≃ Fin reindex (partitionFunctionMeasure_bernSuspensionWitness_eq, hence equal renyiDimMeasure at every q) — the flow q-dependence is exactly the base q-dependence.