CartanUniformCompactProbeBridge.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform constants for compact source bridges

The compact section, normalized generator and pivot cancellation are combined before using the metric estimate. The constants are independent of the small parameter and of every ideal probe and starting sheet.

theorem OAI.PolycyclicRecognition.exists_uniform_compact_source_probe_bridge_bound line 32
Source documentation
The metric constants are selected before the compact section, scale and subexponential radii. Those data affect only the eventual scale threshold. This order permits choosing the source displacement after a fixed target restriction tolerance, uniformly across the original neighboring cells.
```
theorem exists_uniform_compact_source_probe_bridge_bound
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput