OAI/Combinatorics/Progressions/Estimates/MixedRootCyclicComparison.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedWrappedDiagonalCorrection line 13
2. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCyclicDiagonalCorrection line 20
3. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedWrappedDiagonalCorrection_mean_error line 28
4. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedCyclicDiagonalCorrection_mean_error line 72
5. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixedCyclicDiagonalCorrection_expansion line 114
6. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedRootCyclicCorrection line 213
7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedRootCyclicCorrection_mean_error line 217
8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixedRootCyclicCorrection_expansion line 237