Polar.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Polar unitaries close to the identity

We construct the polar factor of an invertible element using the positive square root supplied by continuous functional calculus.

theorem OAI.KadisonKastler.isUnit_abs line 29
Source documentation
The absolute value of an invertible element is invertible.
```
theorem isUnit_abs (t : Aˣ) : IsUnit (CFC.abs (t : A)) := by
…
```
theorem OAI.KadisonKastler.exists_unitary_mul_abs line 34
Source documentation
Polar decomposition of an invertible element, with unitary polar factor.
```
theorem exists_unitary_mul_abs (t : Aˣ) :
    ∃ u : unitary A, (u : A) * CFC.abs (t : A) = (t : A) := by
…
```

theorem OAI.KadisonKastler.norm_unit_inv_le_of_near_one line 62

Source documentation

Inverting a unit close to one gives the usual geometric-series bound.

theorem norm_unit_inv_le_of_near_one [Nontrivial A] (t : Aˣ)
    (ht : ‖(t : A) - 1‖ < 1) :
    ‖((t⁻¹ : Aˣ) : A)‖ ≤ (1 - ‖(t : A) - 1‖)⁻¹ := by
…

theorem OAI.KadisonKastler.norm_positive_unit_sub_one_le line 78

Source documentation

A positive unit with upper bounds on its norm and inverse lies within the same radius of the identity.

theorem norm_positive_unit_sub_one_le [Nontrivial A] (s : Aˣ) (hs : 0 ≤ (s : A)) {r : ℝ}
    (hr : 0 ≤ r) (hr₁ : r < 1) (hnorm : ‖(s : A)‖ ≤ 1 + r)
    (hinv : ‖((s⁻¹ : Aˣ) : A)‖ ≤ (1 - r)⁻¹) :
    ‖(s : A) - 1‖ ≤ r := by
…

theorem OAI.KadisonKastler.norm_abs_sub_one_le line 105
Source documentation
Taking the absolute value of a unit does not increase its distance from one, provided that distance is less than one.
```
theorem norm_abs_sub_one_le [Nontrivial A] (t : Aˣ)
    (ht : ‖(t : A) - 1‖ < 1) :
    ‖CFC.abs (t : A) - 1‖ ≤ ‖(t : A) - 1‖ := by
…
```

theorem OAI.KadisonKastler.exists_polar_unitary_near_one_of_unit line 134

Source documentation

The polar unitary of a unit close to one is within twice that distance of one.

theorem exists_polar_unitary_near_one_of_unit [Nontrivial A] (t : Aˣ)
    (ht : ‖(t : A) - 1‖ < 1) :
    ∃ u : unitary A, (u : A) * CFC.abs (t : A) = (t : A) ∧
      ‖(u : A) - 1‖ ≤ 2 * ‖(t : A) - 1‖ := by
…

theorem OAI.KadisonKastler.exists_polar_unitary_near_one line 154
Source documentation
Every element within distance one of the identity has a unitary polar factor within twice its original distance of the identity.
```
theorem exists_polar_unitary_near_one (T : A) (hT : ‖T - 1‖ < 1) :
    ∃ u : unitary A, (u : A) * CFC.abs T = T ∧ ‖(u : A) - 1‖ ≤ 2 * ‖T - 1‖ := by
…
```

theorem OAI.KadisonKastler.exists_positive_polar_decomposition_near_one line 165

Source documentation

Polar decomposition near one without an order instance in the statement. Positivity of the second factor is expressed as being a star square.

theorem exists_positive_polar_decomposition_near_one (T : A) (hT : ‖T - 1‖ < 1) :
    ∃ (u : unitary A) (p : A), (∃ q : A, p = star q * q) ∧
      p * p = star T * T ∧ (u : A) * p = T ∧ ‖(u : A) - 1‖ ≤ 2 * ‖T - 1‖ := by
…