OAI/Analysis/OInfinity/ZeroCorner.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

An explicit coisometric pair in the complementary corner

Three orthogonal isometries suffice to construct two relative isometries whose ranges add up to 1 - r₀ * star r₀. The construction uses the checked two-swap completion, with its connected unitary retained explicitly. The unit of this pair is the stated corner projection, not the ambient unit.

  1. lemma OAI.WeakPureInfiniteness.partialIsometrySwap_commutes line 20
  2. lemma OAI.WeakPureInfiniteness.partialIsometryCompletion_commutes line 26
  3. lemma OAI.WeakPureInfiniteness.exists_zero_corner_cuntz_pair line 39
  4. lemma OAI.WeakPureInfiniteness.zeroCornerCompletion_commutes line 174

    Source documentation

    The zero-corner completion is a fixed finite polynomial, so it retains exact commutation with every element commuting with the three input isometries and their adjoints.

    lemma zeroCornerCompletion_commutes (r₀ r₁ r₂ y : E)
    (h₀ : Commute r₀ y) (h₀s : Commute (star r₀) y)
    (h₁ : Commute r₁ y) (h₁s : Commute (star r₁) y)
    (h₂ : Commute r₂ y) (h₂s : Commute (star r₂) y) :
    Commute (partialIsometryCompletion r₂ (r₀ * star r₀)
      (((r₀ * star r₀) + r₁ * (1 - r₀ * star r₀)) * star r₀)) y := by
…

    Mentions: OAI.WeakPureInfiniteness.partialIsometryCompletion

  5. structure OAI.WeakPureInfiniteness.ZeroCornerControl line 191
  6. lemma OAI.WeakPureInfiniteness.zeroCornerControl_one line 196
  7. lemma OAI.WeakPureInfiniteness.zeroCornerControl_star line 199
  8. lemma OAI.WeakPureInfiniteness.zeroCornerControl_add line 204
  9. lemma OAI.WeakPureInfiniteness.zeroCornerControl_sub line 219
  10. lemma OAI.WeakPureInfiniteness.zeroCornerControl_mul_bound line 234
  11. lemma OAI.WeakPureInfiniteness.zeroCornerControl_mul line 251
  12. lemma OAI.WeakPureInfiniteness.zeroCornerControl_swap line 264
  13. lemma OAI.WeakPureInfiniteness.zeroCornerCompletion_commutator_bound line 277

    Source documentation

    A uniform polynomial estimate, valid before the Cuntz relations are used. The deliberately coarse constant keeps the input tolerance independent of the test element and of the ambient algebra.

    lemma zeroCornerCompletion_commutator_bound [Nontrivial E] (r₀ r₁ r₂ x : E) (δ : ℝ)
    (hN : ∀ r ∈ ({r₀, r₁, r₂} : Set E), ‖r‖ ≤ 1)
    (hC : ∀ r ∈ ({r₀, r₁, r₂} : Set E),
      ‖r * x - x * r‖ ≤ δ ∧ ‖star r * x - x * star r‖ ≤ δ) :
    let U := partialIsometryCompletion r₂ (r₀ * star r₀)
…

    Mentions: OAI.WeakPureInfiniteness.partialIsometryCompletion

  14. lemma OAI.WeakPureInfiniteness.zeroCornerPair_commutator_bound line 302
  15. lemma OAI.WeakPureInfiniteness.zeroCorner_star_commutator_norm line 329
  16. lemma OAI.WeakPureInfiniteness.exists_approximately_central_zero_corner_pair line 338

    Source documentation

    Global central rows produce a coisometric pair in their complementary corner with arbitrarily small finite-set commutators. The corner unit is kept explicit in the conclusion.

    lemma exists_approximately_central_zero_corner_pair [Nontrivial E] (s t : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hc : ∀ i j, Commute (s i) (t j) ∧ Commute (s i) (star (t j)))
    (n : ℕ) (δ : ℝ) (hδ : 0 < δ) :
    ∃ (q a b : E), q ≠ 0 ∧ star q = q ∧ q * q = q ∧
      star a * a = q ∧ star b * b = q ∧ star a * b = 0 ∧
      a * star a + b * star b = q ∧
      (∀ i < n, ‖a * s i - s i * a‖ < δ ∧ ‖b * s i - s i * b‖ < δ ∧
        ‖a * star (s i) - star (s i) * a‖ < δ ∧
        ‖b * star (s i) - star (s i) * b‖ < δ) ∧
      ∀ k, Commute a (t k) ∧ Commute b (t k) ∧
        Commute a (star (t k)) ∧ Commute b (star (t k)) := by
…