OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanFixedPolarTargets.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed target measure and trace on a transformed polar cone

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.MeasuredCone.exists_fixed_polar_target_regions line 32

    Source documentation

    Normalize only the target quotient Haar measure. The published action, its exact trace, and every later path region use this same fixed product measure on the nilpotent factor.

    theorem MeasuredCone.exists_fixed_polar_target_regions
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput