ClosedUnitaryApproximation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Unitary approximation in a closed neighbouring algebra

Spectral permanence reflects invertibility of a sufficiently close contraction into the closed subalgebra. Its polar unitary then has at most three times the original approximation error. No finiteness assumption on the target is needed.

theorem OAI.KadisonKastler.isUnit_of_near_ambient_unitary line 23

Source documentation

Invertibility near an ambient unitary is reflected into a closed C-star subalgebra.

theorem isUnit_of_near_ambient_unitary (S : StarSubalgebra ℂ A)
    [IsClosed (S : Set A)] (u : unitary A) (x : S)
    (hclose : ‖(x : A) - (u : A)‖ < 1) : IsUnit x := by
…

theorem OAI.KadisonKastler.exists_unitary_near_of_closed_subalgebra line 36

Source documentation

Polar normalization of a nearby contraction in an arbitrary closed subalgebra costs a factor of three.

theorem exists_unitary_near_of_closed_subalgebra (S : StarSubalgebra ℂ A)
    [IsClosed (S : Set A)] (u : unitary A) (x : S) (hx : ‖x‖ ≤ 1)
    (hclose : ‖(x : A) - (u : A)‖ < 1) :
    ∃ v : unitary S, ‖(v : A) - (u : A)‖ ≤ 3 * ‖(x : A) - (u : A)‖ := by
…

theorem OAI.KadisonKastler.exists_unitary_approx_of_small_kkDistance line 58
Source documentation
A sufficiently small Kadison--Kastler gap supplies unitary approximants in the second algebra, regardless of its type.
```
theorem exists_unitary_approx_of_small_kkDistance {b : ℝ}
    (hb : b ≤ 1) (hgap : kkDistance M N < b) (u : unitary (Algebra M)) :
    ∃ v : unitary (Algebra N),
      ‖(v : H →L[ℂ] H) - (u : H →L[ℂ] H)‖ < 3 * b := by
…
```
Mentions: OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.exists_unitary_approx_of_nearInclusion line 74
Source documentation
Strict one-sided near inclusion also supplies unitary approximants. The additional factor two normalizes the original algebra approximant.
```
theorem exists_unitary_approx_of_nearInclusion {γ : ℝ}
    (hsmall : 2 * γ ≤ 1) (hnear : NearInclusion M N γ)
    (u : unitary (Algebra M)) :
    ∃ v : unitary (Algebra N),
      ‖(v : H →L[ℂ] H) - (u : H →L[ℂ] H)‖ < 6 * γ := by
…
```
Mentions: OAI.KadisonKastler.NearInclusion, OAI.KadisonKastler.Algebra