OAI.StandardMapEntropy.main_components
ProvedThe 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.
-- 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
theorem main_components : MainComponentsObligation := by sorry end StandardMapEntropy end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.