CommonCornerShrink.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Quantitative shrinking to a common corner

The explicit coisometry filler turns the canonical-shift implementer into a partial isometry. Its initial and final projections are exact, and its conjugation error is the shift error itself.

lemma OAI.WeakPureInfiniteness.finiteCuntzTransfer_conjugate_commuting line 21

lemma OAI.WeakPureInfiniteness.binary_shift_shrink_difference line 45

Source documentation

Exact error formula for the inserted-unitary shrink.

lemma binary_shift_shrink_difference (r a : Fin 2 → E)
    (hr : ∀ i j, star (r i) * r j = if i = j then 1 else 0)
    (ha : ∀ i j, star (a i) * a j = if i = j then 1 else 0)
    (has : (∑ i, a i * star (a i)) = 1) (u : unitary E)
    (x : E) (hx : ∀ i, Commute x (r i) ∧ Commute x (star (r i))) :
    let v := (u : E) * finiteCuntzTransfer r a 1
…

Mentions: OAI.WeakPureInfiniteness.finiteCuntzTransfer

lemma OAI.WeakPureInfiniteness.binary_shift_shrink_error line 98

lemma OAI.WeakPureInfiniteness.exists_canonicalShift_prefix_inverse line 127

Source documentation

The inverse shift implementer controls every prescribed encoded prefix element, with its tolerance chosen after the prefix length.

lemma exists_canonicalShift_prefix_inverse [Nontrivial E]
    (a : Fin 2 → E)
    (ha : ∀ i j, star (a i) * a j = if i = j then 1 else 0)
    (has : (∑ i, a i * star (a i)) = 1) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ u : unitary E, ∀ i ≤ m,
      ‖(u : E) * finiteRowShift a (a 0 ^ i * a 1) * star (u : E) -
        (a 0 ^ i * a 1)‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.finiteRowShift

lemma OAI.WeakPureInfiniteness.exists_binary_encoded_shrink line 183

Source documentation

A concrete partial isometry shrinks the whole unit past r₀, while approximating the prescribed finite encoded row on the resulting corner.

lemma exists_binary_encoded_shrink [Nontrivial E]
    (r a : Fin 2 → E)
    (hr : ∀ i j, star (r i) * r j = if i = j then 1 else 0)
    (ha : ∀ i j, star (a i) * a j = if i = j then 1 else 0)
    (has : (∑ i, a i * star (a i)) = 1)
    (hc : bergRowsCommute a r) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ C : E, star C * C = 1 ∧ C * star C = 1 - r 0 * star (r 0) ∧
      ∀ i ≤ m, ‖C * (a 0 ^ i * a 1) * star C -
        (a 0 ^ i * a 1) * (1 - r 0 * star (r 0))‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute

lemma OAI.WeakPureInfiniteness.exists_relative_binary_encoded_shrink line 205

Source documentation

The same shrink inside an actual projection corner. Both support identities and both Murray--von Neumann projections are part of the output.

lemma exists_relative_binary_encoded_shrink
    (q : E) (hq : star q = q) (hqq : q * q = q) (hq0 : q ≠ 0)
    (r a : Fin 2 → E)
    (hrs : ∀ i, q * r i = r i ∧ r i * q = r i)
    (hasp : ∀ i, q * a i = a i ∧ a i * q = a i)
    (hr : ∀ i j, star (r i) * r j = if i = j then q else 0)
    (ha : ∀ i j, star (a i) * a j = if i = j then q else 0)
    (has : (∑ i, a i * star (a i)) = q)
    (hc : bergRowsCommute a r) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ C : E, q * C = C ∧ C * q = C ∧ star C * C = q ∧
      C * star C = q - r 0 * star (r 0) ∧
      ∀ i ≤ m, ‖C * (a 0 ^ i * a 1) * star C -
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute

lemma OAI.WeakPureInfiniteness.exists_canonicalNegative_common_shrink line 252

Source documentation

Concrete transfer from the first stabilized unit to the common unit. The binary encoding is chosen inside the source algebra, so it commutes with the other canonical row without an added uniqueness hypothesis.

lemma exists_canonicalNegative_common_shrink [Nontrivial E]
    (C D : StarSubalgebra ℂ E) [IsClosed (C : Set E)] [IsClosed (D : Set E)]
    (hc : ∀ x : C, ∀ y : D, Commute (x : E) (y : E))
    (s : ℕ → C) (t : ℕ → D)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    let S : ℕ → E := fun i => s i
…

lemma OAI.WeakPureInfiniteness.exists_canonicalNegative_shrink line 366

Source documentation

The shrink for the two given canonical rows; no chosen encoding or extra commutant hypothesis occurs in this application.

lemma exists_canonicalNegative_shrink [Nontrivial E]
    (s t : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (hc : bergRowsCommute s t) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    let P := canonicalTailProjection s 1
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.canonicalTailProjection