OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanFactorHaarInvariance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual Cartan factor action preserves the chosen Haar measure

  1. theorem OAI.PolycyclicRecognition.CartanFactorModel.action_preserves_haar line 29

    Source documentation

    Trace zero and the published realization imply that the original factor action preserves every Haar normalization, including the measure constructed in ideal/quotient section coordinates.

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

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput

  2. theorem OAI.PolycyclicRecognition.CartanFactorModel.exists_probe_source_packing_constant line 59

    Source documentation

    The actual Lie-model action supplies the invariance needed by the fixed-pivot source count. No action or fixed-slice volume assumption remains.

    theorem exists_probe_source_packing_constant
    [IsIsometricSMul G G] [ProperSpace G]
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput