OAI/Combinatorics/Progressions/Estimates/SlicedPrincipalInverse.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.principalSliceValue_contDiff line 14
2. def OAI.Erdos3.principalSliceSlope line 19
3. theorem OAI.Erdos3.principalSliceValue_fderiv_single line 24
4. theorem OAI.Erdos3.principalSliceSlope_lower line 52
5. theorem OAI.Erdos3.scalar_identity_inverse_abs_bound line 85
6. def OAI.Erdos3.principalSliceSingleton line 108
7. theorem OAI.Erdos3.principalSliceSingleton_contDiff line 112
8. theorem OAI.Erdos3.principalSliceSingleton_selectedDerivative line 116
9. theorem OAI.Erdos3.principalSliceSingleton_inverse_bound line 137
10. def OAI.Erdos3.jointSlicedPrincipal line 155
11. def OAI.Erdos3.jointSlicedInjection line 159
12. theorem OAI.Erdos3.jointSlicedInjection_norm_le line 162
13. theorem OAI.Erdos3.jointSlicedPrincipal_contDiff line 168
14. theorem OAI.Erdos3.jointSlicedPrincipal_inverse_bound line 173
15. theorem OAI.Erdos3.jointSlicedPrincipal_perturbed_inverse line 186