IncompleteTails.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Two-sided terminal corners of the incomplete-row cocycle

The actual cocycle transports every completed source layer to its target layer. Its remaining generator error lies from the source terminal corner to the next target terminal corner. Neither corner is discarded in norm.

lemma OAI.WeakPureInfiniteness.bergCornerLift_mul_image line 19
lemma OAI.WeakPureInfiniteness.bergCornerLift_image_mul_star line 24
lemma OAI.WeakPureInfiniteness.bergCornerLift_sandwich_image line 30
lemma OAI.WeakPureInfiniteness.incompleteCocycle_conjugate_iterate line 43
Source documentation
The outer k steps transport a whole iterated corner, retaining the initial n-step cocycle inside that corner.
```
lemma incompleteCocycle_conjugate_iterate (n k : ℕ) (x : E) :
    (finiteGroupCocycle (G := unitary E) (incompleteUnitaryShift φ) u (n + k) : E) *
…
```
Mentions: OAI.WeakPureInfiniteness.finiteGroupCocycle, OAI.WeakPureInfiniteness.incompleteUnitaryShift
lemma OAI.WeakPureInfiniteness.incompleteCocycle_tail_conjugate line 73
lemma OAI.WeakPureInfiniteness.incompleteCocycle_tail_transport line 83
lemma OAI.WeakPureInfiniteness.incompleteCocycle_layer_transport line 93
lemma OAI.WeakPureInfiniteness.incompleteCocycle_difference_both_tails line 107
Source documentation
The successive cocycle difference is a rectangular operator from the source terminal projection to the target terminal projection.
```
lemma incompleteCocycle_difference_both_tails (n : ℕ) :
    bergTowerTail ψ n *
      ((finiteGroupCocycle (G := unitary E) (incompleteUnitaryShift φ) u n : E) -
…
```
Mentions: OAI.WeakPureInfiniteness.bergTowerTail, OAI.WeakPureInfiniteness.finiteGroupCocycle, OAI.WeakPureInfiniteness.incompleteUnitaryShift
lemma OAI.WeakPureInfiniteness.incompleteRow_conjugate_corner line 135
lemma OAI.WeakPureInfiniteness.incompleteRow_difference_target_tail line 149
lemma OAI.WeakPureInfiniteness.incompleteRow_generator_error_both_tails line 166
Source documentation
The precise two-family boundary: source depth n, target depth n+1.
```
lemma incompleteRow_generator_error_both_tails (n : ℕ) (i : I) :
    bergTowerTail (finiteCuntzDiagonalHom t ht) (n + 1) *
      ((finiteGroupCocycle (G := unitary E) (incompleteUnitaryShift
…
```
Mentions: OAI.WeakPureInfiniteness.bergTowerTail, OAI.WeakPureInfiniteness.finiteCuntzDiagonalHom, OAI.WeakPureInfiniteness.finiteGroupCocycle, OAI.WeakPureInfiniteness.incompleteUnitaryShift