OAI.StandardMapEntropy.main_entropy

The theorem states that the defined proposition MainObligation holds. Unfolded, it says there is a real k₀>0 such that for every real k≥k₀ the metric entropy of the standard map with parameter k with respect to area measure is strictly positive. Here the torus is the product of two copies of the circle ℝ/ℤ, and area is the product of the Lebesgue (Haar) measures on the two circles. The standard map sends (x,y) to (x+y+k sin(2πx), y+k sin(2πx)), with the circle coordinates added modulo 1. For a measurable map p from the torus to Fin(r+1), a finite partition into r+1 labelled pieces, the block atom of a word w of length n is the set of points z whose i-th iterate under the map has label w(i) for every i<n. The block entropy is −Σ_w μ(atom) log μ(atom) over all words, using real-valued measures. The partition entropy is the infimum over n≥0 of the ENNReal-valued number ofReal(blockEntropy for n+1 blocks divided by (n+1)). The metric entropy is the supremum over r and over all such partitions of the partition entropy. The source does not state an invariance or ergodicity hypothesis in the definition.