The complete-block tower base and the residual estimate (Rokhlin tower, issue #15)

To build a Rokhlin tower of height N, one selects from the skyscraper over a small base set A only those floors that start a complete block of height N. This file constructs that tower base and proves the two facts the tower lemma needs from it:

• the N translates eⁱ '' B, i : Fin N, are pairwise disjoint (pairwise_disjoint_levels), and
• the uncovered residual (⋃ i, eⁱ '' B)ᶜ is small — it is contained, up to the null skyscraper complement, in the top incomplete floors, whose measure is bounded by ∑ k, ((k+1) mod N) · μ (returnLevel e A (k+1)) (measure_topFloors_le).

Main definitions

• Oseledets.Krieger.towerBase e A N — the union of floors e^[m·N] '' (returnLevel e A (k+1)) that begin a complete height-N block (guard (m+1)·N ≤ k+1).
• Oseledets.Krieger.coveredSet e A N — the union ⋃ i : Fin N, eⁱ '' (towerBase e A N).
• Oseledets.Krieger.topFloors e A N — the top incomplete floors ⌊(k+1)/N⌋·N ≤ j ≤ k of each column.

Main results

• pairwise_disjoint_levels — the N translates of the tower base are pairwise disjoint.
• compl_inter_skyscraper_subset_topFloors — (coveredSet)ᶜ ∩ skyscraper ⊆ topFloors.
• measure_topFloors_le — μ (topFloors e A N) ≤ ∑ k, ((k+1) mod N) · μ (returnLevel e A (k+1)).
• residual_lt_eps, residual_arith, tsum_residual_le, measure_gt_of_compl_lt — the ℝ≥0∞ arithmetic assembling the residual bound < ε.

The complete-block tower base and level disjointness

def Oseledets.Krieger.towerBase {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) (N : ℕ) : Set α

The tower base B: floors at heights m·N that START a complete block of height N inside a column of height k+1 (guard (m+1)·N ≤ k+1 ensures only complete blocks).

Equations

• Oseledets.Krieger.towerBase e A N = ⋃ (k : ℕ), ⋃ (m : ℕ), ⋃ (_ : (m + 1) * N ≤ k + 1), (⇑e)^[m * N] '' Oseledets.Krieger.returnLevel e A (k + 1)

theorem Oseledets.Krieger.measurableSet_towerBase {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) {A : Set α} (hA : MeasurableSet A) (N : ℕ) : MeasurableSet (towerBase e A N)

Measurability of the tower base.

theorem Oseledets.Krieger.image_towerBase {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) (N i : ℕ) : (⇑e)^[i] '' towerBase e A N = ⋃ (k : ℕ), ⋃ (m : ℕ), ⋃ (_ : (m + 1) * N ≤ k + 1), (⇑e)^[m * N + i] '' returnLevel e A (k + 1)

The key floor-rewrite: for the level i, eⁱ '' B is the union of floors at heights m·N + i.

theorem Oseledets.Krieger.pairwise_disjoint_levels {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) {N : ℕ} (_hN : 1 ≤ N) : Pairwise (Function.onFun Disjoint fun (i : Fin N) => (⇑e)^[↑i] '' towerBase e A N)

Level disjointness. The N levels eⁱ '' B, i : Fin N, are pairwise disjoint. The hypothesis 1 ≤ N is kept for a uniform call shape; i : Fin N already forces N ≥ 1 where it matters.

The residual arithmetic in ℝ≥0∞

theorem Oseledets.Krieger.residual_arith {N : ℕ} (hN : 1 ≤ N) {ε : ℝ} (hε : 0 < ε) {a : ENNReal} (ha : a < ENNReal.ofReal (ε / ↑N)) : ↑N * a < ENNReal.ofReal ε

The core arithmetic: with δ := ofReal (ε/N), a < δ implies N · a < ofReal ε.

theorem Oseledets.Krieger.tsum_residual_le {N : ℕ} (x : ℕ → ENNReal) (c : ℕ → ℕ) (hc : ∀ (k : ℕ), c k ≤ N) : ∑' (k : ℕ), ↑(c k) * x k ≤ ↑N * ∑' (k : ℕ), x k

The tsum residual bound: ∑ c_k · x_k ≤ N · ∑ x_k when c_k ≤ N.

theorem Oseledets.Krieger.measure_gt_of_compl_lt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {C : Set α} (hC : MeasurableSet C) {ε : ℝ} (hε1 : ENNReal.ofReal ε ≤ 1) (hcompl : μ Cᶜ < ENNReal.ofReal ε) : 1 - ENNReal.ofReal ε < μ C

Final assembly arithmetic: for a probability measure, μ Cᶜ < ofReal ε and ofReal ε ≤ 1 imply 1 - ofReal ε < μ C.

The residual-covering combinatorics

def Oseledets.Krieger.coveredSet {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) (N : ℕ) : Set α

The covered set C = ⋃ i < N, eⁱ '' B.

Equations

• Oseledets.Krieger.coveredSet e A N = ⋃ (i : Fin N), (⇑e)^[↑i] '' Oseledets.Krieger.towerBase e A N

def Oseledets.Krieger.topFloors {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) (N : ℕ) : Set α

The top incomplete floors: in column k+1, the floors at heights ⌊(k+1)/N⌋·N ≤ j ≤ k. These are the (k+1) mod N uncovered floors.

Equations

• Oseledets.Krieger.topFloors e A N = ⋃ (k : ℕ), ⋃ (j : ℕ), ⋃ (_ : (k + 1) / N * N ≤ j ∧ j ≤ k), (⇑e)^[j] '' Oseledets.Krieger.returnLevel e A (k + 1)

theorem Oseledets.Krieger.nonTop_covered {N : ℕ} (hN : 1 ≤ N) {j k : ℕ} (_hjk : j ≤ k) (hnotTop : j < (k + 1) / N * N) : ∃ (m : ℕ), (m + 1) * N ≤ k + 1 ∧ ∃ i < N, j = m * N + i

Combinatorial heart (pure ℕ): if a floor height j ≤ k is NOT a top floor (i.e. j < ⌊(k+1)/N⌋·N), then it lies in a complete block: there is m with (m+1)·N ≤ k+1 and j = m·N + (j mod N), j mod N < N.

theorem Oseledets.Krieger.topBlock_count {N : ℕ} (_hN : 1 ≤ N) (k : ℕ) : k + 1 - (k + 1) / N * N = (k + 1) % N

The floor count of the top incomplete block of column k+1: the number of integers j with ⌊(k+1)/N⌋·N ≤ j ≤ k is exactly (k+1) mod N.

theorem Oseledets.Krieger.residual_lt_eps {N : ℕ} (hN : 1 ≤ N) {ε : ℝ} (hε : 0 < ε) (x : ℕ → ENNReal) {μA : ENNReal} (hsum : ∑' (k : ℕ), x k = μA) (hμA : μA < ENNReal.ofReal (ε / ↑N)) {S : ENNReal} (hS : S ≤ ∑' (k : ℕ), ↑((k + 1) % N) * x k) : S < ENNReal.ofReal ε

The residual < ε inequality, assembled at the ℝ≥0∞ level: if ∑ x_k = μA, μA < ofReal(ε/N), and S ≤ ∑ ((k+1) mod N) · x_k, then S < ofReal ε.

theorem Oseledets.Krieger.floor_subset_coveredSet {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) {N : ℕ} (hN : 1 ≤ N) {j k : ℕ} (hjk : j ≤ k) (hnotTop : j < (k + 1) / N * N) : (⇑e)^[j] '' returnLevel e A (k + 1) ⊆ coveredSet e A N

A skyscraper floor (j, k) with j < ⌊(k+1)/N⌋·N lies in the covered set: j = m·N + i is a complete-block floor (nonTop_covered).

theorem Oseledets.Krieger.compl_inter_skyscraper_subset_topFloors {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) {N : ℕ} (hN : 1 ≤ N) : (coveredSet e A N)ᶜ ∩ skyscraper e A ⊆ topFloors e A N

The residual structure: (coveredSet)ᶜ ∩ skyscraper ⊆ topFloors. A skyscraper point sits at some floor (j, k), j ≤ k; if it is not covered then j ≥ ⌊(k+1)/N⌋·N (else floor_subset_coveredSet), so it is a top floor.

The residual measure bound

theorem Oseledets.Krieger.topFloors_eq_biUnion {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) (N : ℕ) : topFloors e A N = ⋃ (k : ℕ), ⋃ j ∈ Finset.Icc ((k + 1) / N * N) k, (⇑e)^[j] '' returnLevel e A (k + 1)

topFloors rewritten with a Finset.Icc bUnion over the column floors.

theorem Oseledets.Krieger.measure_topFloors_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (e : α ≃ᵐ α) (he : MeasureTheory.MeasurePreserving (⇑e) μ μ) {A : Set α} (hA : MeasurableSet A) {N : ℕ} (hN : 1 ≤ N) : μ (topFloors e A N) ≤ ∑' (k : ℕ), ↑((k + 1) % N) * μ (returnLevel e A (k + 1))

The residual measure bound: μ (topFloors e A N) ≤ ∑ k, ((k+1) mod N) · μ (returnLevel e A (k+1)). Countable + finite subadditivity, measure_iterate_image to normalize each floor measure, then the floor count topBlock_count.