OAI/Combinatorics/Progressions/Estimates/NativeSquareRecovery.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.recover_middle_coset_of_left_class line 10
2. theorem OAI.Erdos3.recover_mapped_middle_coset_of_left_class line 20
3. theorem OAI.Erdos3.bchSubgroup_inner_grid_of_reindex line 38
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_factorwise_covers line 51
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_factorwise_reconstruction_cover line 116
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_normalized_recovery line 171
7. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_left_class_recovery line 266
8. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_subgroup_recovery line 334
9. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_factorwise_subgroup_recovery line 463
10. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_square_recovery line 602