∑math20

Dynamical systems and ergodic theory · Result 144

Banach’s simple Lebesgue-spectrum problem

1 paperLean

Resolves the probability-preserving form of Banach's simple Lebesgue-spectrum problem within smooth dynamics. A smooth volume-preserving diffeomorphism of the standard-volume three-torus has simple Lebesgue spectrum on its entire complex mean-zero L2 space: the bilateral iterates of one real observable form an orthonormal basis of that space.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of A smooth three-torus diffeomorphism with simple Lebesgue spectrum

A smooth three-torus diffeomorphism with simple Lebesgue spectrum

OpenAI · September 23, 2026

We solve the probability-preserving form of Banach's simple Lebesgue-spectrum problem in smooth dynamics. We construct a C∞ diffeomorphism of the three-torus that preserves standard volume and whose Koopman operator has simple Lebesgue spectrum on the entire mean-zero L2 space.

Read PDF Download Source

Cite
@misc{OAI:A-smooth-three-torus-diffeomorphism-with-simple-Lebesgue-spectrum-September-23-2026,
  author = {{OpenAI}},
  title = {{A smooth three-torus diffeomorphism with simple Lebesgue spectrum}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-smooth-three-torus-diffeomorphism-with-simple-Lebesgue-spectrum-September-23-2026/paper.pdf}{OAI:A-smooth-three-torus-diffeomorphism-with-simple-Lebesgue-spectrum-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

Banach's simple Lebesgue-spectrum problem asks for a probability-preserving transformation with simple Lebesgue spectrum on its mean-zero \(L^2\) space. The formalization constructs a smooth volume-preserving diffeomorphism of the three-torus with this property. It gives a real-valued cyclic vector whose integer iterates form an orthonormal basis of the entire mean-zero space, and an isometric identification under which the Koopman operator becomes multiplication by the coordinate function on the circle. The transformation is also ergodic.

Comparator links

ResultComparator statement
Smooth simple Lebesgue spectrum on the three-torusThreeTorus.lean

Scope note on GitHub →