OAI/Combinatorics/Progressions/Sampling/AllocatedPeriodicGridQuadrature.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.translatedGridMass line 18
  2. theorem OAI.Erdos3.translatedGridMass_nonneg line 21
  3. theorem OAI.Erdos3.translatedGridMass_error line 26
  4. theorem OAI.Erdos3.translatedGridMass_le line 34
  5. theorem OAI.Erdos3.rationalInactiveForecast_zero_off_image line 54
  6. theorem OAI.Erdos3.rationalInactiveForecast_divisor_test_summable line 63
  7. theorem OAI.Erdos3.rationalInactiveForecast_divisor_tsum_test line 77
  8. theorem OAI.Erdos3.rationalInactivePolynomialForecast_tsum_marginal line 110
  9. theorem OAI.Erdos3.rationalInactiveForecast_divisor_tsum_test_norm_le line 134
  10. theorem OAI.Erdos3.rationalInactiveForecast_complexTsumMass_one line 151
  11. theorem OAI.Erdos3.periodicIntegerGrid_summable line 173
  12. theorem OAI.Erdos3.periodicIntegerGrid_complex_quadrature line 186
  13. theorem OAI.Erdos3.rationalInactiveForecast_complex_grid_quadrature line 236
  14. theorem OAI.Erdos3.retainedCharacter_complex_grid_quadrature line 282
  15. theorem OAI.Erdos3.periodicTranslatedIntegerGrid_summable line 315
  16. theorem OAI.Erdos3.periodicTranslatedIntegerGrid_complex_quadrature line 328
  17. theorem OAI.Erdos3.constantPhase_density_test_lipschitz line 378
  18. theorem OAI.Erdos3.retainedRationalCharacter_grid_quadrature line 397
  19. theorem OAI.Erdos3.retainedRationalOutput_grid_quadrature line 458
  20. theorem OAI.Erdos3.rationalOutput_translated_grid_comparison line 534
  21. theorem OAI.Erdos3.rationalOutput_partial_grid_comparison line 624
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveInteger_periodic_quadrature line 709
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveInteger_partial_periodic_quadrature line 727