OAI/Analysis/OInfinity/BergTower.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Finite orthogonal towers and their terminal corner

The layers of a nonunital corner endomorphism form an exact finite orthogonal partition together with the last tail projection. For a Cuntz row, multiplication by each generator shifts these layers. The tail remains explicit throughout; there is no assertion that its norm becomes small as the height grows.

  1. def OAI.WeakPureInfiniteness.bergTowerTail line 22

    Source documentation

    The range projection of the nth iterate of the corner map.

    def bergTowerTail (φ : E →⋆ₙₐ[ℂ] E) : ℕ → E
  | 0 => 1
  | n + 1 => φ (bergTowerTail φ n)
  2. lemma OAI.WeakPureInfiniteness.bergTowerTail_zero line 26
  3. lemma OAI.WeakPureInfiniteness.bergTowerTail_succ line 28
  4. lemma OAI.WeakPureInfiniteness.bergTowerTail_star line 31
  5. lemma OAI.WeakPureInfiniteness.bergTowerTail_mul_of_le line 37
  6. lemma OAI.WeakPureInfiniteness.bergTowerTail_mul_of_ge line 48
  7. def OAI.WeakPureInfiniteness.bergTowerLayer line 54

    Source documentation

    One orthogonal difference of successive range projections.

    def bergTowerLayer (φ : E →⋆ₙₐ[ℂ] E) (n : ℕ) : E :=
…
  8. lemma OAI.WeakPureInfiniteness.bergTowerLayer_star line 57
  9. lemma OAI.WeakPureInfiniteness.bergTowerLayer_sq line 61
  10. lemma OAI.WeakPureInfiniteness.bergTowerLayer_mul_tail line 71
  11. lemma OAI.WeakPureInfiniteness.bergTowerTail_mul_layer line 77
  12. lemma OAI.WeakPureInfiniteness.bergTowerLayer_mul_of_lt line 82
  13. lemma OAI.WeakPureInfiniteness.bergTowerLayer_mul_of_ne line 89
  14. lemma OAI.WeakPureInfiniteness.bergTower_finite_partition line 97

    Source documentation

    The final tail is part of the exact partition; it is not discarded.

    lemma bergTower_finite_partition (φ : E →⋆ₙₐ[ℂ] E) (N : ℕ) :
    (∑ n ∈ Finset.range N, bergTowerLayer φ n) + bergTowerTail φ N = 1 := by
…

    Mentions: OAI.WeakPureInfiniteness.bergTowerLayer, OAI.WeakPureInfiniteness.bergTowerTail

  15. lemma OAI.WeakPureInfiniteness.bergTowerLayer_map line 107
  16. lemma OAI.WeakPureInfiniteness.bergTowerTail_succ_mul_generator line 116

    Source documentation

    A row generator shifts the tail projection by one level.

    lemma bergTowerTail_succ_mul_generator (s : I → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0) (n : ℕ) (i : I) :
    bergTowerTail (finiteCuntzDiagonalHom s hs) (n + 1) * s i =
      s i * bergTowerTail (finiteCuntzDiagonalHom s hs) n := by
…

    Mentions: OAI.WeakPureInfiniteness.bergTowerTail, OAI.WeakPureInfiniteness.finiteCuntzDiagonalHom

  17. lemma OAI.WeakPureInfiniteness.bergTowerLayer_succ_mul_generator line 124

    Source documentation

    The finite layers satisfy exact covariance away from the terminal corner.

    lemma bergTowerLayer_succ_mul_generator (s : I → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0) (n : ℕ) (i : I) :
    bergTowerLayer (finiteCuntzDiagonalHom s hs) (n + 1) * s i =
      s i * bergTowerLayer (finiteCuntzDiagonalHom s hs) n := by
…

    Mentions: OAI.WeakPureInfiniteness.bergTowerLayer, OAI.WeakPureInfiniteness.finiteCuntzDiagonalHom

  18. lemma OAI.WeakPureInfiniteness.bergTowerLayer_zero_mul_generator line 131
  19. lemma OAI.WeakPureInfiniteness.bergTransfer_star_mul line 138

    Source documentation

    Mixed Gram identities retain the coefficient in the corner map.

    lemma bergTransfer_star_mul (s t : I → 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) (x y : E) :
    star (finiteCuntzTransfer s t x) * finiteCuntzTransfer s t y =
      finiteCuntzDiagonalHom s hs (star x * y) := by
…

    Mentions: OAI.WeakPureInfiniteness.finiteCuntzTransfer, OAI.WeakPureInfiniteness.finiteCuntzDiagonalHom

  20. lemma OAI.WeakPureInfiniteness.bergTransfer_mul_star line 159
  21. lemma OAI.WeakPureInfiniteness.bergTransferIter_layer_source line 168

    Source documentation

    Iteration transfers an initial layer exactly to the corresponding layer.

    lemma bergTransferIter_layer_source (s t : I → 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)
    (x : E) (hx : star x * x = bergTowerLayer (finiteCuntzDiagonalHom s hs) 0)
    (n : ℕ) :
    star (finiteCuntzTransferIter s t n x) * finiteCuntzTransferIter s t n x =
      bergTowerLayer (finiteCuntzDiagonalHom s hs) n := by
…

    Mentions: OAI.WeakPureInfiniteness.bergTowerLayer, OAI.WeakPureInfiniteness.finiteCuntzDiagonalHom, OAI.WeakPureInfiniteness.finiteCuntzTransferIter

  22. lemma OAI.WeakPureInfiniteness.bergTransferIter_layer_target line 181
  23. lemma OAI.WeakPureInfiniteness.bergTransferIter_tail_source line 195

    Source documentation

    A unitary coefficient fills the whole last tail, not just a dense part.

    lemma bergTransferIter_tail_source (s t : I → 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)
    (x : unitary E) (n : ℕ) :
    star (finiteCuntzTransferIter s t n (x : E)) *
      finiteCuntzTransferIter s t n (x : E) =
      bergTowerTail (finiteCuntzDiagonalHom s hs) n := by
…

    Mentions: OAI.WeakPureInfiniteness.finiteCuntzTransferIter, OAI.WeakPureInfiniteness.bergTowerTail, OAI.WeakPureInfiniteness.finiteCuntzDiagonalHom

  24. lemma OAI.WeakPureInfiniteness.bergTransferIter_tail_target line 208
  25. def OAI.WeakPureInfiniteness.bergBottomCoefficient line 222

    Source documentation

    The bottom coefficient determined by an exact row extension.

    def bergBottomCoefficient (s t : I → E) (v : unitary E) : E :=
…
  26. lemma OAI.WeakPureInfiniteness.bergRowExtension_star line 226
  27. lemma OAI.WeakPureInfiniteness.bergBottom_mul_generator line 234
  28. lemma OAI.WeakPureInfiniteness.bergBottom_star_generator_mul line 241
  29. lemma OAI.WeakPureInfiniteness.bergExtension_star_transfer line 250
  30. lemma OAI.WeakPureInfiniteness.bergExtension_transfer_star line 258
  31. lemma OAI.WeakPureInfiniteness.bergBottom_source line 265
  32. lemma OAI.WeakPureInfiniteness.bergBottom_target line 283
  33. lemma OAI.WeakPureInfiniteness.bergBottom_add_transfer_mem_unitary line 302

    Source documentation

    Filling the complementary bottom corner makes one transfer step unitary.

    lemma bergBottom_add_transfer_mem_unitary (s t : I → 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)
    (v : unitary E) (hv : ∀ i, (v : E) * s i = t i)
    (x : E) (hx : x ∈ unitary E) :
    bergBottomCoefficient s t v + finiteCuntzTransfer s t x ∈ unitary E := by
…

    Mentions: OAI.WeakPureInfiniteness.bergBottomCoefficient, OAI.WeakPureInfiniteness.finiteCuntzTransfer

  34. def OAI.WeakPureInfiniteness.bergFiniteTower line 342

    Source documentation

    A finite tower is assembled with its entire terminal transfer coefficient.

    def bergFiniteTower (s t : I → E) (v : unitary E) : ℕ → E → E
  | 0, x => x
  | n + 1, x => bergBottomCoefficient s t v +
      finiteCuntzTransfer s t (bergFiniteTower s t v n x)

omit [DecidableEq I] in

    Mentions: OAI.WeakPureInfiniteness.bergBottomCoefficient, OAI.WeakPureInfiniteness.finiteCuntzTransfer

  35. lemma OAI.WeakPureInfiniteness.bergFiniteTower_zero line 348
  36. lemma OAI.WeakPureInfiniteness.bergFiniteTower_succ line 352
  37. lemma OAI.WeakPureInfiniteness.bergFiniteTower_mem_unitary line 357

    Source documentation

    Every finite assembled tower is a genuine unitary, including its last corner.

    lemma bergFiniteTower_mem_unitary (s t : I → 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)
    (v : unitary E) (hv : ∀ i, (v : E) * s i = t i)
    (n : ℕ) (x : E) (hx : x ∈ unitary E) :
    bergFiniteTower s t v n x ∈ unitary E := by
…

    Mentions: OAI.WeakPureInfiniteness.bergFiniteTower

  38. lemma OAI.WeakPureInfiniteness.bergFiniteTower_sub line 369

    Source documentation

    The terminal coefficient is the only varying term in two towers with the same bottom.

    lemma bergFiniteTower_sub (s t : I → E) (v : unitary E) (n : ℕ) (x y : E) :
    bergFiniteTower s t v n x - bergFiniteTower s t v n y =
      finiteCuntzTransferIter s t n (x - y) := by
…

    Mentions: OAI.WeakPureInfiniteness.bergFiniteTower, OAI.WeakPureInfiniteness.finiteCuntzTransferIter

  39. lemma OAI.WeakPureInfiniteness.bergFiniteTower_sub_norm_le line 378
  40. lemma OAI.WeakPureInfiniteness.bergFiniteTower_continuous line 387
  41. lemma OAI.WeakPureInfiniteness.bergFiniteTower_intertwining line 394
  42. lemma OAI.WeakPureInfiniteness.bergFiniteTower_residual line 402