OAI/Analysis/KadisonKastler/ProjectionReflectionOrbit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A reflection exchanges projection defects for vector distance

At the sum of two vectors the defect is the error term; at their difference it is the improvement term. This is the quantitative step for state orbits.

  1. theorem OAI.KadisonKastler.selfAdjoint_unitary_distance_identity line 21
  2. def OAI.KadisonKastler.projectionOrbitReflection line 40
  3. theorem OAI.KadisonKastler.projectionOrbitReflection_star line 50
  4. theorem OAI.KadisonKastler.projectionOrbitReflection_defect line 56
  5. theorem OAI.KadisonKastler.projectionOrbitReflection_distance line 67