OAI/Combinatorics/Progressions/Estimates/NativeNilcharacterTranslationEquivalence.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.coordinateProduct line 17
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.coordinateProduct_norm line 20
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.coordinateProduct_lipschitz line 25
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.coordinateProduct_invariant line 33
5. def OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.productNiltest line 48
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.productNiltest_complexity line 57
7. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.exists_lower_product_family line 81
8. def OAI.Erdos3.NativeNilsequenceExpansion.ofNiltest line 157
9. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.exists_self_equivalence_budget line 173
10. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_self_equivalence_budget line 229
11. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.exists_translation_equivalence_budget line 269
12. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_translation_equivalence_budget line 341