Lax approximation theorem

AbbreviationTorus#✓fully proved

For a natural number \(d\), the \(d\)-dimensional torus is \(\mathbb{T}^d = (\mathbb{R}/\mathbb{Z})^d\), the product of \(d\) copies of the circle \(\mathbb{R}/\mathbb{Z}\).

abbrev Torus (d : ℕ) : Type := Fin d → AddCircle (1 : ℝ)

Used by 6

Used byGrid cube in the torus · Essential-supremum distance between volume-preserving maps · Cyclic cube exchange · Toral dynamical systems as volume-preserving transformations · Toral dynamical system · Volume-preserving transformations of the torus

StructureVolume-preserving transformations of the torus#✓fully proved

Let \(d\) be a natural number. A volume-preserving transformation of the torus \(\mathbb{T}^d = (\mathbb{R}/\mathbb{Z})^d\) is a bijection \(T\) of \(\mathbb{T}^d\) such that \(T\) and \(T^{-1}\) are measurable and \(T\) preserves the volume measure.

structure VolumePreservingEquiv (d : ℕ) where
  toMeasurableEquiv : Torus d ≃ᵐ Torus d
  measurePreserving :
    MeasurePreserving toMeasurableEquiv (volume : Measure (Torus d)) volume

Uses 1 · Used by 4

Statement usesTorus

Used byEssential-supremum distance between volume-preserving maps · Cyclic cube exchange · Lax's approximation theorem · Toral dynamical systems as volume-preserving transformations

DefinitionEssential-supremum distance between volume-preserving maps#✓fully proved

Let \(d\) be a natural number and let \(T\) and \(S\) be measurable, invertible, volume-preserving transformations of the torus \(\mathbb{T}^d = (\mathbb{R}/\mathbb{Z})^d\). Let \(\rho\) be the distance on \(\mathbb{T}^d\) given by the maximum over the coordinates of the distance on the circle \(\mathbb{R}/\mathbb{Z}\) (taken to be \(0\) when \(d = 0\)). The distance \(\delta(T, S) \in [0, \infty]\) is the essential supremum, with respect to the volume measure, of the function \(x \mapsto \rho(T x, S x)\).

This is Knill's metric \(\delta\).

noncomputable def deltaDist {d : ℕ} (T S : VolumePreservingEquiv d) : ℝ≥0∞ :=
  essSup (fun x => edist (T.toMeasurableEquiv x) (S.toMeasurableEquiv x)) (volume : Measure (Torus d))

Uses 2 · Used by 1

Statement usesTorus · Volume-preserving transformations of the torus

Used byLax's approximation theorem

StructureToral dynamical system#✓fully proved

Let \(d\) be a natural number. A toral dynamical system on the torus \(\mathbb{T}^d = (\mathbb{R}/\mathbb{Z})^d\) is a homeomorphism of \(\mathbb{T}^d\) that preserves the volume measure.

structure ToralDynamicalSystem (d : ℕ) where
  toHomeomorph : Torus d ≃ₜ Torus d
  measurePreserving :
    MeasurePreserving toHomeomorph (volume : Measure (Torus d)) volume

Uses 1 · Used by 2

Statement usesTorus

Used byLax's approximation theorem · Toral dynamical systems as volume-preserving transformations

DefinitionToral dynamical systems as volume-preserving transformations#✓fully proved

Let \(d\) be a natural number. A volume-preserving homeomorphism \(T\) of the torus \(\mathbb{T}^d = (\mathbb{R}/\mathbb{Z})^d\) is regarded as a measurable, invertible, volume-preserving transformation of \(\mathbb{T}^d\): the same map, with its inverse, viewed as a measurable equivalence.

noncomputable def ToralDynamicalSystem.toVolumePreservingEquiv {d : ℕ}
    (T : ToralDynamicalSystem d) : VolumePreservingEquiv d where
  toMeasurableEquiv := T.toHomeomorph.toMeasurableEquiv
  measurePreserving := T.measurePreserving

Uses 3 · Used by 1

Statement usesToral dynamical system · Torus · Volume-preserving transformations of the torus

Used byLax's approximation theorem

DefinitionGrid cube in the torus#✓fully proved

Let \(n\) and \(d\) be natural numbers and let \(k = (k_0, \dots, k_{d-1})\) with each \(k_i \in \{0, \dots, n-1\}\). The grid cube with index \(k\) is the set of points \(x\) of the torus \(\mathbb{T}^d = (\mathbb{R}/\mathbb{Z})^d\) such that, for every \(i < d\), the coordinate \(x_i\) is the class modulo \(1\) of some real number \(r\) with \(k_i/n \le r < (k_i + 1)/n\).

def cube (n : ℕ) {d : ℕ} (k : Fin d → Fin n) : Set (Torus d) :=
  { x | ∀ i, ∃ r : ℝ, (k i : ℝ) / n ≤ r ∧ r < ((k i : ℝ) + 1) / n ∧
        x i = ((r : ℝ) : AddCircle (1 : ℝ)) }

Uses 1 · Used by 1

Statement usesTorus

Used byCyclic cube exchange

DefinitionCoordinate shift between grid cubes#✓fully proved

Let \(n\) and \(d\) be natural numbers, let \(\sigma\) be a permutation of the index set \(\{0, \dots, n-1\}^d\), let \(k\) be an index and let \(i < d\). The shift along axis \(i\) determined by \(\sigma\) and \(k\) is the point \((\sigma(k)_i - k_i)/n\) of the circle \(\mathbb{R}/\mathbb{Z}\), that is, the class modulo \(1\) of this real number.

For an index \(j\), the grid cube with index \(j\) is the set of points of the torus \((\mathbb{R}/\mathbb{Z})^d\) whose \(m\)-th coordinate is the class of a real number in \([j_m/n, (j_m + 1)/n)\) for every \(m < d\). For \(n > 0\), translating the \(m\)-th coordinate of each point of the grid cube with index \(k\) by the shift along axis \(m\), for every \(m < d\), carries that cube onto the grid cube with index \(\sigma(k)\).

noncomputable def cubeShift (n : ℕ) {d : ℕ}
    (σ : Equiv.Perm (Fin d → Fin n))
    (k : Fin d → Fin n) (i : Fin d) : AddCircle (1 : ℝ) :=
  ((((((σ k) i : ℤ) - (k i : ℤ) : ℝ) / (n : ℝ)) : ℝ) : AddCircle (1 : ℝ))

Used by 1

Used byCyclic cube exchange

DefinitionCyclic cube exchange#✓fully proved

Let \(n\) and \(d\) be natural numbers. For an index \(k \in \{0, \dots, n-1\}^d\), the grid cube with index \(k\) is the set of points of the torus \(\mathbb{T}^d = (\mathbb{R}/\mathbb{Z})^d\) whose \(i\)-th coordinate is the class of a real number in \([k_i/n, (k_i + 1)/n)\) for every \(i < d\). A measurable, invertible, volume-preserving transformation \(T\) of \(\mathbb{T}^d\) is a cyclic cube exchange with \(n\) subdivisions if \(n > 0\) and there is a permutation \(\sigma\) of \(\{0, \dots, n-1\}^d\) that is a single cycle moving every index, such that for every index \(k\), every point \(x\) of the grid cube with index \(k\) and every \(i < d\), we have \((T x)_i = x_i + (\sigma(k)_i - k_i)/n\) in \(\mathbb{R}/\mathbb{Z}\). Thus \(T\) translates each grid cube \(k\) rigidly onto the grid cube \(\sigma(k)\).

def IsCyclicCubeExchange {d : ℕ} (T : VolumePreservingEquiv d) (n : ℕ) : Prop :=
  0 < n ∧ ∃ σ : Equiv.Perm (Fin d → Fin n),
    σ.IsCycle ∧ σ.support = Finset.univ ∧
    ∀ k : Fin d → Fin n, ∀ x ∈ cube n k, ∀ i,
      T.toMeasurableEquiv x i = x i + cubeShift n σ k i

Uses 4 · Used by 1

Statement usesTorus · Volume-preserving transformations of the torus · Grid cube in the torus · Coordinate shift between grid cubes

Used byLax's approximation theorem

TheoremLax's approximation theorem#●ready to prove

Let \(d \ge 1\) be a natural number and let \(T\) be a toral dynamical system on the torus \(\mathbb{T}^d = (\mathbb{R}/\mathbb{Z})^d\), regarded as a measurable, invertible, volume-preserving transformation of \(\mathbb{T}^d\). Then for every \(\varepsilon \in (0, \infty]\) there are a natural number \(n\) and a measurable, invertible, volume-preserving transformation \(S\) of \(\mathbb{T}^d\) such that \(S\) is a cyclic cube exchange with \(n\) subdivisions and \(\delta(T, S) < \varepsilon\), where \(\delta\) is the essential-supremum distance between volume-preserving maps.

public theorem_wanted lax_approximation {d : ℕ} (hd : 0 < d) (T : ToralDynamicalSystem d)
    {ε : ℝ≥0∞} (hε : 0 < ε) :
    ∃ (n : ℕ) (S : VolumePreservingEquiv d),
      IsCyclicCubeExchange S n ∧ deltaDist T.toVolumePreservingEquiv S < ε

Sources

• P. D. Lax, Approximation of measure preserving transformations, Comm. Pure Appl. Math. 24 (1971). Knill, Some fundamental theorems in mathematics, §110. Problem lax_approximation of the lean-eval benchmark.

Uses 5

Statement usesCyclic cube exchange · Toral dynamical system · Toral dynamical systems as volume-preserving transformations · Volume-preserving transformations of the torus · Essential-supremum distance between volume-preserving maps

8 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.