OAI/Analysis/BoundedHochschild/UnitaryLifts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Unitary lifts and coordinate realizations of free path moments.

  1. lemma OAI.HochschildUnitaryLift.norm_sub_one_lt_two line 30
  2. lemma OAI.HochschildUnitaryLift.exists_symmetry_cut line 43
  3. theorem OAI.HochschildUnitaryLift.exists_three_exponentials line 102
  4. theorem OAI.HochschildUltrapower.exists_unitary_lift line 148
  5. theorem OAI.HochschildUltrapower.exists_unitary_coordinates line 163
  6. theorem OAI.HochschildPaths.simultaneous_paths_of_free_unitaries line 195