TriangularWordBounds.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Polynomial coordinate bounds for bounded-height triangular words

We use the actual prefix diagonals of a word in positive triangular matrices. Every normalized increment is unipotent. Thus bounded heights at every prefix, with bounded step matrices, imply a polynomial endpoint bound. No endpoint-only height assumption is substituted for the path condition.

def OAI.PolycyclicRecognition.PositiveTriangular.framedSteps line 21
Source documentation
The increments seen in the diagonal frame at each prefix.
```
noncomputable def framedSteps (g : positiveTriangular n) :
    List (positiveTriangular n) → List (Matrix (Fin n) (Fin n) ℝ)
  | [] => []
  | a :: l => ((frame g : Matrix (Fin n) (Fin n) ℝ) * matrix a *
      (↑(frame (g * a))⁻¹ : Matrix (Fin n) (Fin n) ℝ)) :: framedSteps (g * a) l
```
Mentions: OAI.PolycyclicRecognition.positiveTriangular, OAI.PolycyclicRecognition.PositiveTriangular.frame, OAI.PolycyclicRecognition.PositiveTriangular.matrix
theorem OAI.PolycyclicRecognition.PositiveTriangular.framedSteps_length line 27
theorem OAI.PolycyclicRecognition.PositiveTriangular.framedSteps_prod line 34
Source documentation
Prefix frames cancel without any commutativity of the step matrices.
```
theorem framedSteps_prod (g : positiveTriangular n) (l : List (positiveTriangular n)) :
    (framedSteps g l).prod = (frame g : Matrix (Fin n) (Fin n) ℝ) *
      (l.map matrix).prod * (↑(frame (g * l.prod))⁻¹ : Matrix (Fin n) (Fin n) ℝ) := by
…
```
Mentions: OAI.PolycyclicRecognition.positiveTriangular, OAI.PolycyclicRecognition.PositiveTriangular.framedSteps, OAI.PolycyclicRecognition.PositiveTriangular.frame, OAI.PolycyclicRecognition.PositiveTriangular.matrix
theorem OAI.PolycyclicRecognition.PositiveTriangular.framedSteps_strict line 44
Source documentation
For the actual prefix diagonal, the normalized step has diagonal one.
```
theorem framedSteps_strict (g : positiveTriangular n) (l : List (positiveTriangular n)) :
    ∀ a ∈ framedSteps g l, StrictUpper (a - 1) := by
…
```
Mentions: OAI.PolycyclicRecognition.positiveTriangular, OAI.PolycyclicRecognition.PositiveTriangular.framedSteps, OAI.PolycyclicRecognition.StrictUpper
theorem OAI.PolycyclicRecognition.PositiveTriangular.framedSteps_norm line 59
Source documentation
Uniform height control is required at every prefix, not only at the end.
```
theorem framedSteps_norm (g : positiveTriangular n) (l : List (positiveTriangular n))
    {H M : ℝ} (hM : 0 ≤ M) (hl : ∀ a ∈ l, ‖matrix a‖ ≤ M)
    (hpath : ∀ p q : List (positiveTriangular n), p ++ q = l →
      ‖(height (g * p.prod)).toAdd‖ ≤ H) :
    ∀ a ∈ framedSteps g l, ‖a‖ ≤ Real.exp H * M * Real.exp H := by
…
```
Mentions: OAI.PolycyclicRecognition.positiveTriangular, OAI.PolycyclicRecognition.PositiveTriangular.matrix, OAI.PolycyclicRecognition.PositiveTriangular.height, OAI.PolycyclicRecognition.PositiveTriangular.framedSteps
theorem OAI.PolycyclicRecognition.PositiveTriangular.frame_one line 85
theorem OAI.PolycyclicRecognition.PositiveTriangular.matrix_prod line 90
theorem OAI.PolycyclicRecognition.PositiveTriangular.norm_word_prod_le line 101
Source documentation
Concrete bounded-height words have polynomially bounded endpoint matrices. The degree is fixed by the matrix dimension and is independent of the word.
```
theorem norm_word_prod_le (l : List (positiveTriangular n))
    {H M : ℝ} (hM : 0 ≤ M) (hl : ∀ a ∈ l, ‖matrix a‖ ≤ M)
    (hpath : ∀ p q : List (positiveTriangular n), p ++ q = l →
      ‖(height p.prod).toAdd‖ ≤ H) :
    ‖matrix l.prod‖ ≤ ((n : ℝ) * (1 + (Real.exp H * M * Real.exp H + 1)) ^ n *
      (1 + (l.length : ℝ)) ^ n) * Real.exp H := by
…
```
Mentions: OAI.PolycyclicRecognition.positiveTriangular, OAI.PolycyclicRecognition.PositiveTriangular.matrix, OAI.PolycyclicRecognition.PositiveTriangular.height

theorem OAI.PolycyclicRecognition.PositiveTriangular.norm_mapped_word_prod_le line 136

Source documentation

The word estimate also applies to a concrete triangular representation of another group, preserving every prefix-height hypothesis.

theorem norm_mapped_word_prod_le {G : Type*} [Group G]
    (ρ : G →* positiveTriangular n) (l : List G)
    {H M : ℝ} (hM : 0 ≤ M) (hl : ∀ a ∈ l, ‖matrix (ρ a)‖ ≤ M)
    (hpath : ∀ p q : List G, p ++ q = l → ‖(height (ρ p.prod)).toAdd‖ ≤ H) :
    ‖matrix (ρ l.prod)‖ ≤ ((n : ℝ) * (1 + (Real.exp H * M * Real.exp H + 1)) ^ n *
      (1 + (l.length : ℝ)) ^ n) * Real.exp H := by
…

Mentions: OAI.PolycyclicRecognition.positiveTriangular, OAI.PolycyclicRecognition.PositiveTriangular.matrix, OAI.PolycyclicRecognition.PositiveTriangular.height