The doubling map's binary join cells (dynamical crux)

This module isolates the dynamical facts behind Rokhlin's entropy equality for the doubling map T : y ↦ 2 • y on UnitAddCircle = AddCircle (1 : ℝ). Let α be the binary partition {[0,1/2), [1/2,1)} (the mk-images of those half-open real intervals). Its n-fold join ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α is the partition of the circle into the 2ⁿ dyadic arcs of length 2⁻ⁿ.

The crux volume_binJoinCell states that every cell of that n-fold join has volume exactly 2⁻ⁿ. Feeding it into the abstract reduction ksEntropyPartition_of_uniform (file AbstractEqui.lean) yields h(α, T) = log 2.

Structure of the argument

• ksJoinCells_succ_head_tail: the head/tail recursion Cₙ₊₁,f = α_{f 0} ∩ T⁻¹(Cₙ, tail f).
• mem_binCell_iff: a circle point lies in α_i iff its [0,1)-representative lies in binLift i = [i/2,(i+1)/2); this turns the mk-image cell into a measurable preimage.
• volume_binCell_inter_preimage: the dynamical heart, volume (α_i ∩ T⁻¹ B) = volume B / 2. The doubling map restricted to the half-arc α_i is the affine 2×-magnification x ↦ 2x - i onto the whole circle, so it halves measures. The proof reduces — via the fundamental-domain measure formula volume_eq_preimage_inter_Ico and Real.volume_preimage_mul_left (factor 1/2) — to the ℤ-translation invariance of mk⁻¹' B (preimage_mk_add_int_eq).
• volume_binJoinCell: induction on n via the head/tail recursion, halving the measure at each step from volume univ = 1.

For the integral side ∫ log|det D(2x)| dμ = ∫ log 2 = log 2 and the headline equality, see Oseledets.Examples.Rokhlin.DoublingEquality.

noncomputable def Oseledets.Examples.Rokhlin.binLift (i : Fin 2) : Set ℝ

Lift of the binary cell i ∈ {0, 1} to the fundamental domain [0, 1): the half-open real interval [i/2, (i+1)/2).

Equations

• Oseledets.Examples.Rokhlin.binLift i = Set.Ico (↑↑i / 2) ((↑↑i + 1) / 2)

noncomputable def Oseledets.Examples.Rokhlin.binCell (i : Fin 2) : Set UnitAddCircle

The i-th cell of the binary partition of the unit circle: the mk-image of [i/2, (i+1)/2).

Equations

• Oseledets.Examples.Rokhlin.binCell i = QuotientAddGroup.mk '' Oseledets.Examples.Rokhlin.binLift i

noncomputable def Oseledets.Examples.Rokhlin.rep (y : UnitAddCircle) : ℝ

The canonical [0,1)-representative of a circle point: AddCircle.equivIco 1 0 followed by the subtype coercion. It is the unique real in [0,1) mapping to the given point under mk.

Equations

• Oseledets.Examples.Rokhlin.rep y = ↑((AddCircle.equivIco 1 0) y)

theorem Oseledets.Examples.Rokhlin.rep_mem_Ico (y : UnitAddCircle) : rep y ∈ Set.Ico 0 1

@[simp]

theorem Oseledets.Examples.Rokhlin.mk_rep (y : UnitAddCircle) : ↑(rep y) = y

theorem Oseledets.Examples.Rokhlin.rep_coe_of_mem {x : ℝ} (hx : x ∈ Set.Ico 0 1) : rep ↑x = x

theorem Oseledets.Examples.Rokhlin.binLift_subset_Ico (i : Fin 2) : binLift i ⊆ Set.Ico 0 1

The lifted binary interval [i/2,(i+1)/2) sits inside the fundamental domain [0,1).

theorem Oseledets.Examples.Rokhlin.mem_binCell_iff (i : Fin 2) (y : UnitAddCircle) : y ∈ binCell i ↔ rep y ∈ binLift i

Characterization of a binary cell via the canonical representative. A circle point lies in binCell i iff its [0,1)-representative lies in the lifted interval binLift i = [i/2,(i+1)/2). This turns the mk-image cell into a preimage of a measurable real set under the measurable map rep, and is the workhorse for measurability, disjointness, and cover.

theorem Oseledets.Examples.Rokhlin.ksJoinCells_succ_head_tail {ι : Type u_1} (cells : ι → Set UnitAddCircle) (T : UnitAddCircle → UnitAddCircle) (n : ℕ) (f : Fin (n + 1) → ι) : Entropy.ksJoinCells cells T (n + 1) f = cells (f 0) ∩ T ⁻¹' Entropy.ksJoinCells cells T n (Fin.tail f)

Head/tail decomposition of an iterated-join cell. Splitting off the k = 0 factor, ⋂ₖ₌₀ⁿ T⁻ᵏ(α_{f k}) = α_{f 0} ∩ T⁻¹(⋂ₖ₌₀ⁿ⁻¹ T⁻ᵏ(α_{(tail f) k})). The shifted factors at k = j+1 are T⁻¹ of the corresponding n-fold-join factor because T^[j+1] = T^[j] ∘ T.

Measurability of the binary cells

theorem Oseledets.Examples.Rokhlin.measurable_rep : Measurable rep

The canonical representative map rep = Subtype.val ∘ equivIco 1 0 is measurable: it is the forward map of the measurable equivalence AddCircle.measurableEquivIco 1 0 post-composed with the measurable subtype coercion.

theorem Oseledets.Examples.Rokhlin.measurableSet_binCell (i : Fin 2) : MeasurableSet (binCell i)

The binary cells are measurable: by mem_binCell_iff, binCell i = rep ⁻¹' binLift i, the preimage of the measurable real interval binLift i under the measurable map rep.

The dynamical half-scaling lemma

The single genuinely-dynamical input: the two doubling-map branches each magnify by 2, so each halves measures.

theorem Oseledets.Examples.Rokhlin.doublingMap_mk (x : ℝ) : doublingMap ↑x = ↑(2 * x)

The doubling map in mk-coordinates: T (mk x) = mk (2 x).

theorem Oseledets.Examples.Rokhlin.preimage_mk_add_int_eq {B : Set UnitAddCircle} (k : ℤ) : (fun (x : ℝ) => x + ↑k) ⁻¹' QuotientAddGroup.mk ⁻¹' B = QuotientAddGroup.mk ⁻¹' B

mk⁻¹' B is invariant under translation by an integer (here i ∈ {0,1} ⊆ ℤ): mk (x + i) = mk x, so x + i ∈ mk⁻¹' B ↔ x ∈ mk⁻¹' B. We phrase it as a set translation identity.

theorem Oseledets.Examples.Rokhlin.volume_eq_preimage_inter_Ico {U : Set UnitAddCircle} (hU : MeasurableSet U) : MeasureTheory.volume U = MeasureTheory.volume (QuotientAddGroup.mk ⁻¹' U ∩ Set.Ico 0 1)

Fundamental-domain measure formula with the half-open [0,1) domain (the Ico analogue of AddCircle.add_projection_respects_measure): for measurable U, volume U = volume (mk⁻¹' U ∩ [0,1)). Obtained from the Ioc 0 1 version by measure_congr, since Ioc 0 1 =ᵐ Ico 0 1.

theorem Oseledets.Examples.Rokhlin.volume_binCell_inter_preimage (i : Fin 2) {B : Set UnitAddCircle} (hB : MeasurableSet B) : MeasureTheory.volume (binCell i ∩ doublingMap ⁻¹' B) = MeasureTheory.volume B / 2

Half-scaling under the doubling map. For any measurable B ⊆ UnitAddCircle, the part of the preimage T⁻¹ B lying in the binary half-arc α_i = binCell i has exactly half the measure of B. Indeed T restricted to α_i = [i/2,(i+1)/2) is the affine map x ↦ 2x - i onto the whole circle (a measure 2×-magnification), so it pulls B back to a set of half the measure inside α_i.

The join cell measure

theorem Oseledets.Examples.Rokhlin.volume_binJoinCell (n : ℕ) (f : Fin n → Fin 2) : MeasureTheory.volume (Entropy.ksJoinCells binCell doublingMap n f) = (2 ^ n)⁻¹

Every binary n-fold-join cell of the doubling map has volume 2⁻ⁿ. Induction on n using the head/tail recursion ksJoinCells_succ_head_tail and the half-scaling lemma volume_binCell_inter_preimage: the base cell (n = 0) is the whole circle of measure 1, and each step multiplies the measure by 1/2.