UnipotentProducts.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Concrete polynomial bounds for unipotent matrix products

Products of n strictly upper triangular n × n matrices vanish, even when the factors are different. Consequently the preceding fixed-degree estimate applies to arbitrarily long products of unipotent increments.

def OAI.PolycyclicRecognition.StrictUpper line 19
Source documentation
Strict upper triangularity, with diagonal vanishing included.
```
def StrictUpper (A : Matrix (Fin n) (Fin n) R) : Prop :=
…
```
theorem OAI.PolycyclicRecognition.strictUpper_prod_entry_zero line 24
Source documentation
Every strictly upper triangular factor advances the row-to-column index by at least one. This is valid for ordered products of distinct matrices.
```
theorem strictUpper_prod_entry_zero (l : List (Matrix (Fin n) (Fin n) R))
    (hl : ∀ A ∈ l, StrictUpper A) (i j : Fin n)
    (hij : (j : ℕ) < (i : ℕ) + l.length) : l.prod i j = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.StrictUpper
theorem OAI.PolycyclicRecognition.strictUpper_prod_zero line 46
Source documentation
The nilpotence bound is the matrix dimension and is independent of all coefficients and of the choice of factors.
```
theorem strictUpper_prod_zero (l : List (Matrix (Fin n) (Fin n) R))
    (hl : ∀ A ∈ l, StrictUpper A) (hn : n ≤ l.length) : l.prod = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.StrictUpper
theorem OAI.PolycyclicRecognition.StrictUpper.pow_eq_zero line 54
Source documentation
A strictly upper triangular matrix has nilpotence degree at most its size.
```
theorem StrictUpper.pow_eq_zero {A : Matrix (Fin n) (Fin n) R} (hA : StrictUpper A) :
    A ^ n = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.StrictUpper

theorem OAI.PolycyclicRecognition.norm_unipotent_prod_le line 71

Source documentation

A fully concrete polynomial bound: uniformly bounded upper unipotent increments have product norm bounded by a degree-n polynomial in their number.

theorem norm_unipotent_prod_le (l : List (Matrix (Fin n) (Fin n) ℝ))
    (hl : ∀ A ∈ l, StrictUpper A) {M : ℝ} (hM : 0 ≤ M)
    (hbound : ∀ A ∈ l, ‖A‖ ≤ M) :
    ‖(l.map (fun A => 1 + A)).prod‖ ≤
      (n : ℝ) * (1 + M) ^ n * (1 + (l.length : ℝ)) ^ n := by
…

Mentions: OAI.PolycyclicRecognition.StrictUpper