OAI/Analysis/KadisonKastler/ModulatedAlgebraGap.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Boundary algebra errors from the ordinary conjugacy gap

Scaling the unit-ball estimate supplies the exact boundary hypothesis used in analytic smoothing, in both directions of conjugation.

  1. theorem OAI.KadisonKastler.infDist_le_norm_mul_of_kkDistance_lt line 19
  2. theorem OAI.KadisonKastler.kkDistance_inverse_conjugate line 44
  3. theorem OAI.KadisonKastler.modulated_sandwich_eq line 53
  4. theorem OAI.KadisonKastler.infDist_modulated_sandwich_le line 60