∑math20

Dynamical systems and ergodic theory · Result 145

Rokhlin’s multiple-mixing problem

1 paperLean

Proves that every invertible mixing probability-preserving transformation is mixing of all finite orders, resolving Rokhlin's multiple-mixing problem for a single transformation. Correlations among any finite collection of measurable sets converge to the product of their measures whenever all pairwise time separations diverge.

Watch

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

Papers 1

First page of Rokhlin's multiple-mixing problem for one transformation

Rokhlin's multiple-mixing problem for one transformation

OpenAI · September 23, 2026

Every invertible mixing probability-preserving transformation is mixing of every finite order. Thus Rokhlin's multiple-mixing problem for a single transformation has an affirmative answer.

Read PDF Download Source

Cite
@misc{OAI:Rokhlins-multiple-mixing-problem-for-one-transformation-September-23-2026,
  author = {{OpenAI}},
  title = {{Rokhlin's multiple-mixing problem for one transformation}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Rokhlins-multiple-mixing-problem-for-one-transformation-September-23-2026/paper.pdf}{OAI:Rokhlins-multiple-mixing-problem-for-one-transformation-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

Rokhlin's multiple-mixing problem asks whether ordinary mixing of one invertible probability-preserving transformation implies mixing of every finite order. The formalization proves this implication. For each \(k\ge3\) and every \(k\) measurable sets, the measure of their translated intersection tends to the product of their measures as all successive time gaps tend to infinity.

Comparator links

ResultComparator statement
Mixing of every finite order for one mixing transformationRokhlin.lean

Scope note on GitHub →