OAI/Combinatorics/Progressions/Estimates/NativeTwoVariableSplitFreezing.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NativeTwoVariableSplit.first_eval_eq line 17
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_controlled_basepoint_normalization line 44
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_controlled_group_normalization line 88
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_controlled_multidegree_basepoint_normalization line 126
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_normalized_common_correlators line 174
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_controlled_frozen_niltest line 241
7. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.freezingExponent line 331
8. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.freezingExponent_ge_two line 334
9. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.freezingExponent_control line 337
10. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_freezing_niltest line 388
11. theorem OAI.Erdos3.NativeTwoVariableSplit.exists_second_expansion_budget line 434