OAI/Combinatorics/Progressions/Nilpotent/AmbientBracketCorrectionPolynomials.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_controlled_bracket_corrections line 15
2. def OAI.Erdos3.bracketLiftMatrix line 66
3. theorem OAI.Erdos3.bracketSystemLift_coordinates line 69
4. theorem OAI.Erdos3.bracketSystemLift_norm_bound line 87
5. theorem OAI.Erdos3.bracketSystemLift_grid line 95
6. theorem OAI.Erdos3.exists_bracket_correction_polynomials line 117
7. theorem OAI.Erdos3.exists_ambient_bracket_correction_polynomials line 209