CartanNMetric.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Linear ambient length of the exponentially large root-ideal boxes

theorem OAI.PolycyclicRecognition.log_two_add_exp_le line 20
Source documentation
An exponential factor inside a logarithm contributes at most its exponent, uniformly for nonnegative scales.
```
theorem log_two_add_exp_le {A S r : ℝ} (hA : 0 ≤ A) (hS : 0 ≤ S) (hr : 0 ≤ r) :
    Real.log (2 + A * Real.exp (r * S)) ≤ Real.log (2 + A) + r * S := by
…
```
theorem OAI.PolycyclicRecognition.root_generators_linear_metric_bound line 39
Source documentation
Each exponentially rescaled root generator has ambient length linear in the logarithmic scale, uniformly over a bounded range of weights.
```
theorem root_generators_linear_metric_bound
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput
theorem OAI.PolycyclicRecognition.exists_cartan_n_chart_metric_bound line 89
Source documentation
Bounded normalized root-ideal coordinates give linear ambient length. This is the anchor bound for chart profiles, even though the nilpotent coordinates themselves grow exponentially.
```
theorem exists_cartan_n_chart_metric_bound
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput
theorem OAI.PolycyclicRecognition.exists_cartan_n_expanded_metric_bound line 127
Source documentation
The same linear bound allows subexponential enlargement of the box radius. Only the fixed positive lower word cost is needed.
```
theorem exists_cartan_n_expanded_metric_bound
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput