OAI/Probability/SignedSweeps/HilbertBlocks.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.isometric_adjoint_apply line 13
  2. lemma OAI.SignedSweeps.isometric_adjoint_comp line 20
  3. def OAI.SignedSweeps.hilbertBlock line 25
  4. lemma OAI.SignedSweeps.hilbertBlock_apply line 30
  5. lemma OAI.SignedSweeps.hilbertBlock_on line 33
  6. lemma OAI.SignedSweeps.hilbertBlock_mul line 37
  7. lemma OAI.SignedSweeps.hilbertBlock_adjoint line 42
  8. lemma OAI.SignedSweeps.hilbertBlock_positive line 48
  9. lemma OAI.SignedSweeps.hilbertBlock_symmetric line 51
  10. lemma OAI.SignedSweeps.hilbertBlock_idempotent line 54
  11. lemma OAI.SignedSweeps.hilbertBlock_trace line 58
  12. lemma OAI.SignedSweeps.hilbertBlock_orthogonal line 64
  13. lemma OAI.SignedSweeps.euclideanEmbedding_adjoint line 85
  14. lemma OAI.SignedSweeps.euclideanEmbedding_orthogonal line 95
  15. lemma OAI.SignedSweeps.euclideanTensorEquiv_single line 106