OAI/Analysis/TracialSplitting/Diagonalization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentMain.exists_coordinate_split line 21
  2. lemma OAI.CurrentMain.projection_of_bounded_sequence line 84
  3. lemma OAI.CurrentMain.commute_of_null_sequence line 99
  4. lemma OAI.CurrentMain.halftrace_of_null_sequence line 110
  5. theorem OAI.CurrentMain.diagonalize_finite_splittings line 126
  6. lemma OAI.CurrentMain.linearMap_zero_of_dense_unitaries line 189
  7. lemma OAI.CurrentMain.splitting_of_dense_unitaries line 209
  8. lemma OAI.CurrentMain.commutator_twoNorm_bound line 245
  9. lemma OAI.CurrentMain.coefficient_half_error_bound line 257
  10. lemma OAI.CurrentMain.splitting_of_uniform_approximants line 276
  11. theorem OAI.CurrentMain.completion_central_splitting_of_finite_stages line 315