RepresentedCorner.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Concrete compression to a common closed subspace

The corner acts on the subspace itself. Its operators are characterized by membership of their extension by zero in the original von Neumann algebra. This constructs the actual corner and proves that a common compression does not increase Kadison--Kastler distance.

def OAI.KadisonKastler.cornerExtension line 25
Source documentation
Extension by zero on the orthogonal complement.
```
def cornerExtension : (E →L[ℂ] E) →ₗ[ℂ] (H →L[ℂ] H) where
…
```
def OAI.KadisonKastler.cornerCompression line 31
Source documentation
Compression of an arbitrary ambient operator.
```
def cornerCompression : (H →L[ℂ] H) →ₗ[ℂ] (E →L[ℂ] E) where
…
```
theorem OAI.KadisonKastler.cornerExtension_apply line 36
theorem OAI.KadisonKastler.cornerCompression_apply line 39
theorem OAI.KadisonKastler.cornerCompression_extension line 42
theorem OAI.KadisonKastler.cornerExtension_compression line 48
theorem OAI.KadisonKastler.cornerExtension_one line 53
theorem OAI.KadisonKastler.cornerExtension_mul line 57
theorem OAI.KadisonKastler.cornerExtension_star line 67
theorem OAI.KadisonKastler.norm_cornerCompression_le line 76
theorem OAI.KadisonKastler.norm_cornerExtension_le line 81
theorem OAI.KadisonKastler.norm_cornerExtension line 88

theorem OAI.KadisonKastler.inner_cornerExtension line 94

Source documentation

Coefficients of extension are coefficients on the projected vectors.

theorem inner_cornerExtension (T : E →L[ℂ] E) (x y : H) :
    inner ℂ y (cornerExtension E T x) =
      inner ℂ (E.orthogonalProjectionOnto y) (T (E.orthogonalProjectionOnto x)) := by
…

Mentions: OAI.KadisonKastler.cornerExtension

def OAI.KadisonKastler.cornerExtensionWOT line 100
theorem OAI.KadisonKastler.continuous_cornerExtensionWOT line 105
def OAI.KadisonKastler.representedCornerAlgebra line 114
Source documentation
The algebra of the concrete corner; its identity extends to the given orthogonal projection in the ambient algebra.
```
def representedCornerAlgebra (M : VonNeumannAlgebra H) (hp : E.starProjection ∈ M) :
    StarSubalgebra ℂ (E →L[ℂ] E) where
…
```
theorem OAI.KadisonKastler.representedCornerAlgebra_wotClosed line 138
def OAI.KadisonKastler.representedCorner line 146
Source documentation
Compression of a von Neumann algebra to the range of one of its projections, represented on that range.
```
def representedCorner (M : VonNeumannAlgebra H) (hp : E.starProjection ∈ M) :
    VonNeumannAlgebra E :=
…
```
theorem OAI.KadisonKastler.mem_representedCorner line 151
theorem OAI.KadisonKastler.cornerCompression_mem line 155
theorem OAI.KadisonKastler.cornerExtension_mem_unitBall line 162
Source documentation
Every corner contraction extends to an ambient contraction.
```
theorem cornerExtension_mem_unitBall {M : VonNeumannAlgebra H}
    (hp : E.starProjection ∈ M) {T : E →L[ℂ] E}
    (hT : T ∈ unitBall (representedCorner E M hp)) :
    cornerExtension E T ∈ unitBall M :=
…
```
Mentions: OAI.KadisonKastler.unitBall, OAI.KadisonKastler.representedCorner, OAI.KadisonKastler.cornerExtension
theorem OAI.KadisonKastler.kkDistance_representedCorner_le line 170
Source documentation
Compressing the same projection in both algebras does not increase their ordinary Kadison--Kastler distance.
```
theorem kkDistance_representedCorner_le (M N : VonNeumannAlgebra H)
    (hM : E.starProjection ∈ M) (hN : E.starProjection ∈ N) :
    kkDistance (representedCorner E M hM) (representedCorner E N hN) ≤ kkDistance M N := by
…
```
Mentions: OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.representedCorner