OAI/Analysis/KadisonKastler/RestrictionGap.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The ordinary gap decreases under a common reducing restriction

Exact contraction lifts through the two restriction homomorphisms avoid any faithfulness assumption and lose no radius in the gap estimate.

  1. theorem OAI.KadisonKastler.starAlgebraBall_hausdorffEDist_ne_top line 23
  2. theorem OAI.KadisonKastler.exists_restriction_ball_approx line 30
  3. theorem OAI.KadisonKastler.restriction_gap_le line 55

    Source documentation

    Restriction can have a kernel on either algebra. It still decreases the distance of their closed unit balls.

    theorem restriction_gap_le
    (hAc : IsClosed (A : Set (H →L[ℂ] H)))
    (hBc : IsClosed (B : Set (H →L[ℂ] H))) :
    Metric.hausdorffDist (starAlgebraBall (reducingRestriction K A hA).range)
      (starAlgebraBall (reducingRestriction K B hB).range) ≤
      Metric.hausdorffDist (starAlgebraBall A) (starAlgebraBall B) := by
…

    Mentions: OAI.KadisonKastler.starAlgebraBall, OAI.KadisonKastler.reducingRestriction