Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

OAI.StandardMapEntropy.main_components

Proved

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states that there is a threshold k₀>0 such that for every real k≥k₀ the standard map has a hyperbolic Bernoulli component. The standard map on the torus (ℝ/ℤ)² sends (x,y) to (x+y+k sin(2πx), y+k sin(2πx)), and area is the product of the Lebesgue measures on the two circle factors. Its derivative at (x,y) is the linear map on ℂ≅ℝ² obtained by conjugating the step (a+ib) ↦ (v a−b)+ia with v=2+2πk cos(2πx) by the linear coordinate change a+ib ↦ a+i(a−b); products of these derivatives along orbits give the derivative cocycle. A vector v≠0 has growth rate l if (1/n) log‖(derivative product over n steps)(v)‖ tends to l. The Lyapunov spectrum at a point is l with l≥0 such that either l=0 and every nonzero vector has growth rate 0, or l>0 and there is a nonzero direction s for which vectors parallel to s (zero wedge product with s) have growth rate −l and all other nonzero vectors have growth rate l. A hyperbolic Bernoulli component for k is a measurable set E of positive area, invariant mod null sets (its preimage under the map equals E almost everywhere), such that the map is ergodic for the area measure restricted to E and normalized to a probability measure, and almost every point of E has some l>0 giving its Lyapunov spectrum. Moreover, there is a positive integer N and measurable sets P₀,…,P_{N−1} whose union equals E almost everywhere, with pairwise null overlaps, each having positive area equal to area(E)/N, and the map carries each Pⱼ onto P_{(j+1) mod N} up to null sets. Finally, the N-th iterate of the map on each Pⱼ, with normalized area, is Bernoulli: there is a probability measure β on ℝ and almost-everywhere inverse measure-preserving encode and decode maps between Pⱼ and the product measure β^ℤ on ℤ-indexed real sequences, with encode of the image of z equal to the sequence shifted by one index.

Preamble
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/StandardMapComponents.lean; bytes 4687..4751
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_StandardMapComponents

namespace OAI

open MeasureTheory Set Filter

open scoped ENNReal Topology

namespace StandardMapEntropy

attribute [local instance] _root_.OAI.StandardMapEntropy.realTangentCompTriple

Formal statement
theorem main_components : MainComponentsObligation := by
  sorry

end StandardMapEntropy
end OAI
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/StandardMapComponents.lean
Human review
  • Endorsed by Community (Bot) · Oct 7, 2026

    Confirmed by the moderator at approval.

  • Endorsed by marwahaha · Oct 7, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me