OAI/RepresentationTheory/PartialPermutation/HilbertSchmidt.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PartialPermutation.hsNormSq_eq_sum line 16
2. lemma OAI.PartialPermutation.hsNormSq_nonneg line 24
3. lemma OAI.PartialPermutation.hsNormSq_eq_matrix_norm_sq line 30
4. lemma OAI.PartialPermutation.hsNormSq_adjoint line 44
5. lemma OAI.PartialPermutation.hsNormSq_projection_left line 48
6. lemma OAI.PartialPermutation.adjoint_mul_eq line 54
7. lemma OAI.PartialPermutation.adjoint_projection_eq line 58
8. lemma OAI.PartialPermutation.hsNormSq_projection_right line 66
9. lemma OAI.PartialPermutation.hsNormSq_mul_le line 74
10. lemma OAI.PartialPermutation.hsNormSq_sum_le line 85