OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanPairMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual averaged slope kills the Cartan root factor

This applies the metric estimate for normalized pairs and the root-flow argument to the very homomorphism used by the stationary L² theorem.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.normalizedPairMeanSlope_kills_root_factor line 37

    Source documentation

    No geometric factorization is assumed for the averaged slope. Its vanishing on the entire actual root factor follows from distortion.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput