CompressionTransfer.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Moving a compression into a spare corner

Orthogonal isometries give a uniform path between the two compressions of a unitary. If the second range is in q, its endpoint is exactly a relative unitary extended by 1-q. Centrality of that relative unitary with respect to a coisometric pair in q remains a separate obligation.

def OAI.WeakPureInfiniteness.compressionTransferPath line 21
Source documentation
Move the first compression to the second by rotating the cancelling pair.
```
def compressionTransferPath (a b z : E) (θ : ℝ) : E :=
…
```
lemma OAI.WeakPureInfiniteness.exists_controlled_compressionTransfer line 24
def OAI.WeakPureInfiniteness.compressedRelativeUnitary line 56
Source documentation
The moved compression as an element of the specified relative corner.
```
def compressedRelativeUnitary (q b z : E) : E := b * z * star b + (q - b * star b)
```
lemma OAI.WeakPureInfiniteness.compressedRelativeUnitary_extension line 58
lemma OAI.WeakPureInfiniteness.compressedRelativeUnitary_properties line 63

lemma OAI.WeakPureInfiniteness.compressedRelativeUnitary_commutator line 130

Source documentation

This exact formula records the extra commutators required after transfer. Centrality of z alone does not remove the range-projection terms.

lemma compressedRelativeUnitary_commutator (q b z y : E) :
    compressedRelativeUnitary q b z * y - y * compressedRelativeUnitary q b z =
      b * (z * y - y * z) * star b +
        (b * y - y * b) * (z - 1) * star b +
        b * (z - 1) * (star b * y - y * star b) + (q * y - y * q) := by
…

Mentions: OAI.WeakPureInfiniteness.compressedRelativeUnitary