CornerUnitary.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Extending a corner unitary by the identity

A unitary on a closed subspace extends to a unitary on the ambient Hilbert space, acting as the identity on the orthogonal complement. Its displacement from the identity is exactly the displacement in the corner.

theorem OAI.KadisonKastler.starProjection_mul_cornerExtension line 19
theorem OAI.KadisonKastler.cornerExtension_mul_starProjection line 23
theorem OAI.KadisonKastler.complement_mul_cornerExtension line 27
theorem OAI.KadisonKastler.cornerExtension_mul_complement line 31
theorem OAI.KadisonKastler.corner_starProjection_star line 37
theorem OAI.KadisonKastler.corner_complement_sq line 42
theorem OAI.KadisonKastler.cornerExtension_add_complement_mem_unitary line 49
def OAI.KadisonKastler.cornerUnitary line 68
Source documentation
The unitary equal to v on E and to the identity on Eᗮ.
```
def cornerUnitary (v : unitary (E →L[ℂ] E)) : unitary (H →L[ℂ] H) :=
…
```
theorem OAI.KadisonKastler.coe_cornerUnitary line 72
theorem OAI.KadisonKastler.cornerUnitary_apply line 76
theorem OAI.KadisonKastler.cornerUnitary_sub_one line 82
theorem OAI.KadisonKastler.norm_cornerUnitary_sub_one line 88
theorem OAI.KadisonKastler.cornerUnitary_mem line 92
theorem OAI.KadisonKastler.unitaryConj_cornerExtension line 99
Source documentation
Extending by the identity intertwines corner and ambient conjugation.
```
theorem unitaryConj_cornerExtension (v : unitary (E →L[ℂ] E)) (T : E →L[ℂ] E) :
    unitaryConj (cornerUnitary E v) (cornerExtension E T) =
      cornerExtension E (unitaryConj v T) := by
…
```
Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.cornerUnitary, OAI.KadisonKastler.cornerExtension