RegularizedPolarFactor.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Contractive approximate polar factors inside the original C-star algebra. These avoid any bidual extension in the row-bound argument.

def OAI.KadisonSimilarity.positiveShiftReciprocal line 15
theorem OAI.KadisonSimilarity.positiveShiftReciprocal_continuous line 18
theorem OAI.KadisonSimilarity.positiveShiftReciprocal_selfAdjoint line 25
theorem OAI.KadisonSimilarity.positiveShiftReciprocal_commute line 29
theorem OAI.KadisonSimilarity.positiveShiftReciprocal_inverse line 32
theorem OAI.KadisonSimilarity.positiveShiftReciprocal_mul_norm_le line 48
theorem OAI.KadisonSimilarity.norm_positiveShiftReciprocal_mul_le line 63
Source documentation
The regularized polar factor is contractive without leaving the algebra.
```
theorem norm_positiveShiftReciprocal_mul_le (x h : A) (hh : 0 ≤ h)
    (hsq : x * star x = h * h) {ε : ℝ} (hε : 0 < ε) :
    ‖positiveShiftReciprocal h ε * x‖ ≤ 1 := by
…
```
Mentions: OAI.KadisonSimilarity.positiveShiftReciprocal
theorem OAI.KadisonSimilarity.regularizedPolar_error line 85
Source documentation
The error in the polar factorization has norm at most the regularizer.
```
theorem regularizedPolar_error (x h : A) (hh : 0 ≤ h)
    (hsq : x * star x = h * h) {ε : ℝ} (hε : 0 < ε) :
    ‖x - h * (positiveShiftReciprocal h ε * x)‖ ≤ ε := by
…
```
Mentions: OAI.KadisonSimilarity.positiveShiftReciprocal