NilpotentProducts.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Polynomial bounds for products with nilpotent increments

The finite-degree product estimate in the nilpotent-coordinate argument is proved here in a normed associative algebra. The factors need not commute. Homogeneous terms are sums over ordered sublists, so nilpotence truncates the expansion before a fixed degree, independently of the number of factors.

def OAI.PolycyclicRecognition.homogeneousProduct line 28
Source documentation
The degree-k part of an ordered product of 1 + x.
```
def homogeneousProduct (l : List A) (k : ℕ) : A :=
…
```
theorem OAI.PolycyclicRecognition.homogeneousProduct_zero line 31
theorem OAI.PolycyclicRecognition.homogeneousProduct_nil_succ line 34
theorem OAI.PolycyclicRecognition.homogeneousProduct_cons_succ line 38
theorem OAI.PolycyclicRecognition.homogeneousProduct_eq_zero_of_length_lt line 45
theorem OAI.PolycyclicRecognition.prod_one_add_eq_sum_homogeneous line 50
Source documentation
Exact ordered expansion; no commutativity hypothesis is used.
```
theorem prod_one_add_eq_sum_homogeneous (l : List A) :
    (l.map (fun x => 1 + x)).prod =
      ∑ k ∈ Finset.range (l.length + 1), homogeneousProduct l k := by
…
```
Mentions: OAI.PolycyclicRecognition.homogeneousProduct

theorem OAI.PolycyclicRecognition.homogeneousProduct_eq_zero_of_nilpotence line 76

Source documentation

Nilpotence kills every homogeneous term of sufficiently high degree.

theorem homogeneousProduct_eq_zero_of_nilpotence (S : Set A) (c : ℕ)
    (hnil : ∀ l : List A, (∀ x ∈ l, x ∈ S) → c ≤ l.length → l.prod = 0)
    (l : List A) (hl : ∀ x ∈ l, x ∈ S) {k : ℕ} (hk : c ≤ k) :
    homogeneousProduct l k = 0 := by
…

Mentions: OAI.PolycyclicRecognition.homogeneousProduct

theorem OAI.PolycyclicRecognition.prod_one_add_eq_truncated line 88

Source documentation

Truncating at the nilpotence degree is exact even for arbitrarily many factors.

theorem prod_one_add_eq_truncated (S : Set A) (c : ℕ)
    (hnil : ∀ l : List A, (∀ x ∈ l, x ∈ S) → c ≤ l.length → l.prod = 0)
    (l : List A) (hl : ∀ x ∈ l, x ∈ S) :
    (l.map (fun x => 1 + x)).prod =
      ∑ k ∈ Finset.range c, homogeneousProduct l k := by
…

Mentions: OAI.PolycyclicRecognition.homogeneousProduct

theorem OAI.PolycyclicRecognition.norm_homogeneousProduct_le line 111
Source documentation
Each homogeneous term has the binomial bound expected from its ordered sublist expansion.
```
theorem norm_homogeneousProduct_le (l : List A) {M : ℝ} (hM : 0 ≤ M)
    (hl : ∀ x ∈ l, ‖x‖ ≤ M) (k : ℕ) :
    ‖homogeneousProduct l k‖ ≤ (l.length.choose k : ℝ) * M ^ k := by
…
```
Mentions: OAI.PolycyclicRecognition.homogeneousProduct

theorem OAI.PolycyclicRecognition.norm_prod_one_add_le_polynomial line 136

Source documentation

Fixed nilpotence degree turns the ordered product expansion into a polynomial bound in the number of factors.

theorem norm_prod_one_add_le_polynomial (S : Set A) (c : ℕ)
    (hnil : ∀ l : List A, (∀ x ∈ l, x ∈ S) → c ≤ l.length → l.prod = 0)
    {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ x ∈ S, ‖x‖ ≤ M)
    (l : List A) (hl : ∀ x ∈ l, x ∈ S) :
    ‖(l.map (fun x => 1 + x)).prod‖ ≤
      (c : ℝ) * (1 + M) ^ c * (1 + (l.length : ℝ)) ^ c := by
…

theorem OAI.PolycyclicRecognition.norm_inv_le_of_nilpotent_sub_one line 171
Source documentation
The inverse of a nilpotent perturbation of one is a finite geometric sum, with a bound that is polynomial in the perturbation norm.
```
theorem norm_inv_le_of_nilpotent_sub_one (u : Aˣ) (c : ℕ)
    (hn : (1 - (u : A)) ^ c = 0) :
    ‖(↑u⁻¹ : A)‖ ≤ (c : ℝ) * (1 + ‖1 - (u : A)‖) ^ c := by
…
```