OAI/Combinatorics/Progressions/Estimates/PrescribedInvariantUnit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.sqrt_complement_lipschitz line 14
2. theorem OAI.Erdos3.exists_complex_unit_completion line 35
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_prescribed_scalar line 116
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_unit_vertical_family line 149
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_prescribed_unit line 226
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_unit_vertical_completion line 325
7. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_canonical_prescribed_unit_with_budget line 409
8. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_prescribed_invariant_unit line 441