OAI/Combinatorics/Progressions/Estimates/SelectedSingletonSmoothTestQuadrature.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.normalizedRealQuadrature_error line 12
2. theorem OAI.Erdos3.shiftedSmoothProductMass_pos_of_mesh line 31
3. theorem OAI.Erdos3.smoothProductProfile_test_lipschitz line 40
4. theorem OAI.Erdos3.smoothProductProfile_real_test_integral_norm_le line 50
5. theorem OAI.Erdos3.shiftedSmoothProductPMF_test_quadrature line 62
6. theorem OAI.Erdos3.smoothProductProfile_complex_test_integrable line 118
7. theorem OAI.Erdos3.shiftedSmoothProductPMF_complex_test_quadrature line 132
8. theorem OAI.Erdos3.selectedResidueSmoothPMF_singleton_complex_quadrature line 208