OAI/Combinatorics/Progressions/Estimates/StepOneSymbolLinearPart.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NilpotentLieFiltration.stepOneFrequencyKernel line 14
2. theorem OAI.Erdos3.NilpotentLieFiltration.mem_real_stepOneFrequencyKernel line 21
3. theorem OAI.Erdos3.NilpotentLieFiltration.exists_stepOne_linear_splitting line 26
4. theorem OAI.Erdos3.NilpotentLieFiltration.stepOne_basis_layers line 79
5. theorem OAI.Erdos3.NilpotentLieFiltration.stepOne_basis_weight line 91
6. def OAI.Erdos3.NilpotentLieFiltration.stepOneGradedEquiv line 96
7. theorem OAI.Erdos3.NilpotentLieFiltration.stepOneGradedEquiv_coordinate line 102
8. theorem OAI.Erdos3.NilpotentLieFiltration.stepOne_gradedPieceProjection line 109
9. theorem OAI.Erdos3.NilpotentLieFiltration.stepOne_graded_submodule line 120
10. theorem OAI.Erdos3.NilpotentLieFiltration.stepOne_symbol_linearPart line 150