FreeCompression.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The three-block free-compression norm estimate

The reduced-word construction in lem:free-compression supplies a projection p with a zero fourth block, a small overlap with the corner e, and L² bounds on the two off-diagonal blocks. These bounds imply the compressed operator norm estimate.

theorem OAI.KadisonSimilarity.three_block_decomposition line 22
Source documentation
The creation, annihilation, and diagonal blocks exhaust an operator when its fourth block is zero.
```
theorem three_block_decomposition (p T : R) (hzero : (1 - p) * T * (1 - p) = 0) :
    T = p * T * (1 - p) + (1 - p) * T * p + p * T * p := by
…
```

theorem OAI.KadisonSimilarity.norm_free_compression_le line 30

Source documentation

Abstract form of the free-compression bound. The parameter b₂ is the tracial L² norm in the intended application.

theorem norm_free_compression_le (e p T : R) (hp : p * p = p)
    {u b₂ : ℝ} (hu : 0 ≤ u) (hb₂ : 0 ≤ b₂)
    (he : ‖e‖ ≤ 1) (hep : ‖e * p‖ ≤ Real.sqrt u) (hpe : ‖p * e‖ ≤ Real.sqrt u)
    (hzero : (1 - p) * T * (1 - p) = 0)
    (hcreate : ‖p * T * (1 - p)‖ ≤ b₂)
    (hannihilate : ‖(1 - p) * T * p‖ ≤ b₂) :
    ‖e * T * e‖ ≤ 2 * Real.sqrt u * b₂ + u * ‖T‖ := by
…

theorem OAI.KadisonSimilarity.norm_narrow_arc_compression_le line 93

Source documentation

For the narrow arc used in the paper, the compression has norm at most three times the corner trace.

theorem norm_narrow_arc_compression_le (e p T : R) (hp : p * p = p)
    {u b₂ : ℝ} (hu : 0 ≤ u) (hb₂ : 0 ≤ b₂)
    (he : ‖e‖ ≤ 1) (hep : ‖e * p‖ ≤ Real.sqrt u) (hpe : ‖p * e‖ ≤ Real.sqrt u)
    (hzero : (1 - p) * T * (1 - p) = 0)
    (hcreate : ‖p * T * (1 - p)‖ ≤ b₂)
    (hannihilate : ‖(1 - p) * T * p‖ ≤ b₂)
    (h₂ : b₂ ^ 2 ≤ u) (hnorm : ‖T‖ ≤ 1) : ‖e * T * e‖ ≤ 3 * u := by
…