TracialCornerEstimate.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A small-corner commutator estimate supplies the actual bounded rectangular derivation used in the full-column argument.

def OAI.KadisonSimilarity.TracialCornerGeometry.cornerRestriction line 24
Source documentation
Compression of the ambient operator to the actual domain and output corners. The domain may have a smaller right support.
```
def cornerRestriction (Y : H →L[ℂ] H) : G.corner e r →L[ℂ] G.corner e 1 :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerRestriction_commutator line 28
theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_cornerRestriction_commutator_le line 43
Source documentation
The rectangular derivation has norm at most the original small-corner constant. Orthogonal domain/output compression introduces no dimension factor.
```
theorem norm_cornerRestriction_commutator_le (Y : H →L[ℂ] H) {ε : ℝ} (hε : 0 ≤ ε)
    (hY : ∀ a : CStarCorner e he, ‖commutator Y (G.left (a : P))‖ ≤ ε * ‖a‖) :
    ‖cornerCommutator (G.cornerRepresentation e he 1) (G.cornerRepresentation e he r)
      (G.cornerRestriction e r Y)‖ ≤ ε := by
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.cornerCommutator

theorem OAI.KadisonSimilarity.TracialCornerGeometry.exists_corrected_corner line 64

Source documentation

The corrected corner intertwiner is obtained with the paper's constant from projection comparison and the exact published cyclic inputs.

theorem exists_corrected_corner
    (τ : P → ℝ) (comparison : FiniteFactorProjectionComparison τ)
    (hr : IsStarProjection r) (hτ : τ r ≤ τ e)
    (Y : H →L[ℂ] H) {ε : ℝ} (hε : 0 ≤ ε)
    (hY : ∀ a : CStarCorner e he, ‖commutator Y (G.left (a : P))‖ ≤ ε * ‖a‖)
    (published : PublishedDerivationInputs.{u,v} (CStarCorner e he)) :
    ∃ T : G.corner e r →L[ℂ] G.corner e 1,
      (∀ a : CStarCorner e he, T.comp (G.cornerRepresentation e he r a) =
        (G.cornerRepresentation e he 1 a).comp T) ∧
      ‖G.cornerRestriction e r Y - T‖ ≤ (1 + 4 * (4 * Real.sqrt 2)) ^ 2 * ε := by
…

Mentions: OAI.KadisonSimilarity.FiniteFactorProjectionComparison, OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.commutator