OAI/Combinatorics/Progressions/Sampling/RationalForecastGridTail.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.rationalOutputDensity line 14
  2. theorem OAI.Erdos3.rationalOutputDensity_nonneg line 19
  3. theorem OAI.Erdos3.rationalOutputDensity_test line 25
  4. theorem OAI.Erdos3.rationalOutputDensity_divisor_test line 46
  5. theorem OAI.Erdos3.rationalOutputDensity_fourier line 56
  6. def OAI.Erdos3.rationalInactiveForecast line 65
  7. theorem OAI.Erdos3.rationalInactiveForecast_nonneg line 72
  8. theorem OAI.Erdos3.rationalInactiveForecast_divisor_test line 81
  9. theorem OAI.Erdos3.rationalOutputDensity_complexMean_one line 109
  10. theorem OAI.Erdos3.rationalInactiveForecast_complexMass_one line 115
  11. theorem OAI.Erdos3.rationalOutputDensity_le_modulus_pow line 136
  12. theorem OAI.Erdos3.rationalInactiveForecast_le_grid_mass_modulus_pow line 152
  13. theorem OAI.Erdos3.rationalInactiveForecast_le_exp_of_grid_modulus line 173
  14. def OAI.Erdos3.integerResidueTuple line 202
  15. theorem OAI.Erdos3.integerResidueTuple_surjective line 208
  16. theorem OAI.Erdos3.rationalOutputDensity_order_bounds line 214
  17. theorem OAI.Erdos3.rationalInactiveForecast_cap line 239
  18. theorem OAI.Erdos3.rationalInactiveForecast_order_truncation line 263
  19. theorem OAI.Erdos3.rationalOutput_gridTest_integrable line 334
  20. theorem OAI.Erdos3.rationalOutput_partial_grid_integrable line 348
  21. theorem OAI.Erdos3.rationalOutput_partial_reference_integrable line 370
  22. theorem OAI.Erdos3.rationalOutput_partial_reference_integral line 381
  23. theorem OAI.Erdos3.rationalOutput_partial_grid_sub_reference_integral line 398
  24. theorem OAI.Erdos3.rationalInactiveForecast_order_truncation_separated line 432
  25. theorem OAI.Erdos3.rationalInactiveForecast_retained_approximation line 484
  26. theorem OAI.Erdos3.compactGrid_summable line 516
  27. theorem OAI.Erdos3.compactGrid_weighted_summable line 524
  28. def OAI.Erdos3.rationalOutputOrderTail line 536
  29. theorem OAI.Erdos3.rationalOutputOrderTail_norm_le line 543
  30. theorem OAI.Erdos3.rationalOutputOrderTail_weighted_norm_le line 552
  31. theorem OAI.Erdos3.rationalOutputOrderTail_weighted_tsum_le line 570
  32. theorem OAI.Erdos3.rationalOutputOrderTail_grid_le line 584
  33. theorem OAI.Erdos3.rationalOutputOrderTail_integral_le line 605
  34. theorem OAI.Erdos3.rationalOutputOrderTail_normalized_grid_le line 624
  35. theorem OAI.Erdos3.rationalOutputOrderTail_mean_integral_le line 644
  36. theorem OAI.Erdos3.rationalOutputOrderTail_grid_difference line 672