OAI/Analysis/KadisonKastler/CornerStateWeights.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Normalized corner states of faithful vector states

The weights of a proper nonzero projection lie strictly between zero and one. The two normalized compressions have norm at most one and reconstruct a state centralizing the projection with exactly those scalar weights.

  1. def OAI.KadisonKastler.projectionVectorWeight line 21
  2. def OAI.KadisonKastler.vectorCornerState line 23
  3. theorem OAI.KadisonKastler.cornerFunctional_vectorFunctional line 26
  4. theorem OAI.KadisonKastler.vectorFunctional_projection line 35
  5. theorem OAI.KadisonKastler.projectionVectorWeight_add_complement line 50
  6. theorem OAI.KadisonKastler.projectionVectorWeight_pos line 56
  7. theorem OAI.KadisonKastler.projectionVectorWeight_mem_Ioo line 67
  8. theorem OAI.KadisonKastler.vectorCornerState_norm_le line 78
  9. theorem OAI.KadisonKastler.weight_smul_vectorCornerState line 86
  10. theorem OAI.KadisonKastler.vectorFunctional_eq_weighted_corners line 91