OAI/Combinatorics/Progressions/Estimates/PrescribedPartitionExpansionCore.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.RationalFilteredNilmanifold.SelectedRefilteredProductExpansionSpec line 27
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.selected_refiltered_product_expansion line 124
3. def OAI.Erdos3.RationalFilteredNilmanifold.PrescribedPartitionExpansionSpec line 247
4. def OAI.Erdos3.RationalFilteredNilmanifold.PreparedHigherShiftContradictionSpec line 393
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.prescribed_partition_expansion_from_partition line 527