OAI/Combinatorics/Progressions/Nilpotent/NativeResidueNiltests.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.RationalTorus.residueObservable_lipschitz line 13
2. def OAI.Erdos3.RationalTorus.residueNiltest line 23
3. theorem OAI.Erdos3.RationalTorus.residueNiltest_unit_interval line 29
4. theorem OAI.Erdos3.RationalTorus.residueNiltest_complexity line 34
5. theorem OAI.Erdos3.RationalTorus.residueNiltest_evalCyclic line 48
6. theorem OAI.Erdos3.RationalTorus.sum_residueNiltest_evalCyclic line 59
7. theorem OAI.Erdos3.RationalTorus.residueNiltest_positive_iff line 65