OAI/Analysis/OInfinity/IncompleteCocycle.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The actual unitary cocycle of an incomplete Cuntz row

The unitary-group endomorphism is u ↦ 1 - φ(1) + φ(u). This retains the defect projection of the canonical finite row. Its connected cocycles satisfy the exact generator recursion and an exact terminal-support formula; the terminal projection is not assigned a small norm.

  1. lemma OAI.WeakPureInfiniteness.bergCornerLift_one line 20
  2. lemma OAI.WeakPureInfiniteness.bergCornerLift_mul line 24
  3. lemma OAI.WeakPureInfiniteness.bergCornerLift_star line 37
  4. def OAI.WeakPureInfiniteness.incompleteUnitaryShift line 41
  5. lemma OAI.WeakPureInfiniteness.incompleteUnitaryShift_coe line 49
  6. lemma OAI.WeakPureInfiniteness.incompleteUnitaryShift_continuous line 52
  7. lemma OAI.WeakPureInfiniteness.bergCornerIterHom_one_eq_tail line 58
  8. lemma OAI.WeakPureInfiniteness.incompleteUnitaryShift_iterate_coe line 64
  9. lemma OAI.WeakPureInfiniteness.incompleteUnitaryShift_iterate_deviation line 73
  10. lemma OAI.WeakPureInfiniteness.finiteGroupCocycle_succ_right line 83
  11. lemma OAI.WeakPureInfiniteness.incompleteCocycle_difference_tail line 93
  12. lemma OAI.WeakPureInfiniteness.finiteGroupCocycle_one line 105
  13. lemma OAI.WeakPureInfiniteness.finiteGroupCocycle_continuous line 111
  14. lemma OAI.WeakPureInfiniteness.incompleteCocycle_joined line 117
  15. lemma OAI.WeakPureInfiniteness.incompleteCocycle_generator line 131
  16. lemma OAI.WeakPureInfiniteness.incompleteCocycle_generator_error line 139
  17. lemma OAI.WeakPureInfiniteness.incompleteCocycle_generator_error_tail line 147
  18. def OAI.WeakPureInfiniteness.canonicalRowCorner line 158
  19. def OAI.WeakPureInfiniteness.canonicalIncompleteCocycle line 163
  20. lemma OAI.WeakPureInfiniteness.exists_connected_canonicalIncompleteCocycle line 172

    Source documentation

    The canonical finite rows have an actual connected unitary cocycle with the exact tail-supported generator defect. This is not yet a small-error half-flip: the displayed difference on the terminal tail remains to be cancelled by the two-family construction.

    lemma exists_connected_canonicalIncompleteCocycle [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 : ∀ i j, Commute (star (t i)) (s j)) (N : ℕ) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
      (∀ n, Joined (1 : unitary E) (canonicalIncompleteCocycle s hs N u n)) ∧
      (∀ n i, i < N →
        (canonicalIncompleteCocycle s hs N u (n + 1) : E) * s i =
          t i * (canonicalIncompleteCocycle s hs N u n : E)) ∧
      (∀ n i, i < N →
        ((canonicalIncompleteCocycle s hs N u (n + 1) : E) * s i -
          t i * (canonicalIncompleteCocycle s hs N u (n + 1) : E)) *
…

    Mentions: OAI.WeakPureInfiniteness.canonicalIncompleteCocycle