From 8279389513d0da676072ebcffe3639c042f80955 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 24 May 2026 07:52:44 +0000 Subject: [PATCH] =?UTF-8?q?feat:=20add=20Ornstein=E2=80=93Weiss=20?= =?UTF-8?q?=E2=84=A4=E1=B5=88=20Rokhlin=20eval=20problem?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit §109 of Knill's "Some Fundamental Theorems in Mathematics" (additional statement; the boxed main theorem is the classical Rokhlin lemma). The multidimensional generalization (Ornstein–Weiss, 1987): for every free measure-preserving ℤᵈ-action T on a standard Borel probability space, every box size N ≥ 1, and every ε > 0, there is a measurable base B such that the translates T v '' B for v ∈ [0, N)ᵈ are pairwise disjoint with measure ≥ 1 - ε. Mathlib has the supporting measure theory and Finset / box machinery but no multidimensional Rokhlin lemma and no free measure-preserving ℤᵈ-actions. Co-Authored-By: Claude Opus 4.7 --- LeanEval/Dynamics/OrnsteinWeiss.lean | 74 +++++++++++++++++++ .../problems/ornstein_weiss_rokhlin.toml | 9 +++ 2 files changed, 83 insertions(+) create mode 100644 LeanEval/Dynamics/OrnsteinWeiss.lean create mode 100644 manifests/problems/ornstein_weiss_rokhlin.toml diff --git a/LeanEval/Dynamics/OrnsteinWeiss.lean b/LeanEval/Dynamics/OrnsteinWeiss.lean new file mode 100644 index 0000000..ece4aee --- /dev/null +++ b/LeanEval/Dynamics/OrnsteinWeiss.lean @@ -0,0 +1,74 @@ +import Mathlib +import EvalTools.Markers + +namespace LeanEval +namespace Dynamics + +/-! +# Ornstein–Weiss `ℤᵈ` Rokhlin lemma (Ornstein–Weiss, 1987) + +§109 of Knill's *Some Fundamental Theorems in Mathematics* (additional +statement). The multidimensional Rokhlin lemma: for every free +measure-preserving `ℤᵈ`-action `T` on a standard Borel probability +space, every box size `N ≥ 1`, and every `ε > 0`, there is a measurable +base `B` such that the translates `T v '' B` for `v ∈ [0, N)ᵈ` are +pairwise disjoint and their union has measure at least `1 − ε`. + +Mathlib has `MeasurePreserving`, `IsProbabilityMeasure`, +`Set.PairwiseDisjoint`, `Fintype.piFinset`, `Finset.Ico`, and +`StandardBorelSpace`, but **no Ornstein–Weiss lemma**, no free +measure-preserving `ℤᵈ`-actions, no multidimensional Rokhlin towers. +The Challenge ships two small helper definitions (`IsFreeAction` and +`boxShape`). + +Three hypotheses beyond the classical Rokhlin lemma: + +* `1 ≤ d` rules out the degenerate `d = 0` case. +* The identity axiom `T 0 = id` is imposed explicitly; the homomorphism + axiom alone only forces `T 0` to be idempotent. Together with the + homomorphism axiom this also gives bijectivity of each `T v` via + `T (-v) ∘ T v = T 0 = id`. +* `[StandardBorelSpace Ω]` rules out the countable-cocountable + σ-algebra defect (see the §109 Rokhlin lemma PR for the + one-dimensional version of this counterexample). +-/ + +open MeasureTheory Set + +/-- A `ℤᵈ`-action by measure-preserving maps is **free** (in the +Ornstein–Weiss sense) if, for every nonzero translation `v`, the set +of points fixed by `T v` has measure zero. -/ +def IsFreeAction {Ω : Type*} [MeasurableSpace Ω] {d : ℕ} + (μ : Measure Ω) (T : (Fin d → ℤ) → Ω → Ω) : Prop := + ∀ v : Fin d → ℤ, v ≠ 0 → μ {x | T v x = x} = 0 + +/-- The integer box `[0, N)ᵈ` as a `Finset` of `ℤᵈ` translations. -/ +noncomputable def boxShape (d N : ℕ) : Finset (Fin d → ℤ) := + Fintype.piFinset (fun _ : Fin d => Finset.Ico (0 : ℤ) (N : ℤ)) + +/-- **Ornstein–Weiss `ℤᵈ` Rokhlin lemma.** For every free +measure-preserving `ℤᵈ`-action `T` on a standard Borel probability +space (with `d ≥ 1`, identity axiom `T 0 = id`, and the homomorphism +axiom), every box size `N ≥ 1`, and every `ε > 0`, there is a +measurable base `B` such that the translates `T v '' B` for +`v ∈ [0, N)ᵈ` are pairwise disjoint and their union has measure at +least `1 − ε`. -/ +@[eval_problem] +theorem ornstein_weiss_rokhlin {Ω : Type*} [MeasurableSpace Ω] + [StandardBorelSpace Ω] + {d : ℕ} (_hd : 1 ≤ d) (μ : Measure Ω) [IsProbabilityMeasure μ] + (T : (Fin d → ℤ) → Ω → Ω) + (_hid : ∀ x, T 0 x = x) + (_hT : ∀ v, MeasurePreserving (T v) μ μ) + (_hgrp : ∀ u v x, T (u + v) x = T u (T v x)) + (_hfree : IsFreeAction μ T) + (N : ℕ) (_hN : 1 ≤ N) {ε : ENNReal} (_hε : 0 < ε) : + ∃ B : Set Ω, + MeasurableSet B ∧ + ((boxShape d N : Finset (Fin d → ℤ)) : Set (Fin d → ℤ)).PairwiseDisjoint + (fun v => T v '' B) ∧ + μ (⋃ v ∈ boxShape d N, T v '' B) ≥ 1 - ε := by + sorry + +end Dynamics +end LeanEval diff --git a/manifests/problems/ornstein_weiss_rokhlin.toml b/manifests/problems/ornstein_weiss_rokhlin.toml new file mode 100644 index 0000000..ec1e6d6 --- /dev/null +++ b/manifests/problems/ornstein_weiss_rokhlin.toml @@ -0,0 +1,9 @@ +id = "ornstein_weiss_rokhlin" +title = "Ornstein–Weiss ℤᵈ Rokhlin lemma" +test = false +module = "LeanEval.Dynamics.OrnsteinWeiss" +holes = ["ornstein_weiss_rokhlin"] +submitter = "Kim Morrison" +notes = "§109 of Knill's 'Some Fundamental Theorems in Mathematics' (additional statement; the boxed main theorem is the classical Rokhlin lemma). The multidimensional generalization: for every free measure-preserving ℤᵈ-action T on a standard Borel probability space, every box size N ≥ 1, and every ε > 0, there is a measurable base B such that the translates T v '' B for v ∈ [0, N)ᵈ are pairwise disjoint with measure ≥ 1 - ε. Three hypotheses beyond the classical lemma: 1 ≤ d (rules out d = 0 degeneracy); the identity axiom T 0 = id (homomorphism alone only forces T 0 idempotent); [StandardBorelSpace Ω] (rules out the countable-cocountable σ-algebra defect). Mathlib has MeasurePreserving, IsProbabilityMeasure, Set.PairwiseDisjoint, Fintype.piFinset, Finset.Ico, StandardBorelSpace, but no Ornstein–Weiss lemma, no free measure-preserving ℤᵈ-actions, no multidimensional Rokhlin towers. The Challenge ships two small helper defs (IsFreeAction, boxShape)." +source = "D. S. Ornstein and B. Weiss, *Entropy and isomorphism theorems for actions of amenable groups*, J. Anal. Math. 48 (1987), 1-141 — Theorem 5.2 establishes the multidimensional (and amenable-group) Rokhlin lemma. Listed as §109 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). No formalization found in any major prover." +informal_solution = "Standard proof reduces to the one-dimensional Rokhlin lemma by induction on d using the quasi-tiling lemma of Ornstein–Weiss: every Følner set in ℤᵈ can be ε-quasi-tiled by finitely many translates of cubes [0, N)ᵈ, so a one-dimensional skyscraper over a transversal of one direction can be folded into a d-dimensional Rokhlin tower with arbitrarily small remainder."