PublishedTypeIIIProjection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The two projection inputs needed for type III compression

Blackadar, Operator Algebras (2006), I.6.1.2--5 and I.9.2.1(iv), give a nonzero spectral projection above any positive threshold below the norm of a positive element. III.1.3.5--7 and III.1.4.2 give equivalence of every nonzero projection to the identity in a countably decomposable type III factor. Only these projection statements are assumed below. Neither input asserts simplicity of an ultraproduct or a perturbation bound.

def OAI.KadisonKastler.FiniteProjectionIn line 34
Source documentation
Finiteness of a projection: an isometry with initial projection p and range under p has range exactly p.
```
def FiniteProjectionIn (M : VonNeumannAlgebra H) (p : Algebra M) : Prop :=
…
```
Mentions: OAI.KadisonKastler.Algebra
structure OAI.KadisonKastler.TypeIIIFactor line 39
Source documentation
The ordinary nonzero type III factor conditions, with type III expressed as absence of nonzero finite projections.
```
structure TypeIIIFactor (M : VonNeumannAlgebra H) : Prop where
…
```
def OAI.KadisonKastler.PublishedVonNeumannSpectralCut line 44
def OAI.KadisonKastler.PublishedTypeIIIProjectionComparison line 51
theorem OAI.KadisonKastler.typeIII_positive_compression line 58