OAI/Analysis/KadisonKastler/MinimalResidualFamily.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The convex family of minimum-distance spatial residuals

For a minimizing pair, the residuals with no larger norm form a convex set invariant under the unitaries of the commutant. Every member has exactly the minimum norm. A strict norm decrease inside this set is therefore impossible.

  1. def OAI.KadisonKastler.boundedSpatialResiduals line 20
  2. theorem OAI.KadisonKastler.boundedSpatialResiduals_convex line 24
  3. theorem OAI.KadisonKastler.boundedSpatialResiduals_conjugate line 54
  4. theorem OAI.KadisonKastler.boundedSpatialResiduals_norm_eq line 85