# Rokhlin’s multiple-mixing problem

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

- [Rokhlin's multiple-mixing problem for one transformation](../../preprints/Rokhlins-multiple-mixing-problem-for-one-transformation-September-23-2026/paper.pdf)

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

| Result | Comparator statement |
| --- | --- |
| Mixing of every finite order for one mixing transformation | [Rokhlin.lean](../ComparatorChallenges/Rokhlin.lean) |