OAI/Analysis/KadisonKastler/SmallContractionUnitaryAverage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Small contractions as four-unitary averages

The half unit ball of a unital C-star algebra lies in the convex hull of its unitaries. The explicit four-term formula is enough for the spatial derivation argument; no unitary density theorem is required.

  1. theorem OAI.KadisonKastler.exists_four_unitaries_average line 21
  2. theorem OAI.KadisonKastler.map_small_contraction_mem_convex line 54
  3. theorem OAI.KadisonKastler.mul_small_contractions_mem_convex line 65