OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCanonicalPolarSamplers.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Counted source samplers using the canonical continuous Cartan dilation

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.MeasuredCone.exists_canonical_polar_samplers line 33

    Source documentation

    The measured source cone determines all group maps and the continuous dilation. Only the original amplitude bound and the published exponential inputs are needed to obtain the counted sampler and its exact conjugation law. Its section is chosen before the scale and neighboring sequence.

    theorem MeasuredCone.exists_canonical_polar_samplers
    (D : M.MeasuredCone F C)
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput