OAI/Analysis/FreeWords/TracialClipApprox.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KKUltraTrace.gnsVector_norm_sq line 16
  2. theorem OAI.KKUltraTrace.gnsVector_star_norm line 21
  3. theorem OAI.KKUltraTrace.gnsVector_mul_norm_left line 27
  4. theorem OAI.KKUltraTrace.gnsVector_mul_norm_right line 33
  5. theorem OAI.KKUltraTrace.clipWeight_excess_support line 40
  6. def OAI.KKUltraTrace.clipRemainderWeight line 47
  7. theorem OAI.KKUltraTrace.spectralClip_sub line 49
  8. theorem OAI.KKUltraTrace.norm_clipRemainderWeight_le line 55
  9. theorem OAI.KKUltraTrace.clipRemainder_norm_lower line 63
  10. theorem OAI.KKUltraTrace.tracial_clip_approximation line 88