OAI/Combinatorics/Progressions/Polynomial/RealComparisonPolynomialProjections.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.MultidegreeLieFiltration.realComparisonLog line 16
2. theorem OAI.Erdos3.MultidegreeLieFiltration.realComparisonLog_coefficient line 20
3. theorem OAI.Erdos3.MultidegreeLieFiltration.realComparisonLog_adapted line 33
4. theorem OAI.Erdos3.MultidegreeLieFiltration.realComparisonLog_eval line 40
5. theorem OAI.Erdos3.MultidegreeLieFiltration.realComparisonLog_first line 59
6. theorem OAI.Erdos3.MultidegreeLieFiltration.realComparisonLog_first_eval line 68
7. theorem OAI.Erdos3.MultidegreeLieFiltration.realComparisonLog_second_ambient line 75
8. theorem OAI.Erdos3.MultidegreeLieFiltration.realComparisonLog_second_eval line 84