The Bernoulli witness for the symbolic entropy–dimension identity

The conditional headline dimH_eq_ksEntropy_div_log_two (Oseledets/Multifractal/SymbolicDimension.lean) is stated for an abstract ergodic shift-invariant probability measure on the one-sided full shift with positive coordinate-partition entropy. This file lays the foundation of the concrete Bernoulli witness that discharges those two conditionals: it equips the full shift Shift α₀ over a finite alphabet with the i.i.d. (Bernoulli) product measure of a single-symbol law ν, and supplies the easy structural facts.

The construction proceeds in (currently three) foundation nodes.

• N1 (probability). The Bernoulli measure bern ν := Measure.infinitePi (fun _ => ν) is a probability measure when ν is.
• N2 (measure preservation). The left shift shiftMap preserves bern ν: the preimage of a measurable box Set.pi ↑s t is the box re-indexed by n ↦ n + 1, and both sides evaluate by infinitePi_pi to the same finite product of ν-masses (every marginal is the same ν, and Finset.prod_map absorbs the injective reindex).
• N4b (positive entropy). The single-symbol Shannon entropy Hnu ν := ∑ i, negMulLog (ν {i}).toReal is strictly positive once ν charges two distinct symbols, because every summand is nonnegative and the two charged ones are strictly positive.

The ergodicity (N3) and the entropy identification (N4a, Hnu ν = ksEntropy) are separate later nodes; they are not attempted here.

Definitions

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

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

Equations

• Oseledets.Multifractal.bern ν = MeasureTheory.Measure.infinitePi fun (x : ℕ) => ν

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

The single-symbol Shannon entropy of the law ν: Hnu ν = ∑ i, negMulLog (ν {i}).toReal. For a Bernoulli measure this is the Kolmogorov–Sinai entropy of the coordinate partition (proved in a later node).

Equations

• Oseledets.Multifractal.Hnu ν = ∑ i : α₀, (ν {i}).toReal.negMulLog

N1 — the Bernoulli measure is a probability measure

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

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

N2 — the shift preserves the Bernoulli measure

def Oseledets.Multifractal.shiftEmb : ℕ ↪ ℕ

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

Equations

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

theorem Oseledets.Multifractal.preimage_shiftMap_pi {α₀ : Type u_1} (s : Finset ℕ) (t : ℕ → Set α₀) : shiftMap ⁻¹' (↑s).pi t = (↑(Finset.map shiftEmb s)).pi fun (n : ℕ) => t (n - 1)

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

theorem Oseledets.Multifractal.measurePreserving_shiftMap_bern {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.MeasurePreserving shiftMap (bern ν) (bern ν)

N2. The left shift map preserves the Bernoulli measure bern ν. The preimage of a box re-indexes by n ↦ n + 1 (preimage_shiftMap_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.

N4b — the single-symbol entropy is positive

theorem Oseledets.Multifractal.measureReal_singleton_le_one {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] (a : α₀) : (ν {a}).toReal ≤ 1

The mass (ν {a}).toReal of any single symbol lies in [0, 1].

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

N4b. The single-symbol Shannon entropy Hnu ν is strictly positive once ν charges two distinct symbols i ≠ j with positive toReal-mass. Every summand negMulLog (ν {a}).toReal is nonnegative (the mass lies in [0, 1]), and the i-summand is strictly positive because (ν {i}).toReal ∈ (0, 1): the upper bound (ν {i}).toReal < 1 follows from ν {i} + ν {j} ≤ ν univ = 1 (disjoint singletons) together with 0 < (ν {j}).toReal.