OAI/Combinatorics/Progressions/Geometry/MultidegreeCoordinateFreezing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.retainedCoordinateWeight line 13
2. def OAI.Erdos3.freezeCoordinates line 15
3. def OAI.Erdos3.freezingPolynomial line 18
4. theorem OAI.Erdos3.freezingPolynomial_support line 22
5. theorem OAI.Erdos3.freezingPolynomial_eval line 31
6. theorem OAI.Erdos3.retainedCoordinate_degree line 36
7. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_normalized_frozen_orbit line 47
8. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_frozen_orbit line 70