CartanStationaryTemplateComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual stationary template-volume comparison

The lower count uses independently sampled coordinates of the actual root factor. The upper count uses the image paths in the ambient group. No volume-comparison statement is assumed as an input.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_template_exponent_le_of_stationary_mean line 50
Source documentation
Stationary averaging and actual path packing bound the exponent of the box supported by any prescribed finite family of Cartan directions.
```
theorem exists_template_exponent_le_of_stationary_mean
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput