Prove Rokhlin (openai/math family 145: Rokhlin's multiple-mixing problem) in Lean 4 with Mathlib; graded by…
Prove Rokhlin (openai/math family 145: Rokhlin's multiple-mixing problem) in Lean 4 with Mathlib; graded by…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 145 of the release, Rokhlin's multiple-mixing problem (Dynamical systems and…
The task
Context: this statement belongs to family 145 of the release, *Rokhlin's multiple-mixing problem* (Dynamical systems and ergodic theory). The family as a whole: Proves that every invertible mixing probability-preserving transformation is mixing of all finite orders, resolving Rokhlin's multiple-mixing problem for a…
Part of raising-heart/openai-math.