OAI/Combinatorics/MatchingPSD/EquivariantCompression.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingSmoothing.Pairing.act_pointwise_mul line 11
2. lemma OAI.MatchingSmoothing.Pairing.act_pointwise_one line 14
3. lemma OAI.MatchingSmoothing.Pairing.act_edgeCoord line 16
4. lemma OAI.MatchingSmoothing.Pairing.lowDegree_invariant line 24
5. def OAI.MatchingSmoothing.permIso line 52
6. lemma OAI.MatchingSmoothing.permIso_apply line 56
7. lemma OAI.MatchingSmoothing.matrix_equivariant line 59
8. lemma OAI.MatchingSmoothing.matrix_trace_square line 69
9. lemma OAI.MatchingSmoothing.invariant_map_eq line 82
10. lemma OAI.MatchingSmoothing.invariant_orthogonal line 92
11. lemma OAI.MatchingSmoothing.starProjection_equivariant line 100
12. lemma OAI.MatchingSmoothing.compression_eigenspace_invariant line 110