OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanStationaryIncrement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Stationary increments through the actual ergodic decomposition

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.increments_tendsto_labels_of_invariant_probability line 47

    Source documentation

    Along each actual Cartan exponential ray, normalized increments approach the finite canonical label set for every fixed invariant probability. The integrand uses the whole finite label set, so no measurable choice of component labels is needed.

    theorem increments_tendsto_labels_of_invariant_probability
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput