OAI/Analysis/KadisonKastler/CStarCommutatorClosure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Spatial commutator bounds pass to the represented bicommutant

Spectral clipping lifts each represented contraction to an actual source contraction. Kaplansky density then passes its commutator bound to the unit ball of the represented von Neumann closure.

  1. theorem OAI.KadisonKastler.exists_source_contraction line 23
  2. theorem OAI.KadisonKastler.commutator_bound_generated_contraction line 31