OAI/Combinatorics/Progressions/Estimates/WeightedOrbitNormalization.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.eval_zero_eq_coefficient line 11
2. theorem OAI.Erdos3.NilpotentLieFiltration.horizontal_bch line 26
3. def OAI.Erdos3.NilpotentLieFiltration.horizontalLog line 37
4. theorem OAI.Erdos3.NilpotentLieFiltration.horizontalLog_mul line 39
5. theorem OAI.Erdos3.NilpotentLieFiltration.horizontalLog_inv line 42
6. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedShift_horizontal_zero line 45
7. theorem OAI.Erdos3.NilpotentLieFiltration.dilationPair_coefficients_mem line 75
8. def OAI.Erdos3.NilpotentLieFiltration.restrictDilationPairPolynomial line 87
9. theorem OAI.Erdos3.NilpotentLieFiltration.restrictDilationPairPolynomial_adapted line 95
10. theorem OAI.Erdos3.NilpotentLieFiltration.restrictDilationPairPolynomial_eval line 108
11. def OAI.Erdos3.NilpotentLieFiltration.restrictDilationPairOrbit line 117
12. theorem OAI.Erdos3.NilpotentLieFiltration.restrictDilationPairOrbit_eval line 125
13. theorem OAI.Erdos3.NilpotentLieFiltration.restrictDilationPairOrbit_zero line 134
14. theorem OAI.Erdos3.NilpotentLieFiltration.exists_dilationPairOrbit_of_coefficients line 147
15. def OAI.Erdos3.MultidegreeLieFiltration.weightedGroupInclusion line 173
16. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedGroupInclusion_injective line 177
17. def OAI.Erdos3.MultidegreeLieFiltration.weightedNormalizationLog line 181
18. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedNormalizationLog_adapted line 185
19. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedNormalizationLog_eval line 192
20. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedNormalizationLog_zero line 200
21. def OAI.Erdos3.MultidegreeLieFiltration.normalizedWeightedOrbit line 206
22. theorem OAI.Erdos3.MultidegreeLieFiltration.normalizedWeightedOrbit_eval line 213
23. theorem OAI.Erdos3.MultidegreeLieFiltration.normalizedWeightedOrbit_zero line 224