OAI/NumberTheory/DukePrimeDegree/Dynamics/InvariantRootExistence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positive entropy yields an invariant root without the numerical entropy formula

  1. theorem OAI.DukePrimeDegree.exists_invariant_root_of_positive_regular_entropy line 17

    Source documentation

    Commutators, isolated-root shearing, a source ordering, and the zero-entropy criterion suffice for existence of one invariant root. No numerical entropy identity or homogeneous-orbit hypothesis is used.

    theorem exists_invariant_root_of_positive_regular_entropy
    (d : ℕ) (hd : 2 < d+1)
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ]
    (hpos : 0 < measureEntropy μ (fun x => rightAction x
      (diagonalOneParameter (regularDiagonalWeights d) (regularDiagonalWeights_sum d) 1))) :
    ∃ (i j : Fin (d+1)) (hij : i ≠ j), ∀ t : ℝ,
      μ.map (fun x => rightAction x (Matrix.SpecialLinearGroup.transvection hij t))=μ := by
…