OAI/Combinatorics/MatchingPSD/PolynomialSpaces.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MatchingSmoothing.MatchingSpace line 8
2. def OAI.MatchingSmoothing.matchingEquiv line 10
3. def OAI.MatchingSmoothing.polynomialSpace line 14
4. def OAI.MatchingSmoothing.relabelIso line 17
5. lemma OAI.MatchingSmoothing.matchingEquiv_relabel line 20
6. lemma OAI.MatchingSmoothing.relabelIso_symm line 23
7. lemma OAI.MatchingSmoothing.polynomialSpace_invariant line 28
8. lemma OAI.MatchingSmoothing.highSpace_invariant line 33
9. lemma OAI.MatchingSmoothing.euclidean_high_degree_dimension line 41
10. lemma OAI.MatchingSmoothing.matching_compression_multiplicity line 66
11. lemma OAI.MatchingSmoothing.symmetric_matching_smoothing line 93