OAI/Combinatorics/Progressions/Estimates/ReducedSymbolDimensions.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.quotientTopSymbolIndex_finite line 17
2. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSymbolIndex_finite line 23
3. theorem OAI.Erdos3.NilpotentLieFiltration.quotientTopSymbolIndex_card_le line 29
4. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSymbolIndex_card_le line 38
5. def OAI.Erdos3.NilpotentLieFiltration.reducedMatrixParameter line 51
6. theorem OAI.Erdos3.NilpotentLieFiltration.reducedMatrixParameter_nonneg line 54
7. theorem OAI.Erdos3.NilpotentLieFiltration.le_reducedMatrixParameter line 59
8. theorem OAI.Erdos3.NilpotentLieFiltration.reduced_lift_matrix_dimensions line 66