OAI/Combinatorics/Progressions/Estimates/LowerRefilteredCyclicExpansion.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_positive_reconstruction line 13
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_native_positive_reconstruction line 83
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_immersion_local_inverse line 152
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_positive_frozen_observable line 234
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_frozen_reconstruction line 332
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_refiltered_reconstruction line 423
7. def OAI.Erdos3.RationalFilteredNilmanifold.RefilteredRecoveryFamily line 509
8. theorem OAI.Erdos3.RationalFilteredNilmanifold.RefilteredRecoveryFamily.mono line 548
9. def OAI.Erdos3.RationalFilteredNilmanifold.LowerRefilteredRecoveryFamily line 586
10. theorem OAI.Erdos3.RationalFilteredNilmanifold.LowerRefilteredRecoveryFamily.mono_cost line 629
11. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_refilteredRecoveryFamily line 651
12. def OAI.Erdos3.RationalFilteredNilmanifold.LowerRefilteredCyclicExpansionSpec line 708
13. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_lower_refiltered_cyclic_expansion line 797