FiniteNeighbor.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finiteness of a nearby von Neumann algebra

A finite factor has unitary polar decompositions. An isometry close to its unit ball is therefore close to a unitary, hence invertible. This proves the finiteness part of the manuscript's finite-neighbor lemma.

theorem OAI.KadisonKastler.norm_isometry_defect_le line 22
Source documentation
The defect of a contraction near an isometry is at most twice its error.
```
theorem norm_isometry_defect_le {x v : A} (hx : ‖x‖ ≤ 1)
    (hv : star v * v = 1) :
    ‖star x * x - 1‖ ≤ 2 * ‖x - v‖ := by
…
```

theorem OAI.KadisonKastler.norm_unitary_polar_sub_le line 44

Source documentation

A unitary polar factor is close to its element by its isometry defect.

theorem norm_unitary_polar_sub_le (x : A) (u : unitary A)
    [PartialOrder A] [StarOrderedRing A]
    (hu : (u : A) * CFC.abs x = x) :
    ‖(u : A) - x‖ ≤ ‖star x * x - 1‖ := by
…

theorem OAI.KadisonKastler.isometry_coisometry_of_near_unitary line 54

Source documentation

Being within one of a unitary forces an isometry to be unitary.

theorem isometry_coisometry_of_near_unitary {v : A}
    (hv : star v * v = 1) (u : unitary A) (hclose : ‖v - (u : A)‖ < 1) :
    v * star v = 1 := by
…

theorem OAI.KadisonKastler.finite_of_near_finite_factor line 76
Source documentation
Finiteness is preserved by a sufficiently small gap from a finite factor. This is the finiteness assertion of the manuscript's finite-neighbor lemma; factoriality is a separate assertion.
```
theorem finite_of_near_finite_factor
    (hfactor : ∀ x : Algebra M, (∀ y : Algebra M, y * x = x * y) →
      ∃ c : ℂ, x = c • (1 : Algebra M))
    (hfinite : ∀ v : Algebra M, star v * v = 1 → v * star v = 1)
    (hgap : kkDistance M N < 1 / 10) :
    ∀ v : Algebra N, star v * v = 1 → v * star v = 1 := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.kkDistance