OAI/Analysis/KadisonKastler/PositiveOrbitContraction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform contraction in the orbit of positive unit vectors

  1. theorem OAI.KadisonKastler.normalized_defect_norm line 21
  2. theorem OAI.KadisonKastler.positive_orbit_distance_contraction line 31