OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanMetricBasepointSampling.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual dominated sampling at a nearby basepoint

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_metric_basepoint_dominated_sampling line 42

    Source documentation

    A nearby center admits a changed sampling law dominated by independent ordinary-cell and allowed-suffix sampling. The domination constant is exact and independent of the map, centers and scale.

    theorem exists_metric_basepoint_dominated_sampling
    (hExp : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput