OAI/Analysis/Commutator/CyclicSpatialImplementation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Kadison.CyclicSpatial.represented_matrix_apply line 27
  2. lemma OAI.Kadison.CyclicSpatial.matrixRepresentation_injective line 32
  3. lemma OAI.Kadison.CyclicSpatial.matrixRepresentation_norm_eq line 44
  4. def OAI.Kadison.CyclicSpatial.delta line 58
  5. lemma OAI.Kadison.CyclicSpatial.delta_apply line 77
  6. lemma OAI.Kadison.CyclicSpatial.delta_derivation line 80
  7. lemma OAI.Kadison.CyclicSpatial.projection_tuple_norm_le line 89
  8. lemma OAI.Kadison.CyclicSpatial.extension_matrix_commutator line 97
  9. lemma OAI.Kadison.CyclicSpatial.extension_matrix_norm_bound line 112
  10. theorem OAI.Kadison.CyclicSpatial.extension_amplified_bound line 133
  11. lemma OAI.Kadison.CyclicSpatial.restriction_distance_bound line 161
  12. theorem OAI.Kadison.CyclicSpatial.exists_cyclic_intertwiner line 173