ToeplitzCompression.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Finite Toeplitz rows compressed by an almost central projection

These are the quantitative estimates in the projection-splitting step for a finite row of canonical O∞ isometries. In addition to almost centrality, a coisometric compression needs small compression of the original vacuum projection. No projection with these properties is assumed to exist here.

def OAI.WeakPureInfiniteness.toeplitzRowCompression line 21
Source documentation
Compression in the ambient algebra, with relative unit q.
```
def toeplitzRowCompression (q : E) (s : I → E) (i : I) : E := q * s i * q
```
def OAI.WeakPureInfiniteness.toeplitzRowVacuum line 24
Source documentation
The defect of the finite isometry row before compression.
```
def toeplitzRowVacuum (s : I → E) : E := 1 - ∑ i, s i * star (s i)
```
lemma OAI.WeakPureInfiniteness.compression_projection_norm line 26
lemma OAI.WeakPureInfiniteness.compression_contract_mul_left line 30
lemma OAI.WeakPureInfiniteness.compression_contract_mul_right line 34

lemma OAI.WeakPureInfiniteness.toeplitz_star_commutator_norm line 39

Source documentation

The adjoint has the same commutator error.

lemma toeplitz_star_commutator_norm (q x : E) (hqs : star q = q) :
    ‖q * star x - star x * q‖ = ‖q * x - x * q‖ := by
…

lemma OAI.WeakPureInfiniteness.toeplitzRowCompression_gram line 48

Source documentation

Exact defect formula for the compressed Gram matrix.

lemma toeplitzRowCompression_gram (q : E) (s : I → E)
    (hq : q * q = q) (hqs : star q = q)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0) (i j : I) :
    star (toeplitzRowCompression q s i) * toeplitzRowCompression q s j -
        (if i = j then q else 0) =
      q * star (s i) * (q * s j - s j * q) * q := by
…

Mentions: OAI.WeakPureInfiniteness.toeplitzRowCompression

lemma OAI.WeakPureInfiniteness.toeplitzRowCompression_gram_bound line 66

Source documentation

Every Gram entry is controlled by one generator commutator.

lemma toeplitzRowCompression_gram_bound (q : E) (s : I → E)
    (hq : q * q = q) (hqs : star q = q)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hns : ∀ i, ‖s i‖ ≤ 1) (δ : ℝ)
    (hcomm : ∀ i, ‖q * s i - s i * q‖ ≤ δ) (i j : I) :
    ‖star (toeplitzRowCompression q s i) * toeplitzRowCompression q s j -
        (if i = j then q else 0)‖ ≤ δ := by
…

Mentions: OAI.WeakPureInfiniteness.toeplitzRowCompression

lemma OAI.WeakPureInfiniteness.toeplitzRowCompression_coisometry line 87

Source documentation

The coisometry defect contains the compressed original vacuum explicitly.

lemma toeplitzRowCompression_coisometry (q : E) (s : I → E)
    (hq : q * q = q) (hqs : star q = q) :
    (∑ i, toeplitzRowCompression q s i * star (toeplitzRowCompression q s i)) - q =
      (∑ i, q * s i * (q * star (s i) - star (s i) * q) * q) -
        q * toeplitzRowVacuum s * q := by
…

Mentions: OAI.WeakPureInfiniteness.toeplitzRowCompression, OAI.WeakPureInfiniteness.toeplitzRowVacuum

lemma OAI.WeakPureInfiniteness.toeplitzRowCompression_coisometry_bound line 109

Source documentation

Approximate centrality and small vacuum compression give the finite coisometry estimate used before perturbing a Toeplitz row to a Cuntz row.

lemma toeplitzRowCompression_coisometry_bound (q : E) (s : I → E)
    (hq : q * q = q) (hqs : star q = q) (hns : ∀ i, ‖s i‖ ≤ 1)
    (δ : ℝ) (hcomm : ∀ i, ‖q * s i - s i * q‖ ≤ δ) :
    ‖(∑ i, toeplitzRowCompression q s i * star (toeplitzRowCompression q s i)) - q‖ ≤
      (Fintype.card I : ℝ) * δ + ‖q * toeplitzRowVacuum s * q‖ := by
…

Mentions: OAI.WeakPureInfiniteness.toeplitzRowCompression, OAI.WeakPureInfiniteness.toeplitzRowVacuum

lemma OAI.WeakPureInfiniteness.toeplitz_complementary_compression_bound line 137
Source documentation
The two relative compressions recover each generator up to twice its commutator error. No smallness is asserted for either complementary projection.
```
lemma toeplitz_complementary_compression_bound (q x : E)
    (hq : q * q = q) (hqs : star q = q) :
    ‖q * x * q + (1 - q) * x * (1 - q) - x‖ ≤ 2 * ‖q * x - x * q‖ := by
…
```