# Banach’s simple Lebesgue-spectrum problem

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

- [A smooth three-torus diffeomorphism with simple Lebesgue spectrum](../../preprints/A-smooth-three-torus-diffeomorphism-with-simple-Lebesgue-spectrum-September-23-2026/paper.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| Smooth simple Lebesgue spectrum on the three-torus | [ThreeTorus.lean](../ComparatorChallenges/ThreeTorus.lean) |