NilpotentExponential.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exponential coordinates for upper unipotent matrices

The analytic matrix exponential is a finite polynomial on nilpotent matrices. This bridges the ordered-product bounds to actual exponential increments, rather than a separately stipulated polynomial group law.

theorem OAI.PolycyclicRecognition.exp_eq_finite_sum_of_pow_eq_zero line 24

Source documentation

Nilpotence truncates the analytic exponential exactly.

theorem exp_eq_finite_sum_of_pow_eq_zero (x : A) {c : ℕ} (hx : x ^ c = 0) :
    NormedSpace.exp x = ∑ k ∈ Finset.range c, ((k.factorial : ℝ)⁻¹) • x ^ k := by
…

theorem OAI.PolycyclicRecognition.norm_exp_sub_one_le_of_pow_eq_zero line 34

Source documentation

The polynomial exponential gives a uniform increment bound on any fixed bounded set of nilpotent logarithms.

theorem norm_exp_sub_one_le_of_pow_eq_zero [NormOneClass A]
    (x : A) {c : ℕ} (hx : x ^ (c + 1) = 0)
    {M : ℝ} (hM : 0 ≤ M) (hbound : ‖x‖ ≤ M) :
    ‖NormedSpace.exp x - 1‖ ≤ (c : ℝ) * (1 + M) ^ c := by
…

theorem OAI.PolycyclicRecognition.StrictUpper.pow line 70
theorem OAI.PolycyclicRecognition.StrictUpper.exp_sub_one line 84

theorem OAI.PolycyclicRecognition.norm_prod_exp_strictUpper_le line 107

Source documentation

Ordered products of actual matrix exponentials of bounded strictly upper triangular logarithms satisfy a polynomial bound, uniformly in word length.

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

Mentions: OAI.PolycyclicRecognition.StrictUpper