MixedComplement.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The complementary action in mixed cancellation

An exact corner comparison determines a unitary on the complementary full isometric copy. The full error is the sum of the mixed-corner error and this concrete complementary conjugation error. A fixed-complement extension of a partial isometry is also given; connectedness is not inferred from its unitary identities.

lemma OAI.WeakPureInfiniteness.unitary_commutes_of_conjugation_eq line 23
Source documentation
Exact projection transport by a unitary implies commutation with the projection when its initial and final projections agree.
```
lemma unitary_commutes_of_conjugation_eq (u : unitary E) (q : E)
    (hq : (u : E) * q * star (u : E) = q) : Commute (u : E) q := by
…
```
lemma OAI.WeakPureInfiniteness.exists_complementary_compression_unitary line 33
Source documentation
Compressing a projection-preserving unitary to its complementary full isometry gives an actual unitary, with the exact intertwining relation.
```
lemma exists_complementary_compression_unitary (r : E) (hr : star r * r = 1)
    (u : unitary E) (hp : Commute (u : E) (r * star r)) :
    ∃ h : unitary E, (h : E) = star r * (u : E) * r ∧ (u : E) * r = r * (h : E) := by
…
```
lemma OAI.WeakPureInfiniteness.complementary_conjugation_decomposition line 65

lemma OAI.WeakPureInfiniteness.exists_mixed_complement_unitary line 79

Source documentation

The remaining term is an actual conjugation by the compressed unitary. It is not estimated by zero merely because the mixed corner is controlled.

lemma exists_mixed_complement_unitary [Nontrivial E] (s t : ℕ → E)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (u : unitary E)
    (huq : (u : E) * canonicalTailProjection t 1 * star (u : E) = canonicalTailProjection t 1) :
    ∃ h : unitary E, (h : E) = star (t 0) * (u : E) * t 0 ∧
      (u : E) * t 0 = t 0 * (h : E) ∧
      ∀ i, ‖(u : E) * mixedSwappedRow s t i * star (u : E) - mixedStabilizedRow t t i‖ ≤
        ‖(h : E) * t i * star (h : E) - t i‖ +
          ‖(u : E) * mixedNegativeRow s t i * star (u : E) - canonicalNegativeRow t i‖ := by
…

Mentions: OAI.WeakPureInfiniteness.canonicalTailProjection, OAI.WeakPureInfiniteness.mixedSwappedRow, OAI.WeakPureInfiniteness.mixedStabilizedRow, OAI.WeakPureInfiniteness.mixedNegativeRow, OAI.WeakPureInfiniteness.canonicalNegativeRow

lemma OAI.WeakPureInfiniteness.exists_fixed_complement_unitary_extension line 117

Source documentation

The prescribed complementary isometries provide the literal extension W + z w*. This theorem asserts unitarity and both exact actions only.

lemma exists_fixed_complement_unitary_extension (q p W w z : E)
    (hq : star q = q) (hp : star p = p)
    (hW : star W * W = q) (hWW : W * star W = p) (hWq : W * q = W)
    (hw : star w * w = 1) (hww : w * star w = 1 - q)
    (hz : star z * z = 1) (hzz : z * star z = 1 - p) :
    ∃ u : unitary E, (u : E) = W + z * star w ∧ (u : E) * q = W ∧ (u : E) * w = z := by
…