OAI/Probability/SignedSweeps/WordTensorBasis.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SignedSweeps.colorHilbert line 13
  2. def OAI.SignedSweeps.wordConsEquiv line 16
  3. def OAI.SignedSweeps.wordTensorBasis line 22
  4. lemma OAI.SignedSweeps.wordTensorBasis_zero line 28
  5. lemma OAI.SignedSweeps.wordTensorBasis_succ line 33
  6. def OAI.SignedSweeps.varyingWordTensor line 42
  7. lemma OAI.SignedSweeps.varyingWordTensor_const line 45
  8. lemma OAI.SignedSweeps.wordTensorBasis_matrix line 48
  9. def OAI.SignedSweeps.isometricConj line 80
  10. lemma OAI.SignedSweeps.isometricConj_apply line 84
  11. lemma OAI.SignedSweeps.isometricConj_eq_block line 88
  12. lemma OAI.SignedSweeps.isometricConj_positive line 94
  13. lemma OAI.SignedSweeps.isometricConj_mul line 100
  14. lemma OAI.SignedSweeps.isometricConj_norm line 106
  15. lemma OAI.SignedSweeps.orthonormal_matrix_conjugate line 134
  16. lemma OAI.SignedSweeps.matrix_orthonormal_coordinates line 148
  17. lemma OAI.SignedSweeps.varyingWordTensor_conjugate line 155
  18. lemma OAI.SignedSweeps.varyingWordTensor_positive line 165
  19. lemma OAI.SignedSweeps.varyingWordTensor_norm_sq_le line 173