OAI/Combinatorics/Progressions/Estimates/ExternalPhysicalMemberPivotMasks.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.RationalFilteredNilmanifold.externalNetNiltest line 17
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.externalNetNiltest_complexity line 27
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_external_net_ordinary_test_family line 44
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_controlled_vertical_operators line 79
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_external_physical_member_net line 175
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_external_physical_member_net_of_half line 187
7. theorem OAI.Erdos3.RationalFilteredNilmanifold.contractiveFamily_integer_error line 215
8. theorem OAI.Erdos3.RationalFilteredNilmanifold.contractiveFamily_real_error line 224
9. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_externalFamily_contractive_vertical_expansion line 233
10. theorem OAI.Erdos3.RationalFilteredNilmanifold.externalFamily_vertical_member_net line 295
11. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_external_physical_member_pivot_masks line 317