ExponentialRemainder.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform estimates for the exponential inverse near zero

These elementary Banach-algebra estimates are used to recover a small normalizer's infinitesimal generator inside its invariant algebra.

theorem OAI.KadisonKastler.norm_pow_succ_sub_pow_succ_le line 20

Source documentation

A bound independent of the algebra and of commutation of the two elements.

theorem norm_pow_succ_sub_pow_succ_le (x y : A) {r : ℝ} (hr : 0 ≤ r)
    (hx : ‖x‖ ≤ r) (hy : ‖y‖ ≤ r) (n : ℕ) :
    ‖x ^ (n + 1) - y ^ (n + 1)‖ ≤ (n + 1 : ℝ) * r ^ n * ‖x - y‖ := by
…

theorem OAI.KadisonKastler.exponential_derivative_coefficient_le_one line 43
Source documentation
Differentiating a positive-degree exponential coefficient never gives an absolute value larger than one.
```
theorem exponential_derivative_coefficient_le_one (n : ℕ) :
    ((n + 1 : ℝ) / (n + 1).factorial) ≤ 1 := by
…
```
def OAI.KadisonKastler.exponentialRemainder line 54
Source documentation
The exponential after removing its constant and linear terms.
```
def exponentialRemainder (x : A) : A := NormedSpace.exp x - 1 - x
```
theorem OAI.KadisonKastler.hasSum_exponentialRemainder line 56
theorem OAI.KadisonKastler.norm_exponential_term_sub_le line 64
theorem OAI.KadisonKastler.norm_exponentialRemainder_sub_le line 89