OAI/Analysis/KadisonKastler/InfinitesimalExponentiation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Exponentiating the infinitesimal normalizer estimate

  1. def OAI.KadisonKastler.separateUnitaryProducts line 16

    Source documentation

    Products of an algebra unitary and a commutant unitary.

    def separateUnitaryProducts (M : VonNeumannAlgebra H) : Set (H →L[ℂ] H) :=
…
  2. theorem OAI.KadisonKastler.one_mem_separateUnitaryProducts line 20
  3. theorem OAI.KadisonKastler.separateUnitaryProducts_mul line 24
  4. theorem OAI.KadisonKastler.separateUnitaryProducts_star line 38
  5. theorem OAI.KadisonKastler.conjugates_of_mem_separateUnitaryProducts line 48
  6. theorem OAI.KadisonKastler.infDist_separateUnitaryProducts_left line 56
  7. theorem OAI.KadisonKastler.infDist_unitaryConj_normalizer line 79
  8. theorem OAI.KadisonKastler.expUnitary_mem_vonNeumann line 87
  9. theorem OAI.KadisonKastler.expUnitary_mem_separateUnitaryProducts line 95
  10. theorem OAI.KadisonKastler.infDist_expUnitary_le_infDist_selfAdjointSum line 109