OAI/Combinatorics/Progressions/Estimates/LipschitzExtensionAlongMap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_real_lipschitz_extension_interval line 15
2. theorem OAI.Erdos3.exists_complex_bounded_lipschitz_extension line 27
3. theorem OAI.Erdos3.exists_complex_extension_from_subset line 62
4. theorem OAI.Erdos3.complex_half_norm_le_one line 86
5. theorem OAI.Erdos3.lipschitz_complex_half line 91
6. theorem OAI.Erdos3.complex_prod_halves line 104
7. theorem OAI.Erdos3.exists_complex_extension_along_map line 120