TracialIncludedCorners.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Small-corner bounds from Q inside P pass to the included tracial ultrapower Q^ω inside P^ω. The strict trace gap is explicit.

theorem OAI.KadisonSimilarity.included_ultrapower_corner_bound line 26

Source documentation

The full small-corner transfer, including lifting inside the prescribed subalgebra, near-minimal quotient lifts, and Hilbert compression.

theorem included_ultrapower_corner_bound
    (rounding : SpectralProjectionRoundingInput τA)
    (T : τB.GNS →L[ℂ] τB.GNS) {ε s : ℝ} (hε : 0 ≤ ε)
    (hcorner : ∀ (q : A) (hq : IsStarProjection q), (τA q).re ≤ s →
      ∀ z : CStarCorner (φ q) (hq.map φ),
        ‖commutator T (τB.gnsStarAlgHom (z : B))‖ ≤ ε * ‖z‖)
    (e : Ultrapower τA hA ω trA) (he : IsStarProjection e)
    (hte : (quotientTrace τA hA ω trA e).re < s)
    (z : CStarCorner (Φ e) (he.map Φ)) :
    ‖commutator (tracialUltrapowerCompression τB hB ω trB T)
      ((quotientTrace τB hB ω trB).gnsStarAlgHom
        (z : Ultrapower τB hB ω trB))‖ ≤ ε * ‖z‖ := by
…

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