SmoothingInverse.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Invertibility and inverse bounds for the smoothed pair

theorem OAI.KadisonKastler.isUnit_of_two_approximate_inverses line 15
Source documentation
Two approximate inverse identities give an actual inverse. The algebra need not be directly finite.
```
theorem isUnit_of_two_approximate_inverses (a c : A)
    (hac : ‖a * c - 1‖ < 1) (hca : ‖c * a - 1‖ < 1) : IsUnit a := by
…
```

theorem OAI.KadisonKastler.norm_inverse_le_of_approximate_inverse line 38

Source documentation

The inverse bound only needs the approximate right inverse once actual invertibility has been established.

theorem norm_inverse_le_of_approximate_inverse (a : Aˣ) (c : A) {η : ℝ}
    (hη : η < 1) (hac : ‖(a : A) * c - 1‖ ≤ η) :
    ‖((a⁻¹ : Aˣ) : A)‖ ≤ ‖c‖ / (1 - η) := by
…

theorem OAI.KadisonKastler.norm_unitary_star_sub_approximate_inverse_le line 54