OAI/Combinatorics/Progressions/Fourier/UniformScaledRetainedCharacters.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.unscale_grid_interval line 12
  2. theorem OAI.Erdos3.rationalGridMajorSet_rational line 21
  3. theorem OAI.Erdos3.rationalGridMajorBox_character line 36
  4. def OAI.Erdos3.lengthAwareSpectrumCover line 68
  5. theorem OAI.Erdos3.lengthAwareSpectrumCover_card line 73
  6. theorem OAI.Erdos3.lengthAwareSpectrumCover_accuracy line 88
  7. theorem OAI.Erdos3.exists_lengthAwareSpectrum_accuracy line 122
  8. theorem OAI.Erdos3.rationalGridMajorBox_scaled_character line 153
  9. theorem OAI.Erdos3.lengthAwarePolynomialGrid_character line 177
  10. def OAI.Erdos3.localizedMajorArcBudget line 222
  11. def OAI.Erdos3.localizedMajorArcLengthBudget line 225
  12. def OAI.Erdos3.localizedMajorArcErrorBudget line 229
  13. theorem OAI.Erdos3.localizedMajorArcBudget_pos line 233
  14. theorem OAI.Erdos3.localizationLengthBudget_threshold_eq line 245
  15. theorem OAI.Erdos3.localizedMajorArcBudget_eq_power line 250
  16. theorem OAI.Erdos3.localizedMajorArcLengthBudget_eq line 260
  17. theorem OAI.Erdos3.localizedMajorArcErrorBudget_eq line 266
  18. def OAI.Erdos3.majorArcBiasExponent line 282
  19. def OAI.Erdos3.majorArcBiasConstant line 284
  20. def OAI.Erdos3.majorArcLocalizationConstant line 288
  21. def OAI.Erdos3.majorArcLengthExponent line 291
  22. def OAI.Erdos3.majorArcLengthConstant line 293
  23. def OAI.Erdos3.majorArcErrorExponent line 296
  24. def OAI.Erdos3.majorArcErrorConstant line 298
  25. theorem OAI.Erdos3.majorArcBiasConstant_pos line 301
  26. theorem OAI.Erdos3.majorArcLocalizationConstant_pos line 307
  27. theorem OAI.Erdos3.majorArcLengthConstant_pos line 313
  28. theorem OAI.Erdos3.majorArcErrorConstant_pos line 320
  29. theorem OAI.Erdos3.localizedMajorArcBudget_constant line 327
  30. theorem OAI.Erdos3.localizedMajorArcLengthBudget_le_power line 332
  31. theorem OAI.Erdos3.localizedMajorArcErrorBudget_constant line 354
  32. def OAI.Erdos3.majorArcCoverExponent line 372
  33. def OAI.Erdos3.majorArcCoverConstant line 375
  34. def OAI.Erdos3.majorArcSpectrumExponent line 378
  35. def OAI.Erdos3.majorArcSpectrumConstant line 380
  36. theorem OAI.Erdos3.majorArcCoverConstant_one_le line 383
  37. theorem OAI.Erdos3.majorArcSpectrumConstant_nonneg line 392
  38. theorem OAI.Erdos3.majorArc_denominator_le_cover line 397
  39. theorem OAI.Erdos3.majorArc_scaled_error_le_cover line 412
  40. theorem OAI.Erdos3.uniformMajorArcCover_card line 433
  41. def OAI.Erdos3.uniformSpectrumBlockCount line 451
  42. def OAI.Erdos3.uniformBlockSpectrumCover line 454
  43. def OAI.Erdos3.uniformBlockSpectrumCardBudget line 460
  44. def OAI.Erdos3.uniformBlockSpectrumAccuracyConstant line 464
  45. theorem OAI.Erdos3.uniformBlockSpectrumCover_card line 468
  46. theorem OAI.Erdos3.uniformBlockSpectrum_tail line 479
  47. theorem OAI.Erdos3.exists_uniformBlockSpectrum_level line 504
  48. theorem OAI.Erdos3.polynomialGridCover_character line 520
  49. theorem OAI.Erdos3.fullGrid_rational_character line 539
  50. def OAI.Erdos3.uniformCharacterDenominatorBound line 555
  51. theorem OAI.Erdos3.uniformBlockSpectrumCover_character line 559
  52. theorem OAI.Erdos3.grid_character_rescale line 593
  53. def OAI.Erdos3.uniformScaledRetainedFrequencyBound line 615
  54. def OAI.Erdos3.uniformScaledRetainedDenominatorBound line 618
  55. theorem OAI.Erdos3.uniformScaledRetainedFrequencyBound_nonneg line 622
  56. theorem OAI.Erdos3.uniformScaledRetainedDenominatorBound_one_le line 625
  57. theorem OAI.Erdos3.uniformBlockSpectrumCover_scaled_character line 631
  58. theorem OAI.Erdos3.uniformBlockSpectrumCover_modes line 643