TracialSmallCornerTransfer.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

A small-corner commutator estimate transports along a partial isometry in the algebra commuting with the implementing operator. Projection comparison then supplies that partial isometry in the prescribed factor.

theorem OAI.KadisonSimilarity.norm_le_one_of_initial_projection line 18
Source documentation
A partial isometry is contractive, including when its initial projection is zero.
```
theorem norm_le_one_of_initial_projection (v f : P) (hf : IsStarProjection f)
    (hv : star v * v = f) : ‖v‖ ≤ 1 := by
…
```
theorem OAI.KadisonSimilarity.mul_eq_self_of_final_projection line 28
Source documentation
The final support condition and the initial projection identity imply that the partial isometry lands in the requested corner.
```
theorem mul_eq_self_of_final_projection (e f v : P) (hf : IsStarProjection f)
    (hv : star v * v = f) (hev : e * (v * star v) = v * star v) : e * v = v := by
…
```

def OAI.KadisonSimilarity.partialIsometryCornerMap line 39

Source documentation

Conjugation by the partial isometry is an actual ambient corner element.

def partialIsometryCornerMap (e f : P) (he : IsStarProjection e) (hf : IsStarProjection f)
    (v : P) (hv : star v * v = f) (hev : e * (v * star v) = v * star v)
    (z : CStarCorner f hf) : CStarCorner e he :=
…

Mentions: OAI.KadisonSimilarity.CStarCorner

theorem OAI.KadisonSimilarity.partialIsometryCornerMap_recover line 51

Source documentation

The original corner element is recovered exactly.

theorem partialIsometryCornerMap_recover (e f : P)
    (he : IsStarProjection e) (hf : IsStarProjection f)
    (v : P) (hv : star v * v = f) (hev : e * (v * star v) = v * star v)
    (z : CStarCorner f hf) :
    star v * (partialIsometryCornerMap e f he hf v hv hev z : P) * v = z := by
…

Mentions: OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.partialIsometryCornerMap

theorem OAI.KadisonSimilarity.norm_partialIsometryCornerMap_le line 61

theorem OAI.KadisonSimilarity.corner_commutator_bound_of_partial_isometry line 77

Source documentation

Algebraic transport, before using any projection comparison theorem.

theorem corner_commutator_bound_of_partial_isometry
    (L : P →⋆ₐ[ℂ] (H →L[ℂ] H)) (T : H →L[ℂ] H)
    (e f : P) (he : IsStarProjection e) (hf : IsStarProjection f)
    (v : P) (hv : star v * v = f) (hev : e * (v * star v) = v * star v)
    (hTv : T * L v = L v * T) (hTvs : T * L (star v) = L (star v) * T)
    {ε : ℝ} (hε : 0 ≤ ε)
    (hbound : ∀ x : CStarCorner e he, ‖commutator T (L (x : P))‖ ≤ ε * ‖x‖) :
    ∀ z : CStarCorner f hf, ‖commutator T (L (z : P))‖ ≤ ε * ‖z‖ := by
…

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

theorem OAI.KadisonSimilarity.corner_commutator_bound_of_hom_comparison line 116

Source documentation

Projection comparison can be performed in a separate included factor; the resulting partial isometry is then mapped into the represented algebra.

theorem corner_commutator_bound_of_hom_comparison
    {A : Type*} [CStarAlgebra A] (φ : A →⋆ₐ[ℂ] P)
    (L : P →⋆ₐ[ℂ] (H →L[ℂ] H))
    (τ : A → ℝ) (comparison : FiniteFactorProjectionComparison τ)
    (e f : A) (he : IsStarProjection e) (hf : IsStarProjection f)
    (htrace : τ f ≤ τ e) (T : H →L[ℂ] H)
    (hcomm : ∀ a : A, T * L (φ a) = L (φ a) * T)
    {ε : ℝ} (hε : 0 ≤ ε)
    (hbound : ∀ z : CStarCorner (φ e) (he.map φ),
      ‖commutator T (L (z : P))‖ ≤ ε * ‖z‖) :
    ∀ z : CStarCorner (φ f) (hf.map φ),
      ‖commutator T (L (z : P))‖ ≤ ε * ‖z‖ := by
…

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

theorem OAI.KadisonSimilarity.TracialCornerGeometry.small_corner_commutator_bound_of_comparison line 142

Source documentation

Finite-factor comparison is used in Q itself, ensuring that the implementing partial isometry belongs to the algebra commuting with T.

theorem small_corner_commutator_bound_of_comparison
    (τ : Q → ℝ) (comparison : FiniteFactorProjectionComparison τ)
    (e f : Q) (he : IsStarProjection (e : P)) (hf : IsStarProjection (f : P))
    (htrace : τ f ≤ τ e) (T : H →L[ℂ] H)
    (hTQ : ∀ a : Q, T.comp (G.left (a : P)) = (G.left (a : P)).comp T)
    {ε : ℝ} (hε : 0 ≤ ε)
    (hbound : ∀ x : CStarCorner (e : P) he,
      ‖commutator T (G.left (x : P))‖ ≤ ε * ‖x‖) :
    ∀ z : CStarCorner (f : P) hf,
      ‖commutator T (G.left (z : P))‖ ≤ ε * ‖z‖ := by
…

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