TriangularProducts.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Polynomial products with bounded diagonal prefixes

For an upper triangular matrix path, remove the diagonal of each prefix. The resulting increments are unipotent. If the original increments are bounded and all diagonal prefixes and their inverses are bounded, the unipotent increments are uniformly bounded. Their products therefore have polynomial size. This is the coordinate estimate behind bounded-height path packing.

def OAI.PolycyclicRecognition.gaugedFactors line 23

Source documentation

Change of diagonal frame at each successive prefix of a word.

def gaugedFactors (d : ℕ → Rˣ) : ℕ → List R → List R
  | _, [] => []
  | k, a :: l => ((d k : R) * a * (↑(d (k + 1))⁻¹ : R)) :: gaugedFactors d (k + 1) l

theorem OAI.PolycyclicRecognition.gaugedFactors_length line 27
theorem OAI.PolycyclicRecognition.gaugedFactors_prod line 34
Source documentation
All internal changes of frame cancel exactly.
```
theorem gaugedFactors_prod (d : ℕ → Rˣ) (k : ℕ) (l : List R) :
    (gaugedFactors d k l).prod = (d k : R) * l.prod * (↑(d (k + l.length))⁻¹ : R) := by
…
```
Mentions: OAI.PolycyclicRecognition.gaugedFactors

theorem OAI.PolycyclicRecognition.norm_gaugedFactors_le line 52

Source documentation

A bounded frame and its inverse give uniformly bounded gauged increments.

theorem norm_gaugedFactors_le (d : ℕ → Rˣ) (k : ℕ) (l : List R)
    {B M : ℝ} (hB : 0 ≤ B) (hM : 0 ≤ M)
    (hd : ∀ i, ‖(d i : R)‖ ≤ B ∧ ‖(↑(d i)⁻¹ : R)‖ ≤ B)
    (hl : ∀ a ∈ l, ‖a‖ ≤ M) :
    ∀ a ∈ gaugedFactors d k l, ‖a‖ ≤ B * M * B := by
…

Mentions: OAI.PolycyclicRecognition.gaugedFactors

def OAI.PolycyclicRecognition.diagonalUnit line 78
Source documentation
A diagonal unit is represented by a genuine invertible diagonal matrix.
```
def diagonalUnit (d : Fin n → ℝˣ) : (Matrix (Fin n) (Fin n) ℝ)ˣ where
…
```

theorem OAI.PolycyclicRecognition.strictUpper_diagonal_gauge line 91

Source documentation

Matching successive prefix diagonals makes each gauged increment unipotent.

theorem strictUpper_diagonal_gauge (A : Matrix (Fin n) (Fin n) ℝ)
    (hA : A.IsUpperTriangular) (d e : Fin n → ℝˣ)
    (hdiag : ∀ i, (d i : ℝ) * A i i = (e i : ℝ)) :
    StrictUpper ((diagonalUnit d : Matrix (Fin n) (Fin n) ℝ) * A *
      (↑(diagonalUnit e)⁻¹ : Matrix (Fin n) (Fin n) ℝ) - 1) := by
…

Mentions: OAI.PolycyclicRecognition.StrictUpper, OAI.PolycyclicRecognition.diagonalUnit

theorem OAI.PolycyclicRecognition.norm_triangular_prod_le line 111

Source documentation

Uniformly bounded upper triangular increments and bounded diagonal prefixes have polynomially bounded product. The strict-upper condition is supplied by strictUpper_diagonal_gauge for the actual prefix diagonals.

theorem norm_triangular_prod_le (d : ℕ → (Matrix (Fin n) (Fin n) ℝ)ˣ)
    (l : List (Matrix (Fin n) (Fin n) ℝ)) {B M : ℝ} (hB : 0 ≤ B) (hM : 0 ≤ M)
    (hd0 : d 0 = 1)
    (hd : ∀ i, ‖(d i : Matrix (Fin n) (Fin n) ℝ)‖ ≤ B ∧
      ‖(↑(d i)⁻¹ : Matrix (Fin n) (Fin n) ℝ)‖ ≤ B)
    (hl : ∀ a ∈ l, ‖a‖ ≤ M)
    (hstrict : ∀ a ∈ gaugedFactors d 0 l, StrictUpper (a - 1)) :
    ‖l.prod‖ ≤ ((n : ℝ) * (1 + (B * M * B + 1)) ^ n *
      (1 + (l.length : ℝ)) ^ n) * B := by
…

Mentions: OAI.PolycyclicRecognition.gaugedFactors, OAI.PolycyclicRecognition.StrictUpper