PolynomialChartCoordinates.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Polynomial logarithm bounds for the actual scaled coordinate charts

theorem OAI.PolycyclicRecognition.bracketWordExponent_one line 16
Source documentation
Unit letter weights give the ordinary bracket length.
```
theorem bracketWordExponent_one {I : Type*} [Fintype I] [DecidableEq I]
    (w : FreeMagma I) : bracketWordExponent (fun _ => 1) w = bracketWordLength w := by
…
```
Mentions: OAI.PolycyclicRecognition.bracketWordExponent, OAI.PolycyclicRecognition.bracketWordLength

theorem OAI.PolycyclicRecognition.norm_polynomial_chart_log_le line 28

Source documentation

Integer coordinate weights make the logarithm of every bounded chart point polynomially bounded in the actual scale, in any fixed reference basis. This estimate does not assume a limiting group or metric.

theorem norm_polynomial_chart_log_le
    {L J K : Type*} [LieRing L] [LieAlgebra ℝ L] [Fintype J] [Fintype K]
    (b : Basis J ℝ L) (b₀ : Basis K ℝ L) (cost : J → ℕ)
    (p : ℕ) (hp : ∀ j, cost j ≤ p)
    {r : ℝ} (hr : 1 ≤ r) (z : J → ℝ) :
    ‖b₀.equivFun ((exponentialRescaleBasis b (fun j => (cost j : ℝ)) (Real.log r)).equivFun.symm z)‖ ≤
      (∑ j, ‖b₀.equivFun (b j)‖) * ‖z‖ * (1 + r) ^ p := by
…

Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis