OAI/Analysis/KadisonKastler/StateOrbitNorm.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Vector norms on approximate state-central orbit hulls

Approximate invariance of the reference state controls the vector norm of every conjugate. Weak lower semicontinuity extends the estimate to the closed convex hull; its asymptotic core cannot increase vector norm.

  1. theorem OAI.KadisonKastler.stateConjugate_vector_norm_sq_le line 21
  2. theorem OAI.KadisonKastler.wotVectorSquaredBall_convex line 45
  3. theorem OAI.KadisonKastler.stateOrbitHull_vector_norm_sq_le line 59
  4. theorem OAI.KadisonKastler.stateOrbitCore_vector_norm_sq_le line 73