OAI/Analysis/KadisonKastler/CommonCenterReduction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Removing the common-center premise

Center alignment reduces unrestricted separable stability to stability for algebras with a common center, with explicit tolerance estimates.

  1. def OAI.KadisonKastler.CommonCenterSeparableStability line 22

    Source documentation

    Strong stability for algebras with a common center, uniform over separable Hilbert-space representations.

    def CommonCenterSeparableStability : Prop :=
…
  2. theorem OAI.KadisonKastler.separableStrongStability_of_common_center line 29