OAI/Analysis/BoundedHochschild/CentralLinearPatch.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Central spectral cuts and simultaneous linear norm control.

  1. lemma OAI.HochschildCentralQuantization.exists_central_norm_cut line 28
  2. theorem OAI.HochschildCentralQuantization.exists_unitary_central_linear_patch line 80