OAI/Combinatorics/Progressions/Estimates/SelectedWindowIndicator.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.normalized_complex_point_error line 13
2. theorem OAI.Erdos3.finite_window_normalized_l1_error line 21
3. theorem OAI.Erdos3.finite_window_normalized_test_error line 35
4. theorem OAI.Erdos3.finite_window_weighted_integrable line 67
5. theorem OAI.Erdos3.finite_window_weighted_integral_error line 85
6. def OAI.Erdos3.selectedProductExtension line 121
7. theorem OAI.Erdos3.selectedProductExtension_error line 125
8. theorem OAI.Erdos3.selectedProductExtension_measurable line 163
9. theorem OAI.Erdos3.selectedWindow_volume_cancel line 173
10. theorem OAI.Erdos3.selectedProductExtension_windowIndicator line 191