OAI/Combinatorics/Progressions/Estimates/TwoDownsetPrecision.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.DownsetSplittingStatement line 12
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_multidegree_downset_splitting line 67
3. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.TwoDownsetSplittingStatement line 137
4. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.TwoDownsetCorrelationStatement line 191
5. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.TwoDownsetPrecisionStatement line 242
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_two_downset_splitting line 297
7. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_two_downset_correlation line 404
8. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_two_downset_precision line 480