ZeroCornerRows.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Finite Cuntz rows in the explicit complementary corner

Repeatedly splitting the first range of a relative Cuntz pair produces every finite row size. All ranges still sum to the same projection q; the complement 1 - q is retained. The commutator estimate grows only linearly with the number of splittings.

lemma OAI.WeakPureInfiniteness.relativeIsometry_mul_support line 21
Source documentation
Right support follows from the relative isometry equation.
```
lemma relativeIsometry_mul_support (a q : E) (ha : star a * a = q)
    (hqstar : star q = q) (hqq : q * q = q) : a * q = a := by
…
```
lemma OAI.WeakPureInfiniteness.relativeCuntzPair_support line 31
def OAI.WeakPureInfiniteness.zeroCornerRow line 45
Source documentation
At stage zero the row is the corner unit. Every successor replaces it by b followed by the old row multiplied on the left by a.
```
def zeroCornerRow (q a b : E) : (n : ℕ) → Fin (n + 1) → E
  | 0, _ => q
  | n + 1, i => Fin.cases b (fun j => a * zeroCornerRow q a b n j) i
```
lemma OAI.WeakPureInfiniteness.zeroCornerRow_support line 49
lemma OAI.WeakPureInfiniteness.zeroCornerRow_gram line 64
lemma OAI.WeakPureInfiniteness.zeroCornerRow_range_sum line 96
lemma OAI.WeakPureInfiniteness.zeroCornerRow_norm_le line 117
lemma OAI.WeakPureInfiniteness.row_product_commutator_le line 129

lemma OAI.WeakPureInfiniteness.zeroCornerRow_commutator_bound line 144

Source documentation

Each splitting costs at most one extra input commutator.

lemma zeroCornerRow_commutator_bound (q a b x : E) (δ γ : ℝ) (hδ : 0 ≤ δ) (hγ : 0 ≤ γ)
    (hq : ‖q‖ ≤ 1) (ha : ‖a‖ ≤ 1) (hb : ‖b‖ ≤ 1)
    (hqc : ‖q * x - x * q‖ ≤ γ) (hac : ‖a * x - x * a‖ ≤ δ)
    (hbc : ‖b * x - x * b‖ ≤ δ) :
    ∀ n i, ‖zeroCornerRow q a b n i * x - x * zeroCornerRow q a b n i‖ ≤
      (n : ℝ) * δ + γ := by
…

Mentions: OAI.WeakPureInfiniteness.zeroCornerRow

lemma OAI.WeakPureInfiniteness.zeroCornerRow_commutes line 166
lemma OAI.WeakPureInfiniteness.projection_norm_le_one line 177
lemma OAI.WeakPureInfiniteness.relativeIsometry_norm_le_one line 183
lemma OAI.WeakPureInfiniteness.row_star_commutator_norm line 189
lemma OAI.WeakPureInfiniteness.pair_projection_commutator_le line 195

lemma OAI.WeakPureInfiniteness.exists_approximately_central_finite_corner_row line 210

Source documentation

Every finite size occurs in a nonzero approximately central corner. Choosing m = 2*k+1 gives an even row of size 2*k+2.

lemma exists_approximately_central_finite_corner_row [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 m : ℕ) (δ : ℝ) (hδ : 0 < δ) :
    ∃ (q : E) (v : Fin (m + 1) → E),
      q ≠ 0 ∧ star q = q ∧ q * q = q ∧
      (∀ i j, star (v i) * v j = if i = j then q else 0) ∧
      (∑ i, v i * star (v i)) = q ∧
      (∀ i, q * v i = v i ∧ v i * q = v i) ∧
      (∀ i k, k < n → ‖v i * s k - s k * v i‖ < δ ∧
        ‖v i * star (s k) - star (s k) * v i‖ < δ) ∧
…