FiniteRowIsometry.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

A finite isometry from a coisometric row to an incomplete row

The finite sum consists of all words of length at most m with an unused isometry inserted between the source and target words. The recursion makes its normalization and compression identities explicit. The target unit q may be a proper corner; no commutation between the two rows is required.

def OAI.WeakPureInfiniteness.finiteRowWordSum line 21
Source documentation
The unnormalized sum ∑ |μ|≤m, s_μ r t_μ*.
```
def finiteRowWordSum (s t : I → E) (r q : E) : ℕ → E
  | 0 => r * q
  | m + 1 => r * q + finiteCuntzTransfer t s (finiteRowWordSum s t r q m)
```
Mentions: OAI.WeakPureInfiniteness.finiteCuntzTransfer
lemma OAI.WeakPureInfiniteness.rowTransfer_star_mul line 25
lemma OAI.WeakPureInfiniteness.rowRoot_star_transfer line 44
lemma OAI.WeakPureInfiniteness.rowSum_step_inner line 54
lemma OAI.WeakPureInfiniteness.rowTarget_scalar line 74

lemma OAI.WeakPureInfiniteness.finiteRowWordSum_inner line 80

Source documentation

Equal-depth and consecutive-depth inner products have the same value.

lemma finiteRowWordSum_inner (s t : I → E) (r q : E)
    (hq : q * q = q) (hqs : star q = q) (hrr : star r * r = 1)
    (hr : ∀ i, star r * s i = 0)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (htq : ∀ i, t i * q = t i) (ht : ∑ i, t i * star (t i) = q) (m : ℕ) :
    star (finiteRowWordSum s t r q m) * finiteRowWordSum s t r q m =
        ((m : ℂ) + 1) • q ∧
      star (finiteRowWordSum s t r q m) * finiteRowWordSum s t r q (m + 1) =
        ((m : ℂ) + 1) • q := by
…

Mentions: OAI.WeakPureInfiniteness.finiteRowWordSum

lemma OAI.WeakPureInfiniteness.finiteRowWordSum_star_generator line 116
lemma OAI.WeakPureInfiniteness.finiteRowWordSum_compression line 132
lemma OAI.WeakPureInfiniteness.finiteRowWordSum_range_compression line 152
def OAI.WeakPureInfiniteness.finiteRowIsometry line 183
Source documentation
The normalized finite sum.
```
def finiteRowIsometry (s t : I → E) (r q : E) (m : ℕ) : E :=
…
```
lemma OAI.WeakPureInfiniteness.finiteRowScale_square line 186
lemma OAI.WeakPureInfiniteness.finiteRowIsometry_gram line 193
lemma OAI.WeakPureInfiniteness.finiteRowIsometry_compression line 206
lemma OAI.WeakPureInfiniteness.finiteRowIsometry_range_compression line 220