OAI/Combinatorics/Progressions/Fourier/FixedPrincipalCoefficientSpectrum.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.weightedPositiveModerateGridCoefficient_mem_polynomial line 12
  2. theorem OAI.Erdos3.weightedPositiveModerateGridCoefficient_minor_polynomial line 100
  3. def OAI.Erdos3.positiveModerateSpectrumExponent line 129
  4. def OAI.Erdos3.positiveModerateSpectrumConstant line 132
  5. def OAI.Erdos3.positiveModerateSpectrumBlockCount line 135
  6. def OAI.Erdos3.positiveModerateSpectrumCover line 138
  7. theorem OAI.Erdos3.positiveModerateSpectrumCover_card line 144
  8. theorem OAI.Erdos3.exists_positiveModerateSpectrum_level line 159
  9. theorem OAI.Erdos3.positiveModerateSpectrum_tail line 172
  10. theorem OAI.Erdos3.weightedPositiveModerate_uniform_spectrum_tail line 200
  11. theorem OAI.Erdos3.weightedPositiveAffineModerate_uniform_spectrum_tail line 242
  12. def OAI.Erdos3.positiveModerateAccuracyScale line 287
  13. def OAI.Erdos3.positiveModerateRetainedBias line 291
  14. theorem OAI.Erdos3.positiveModerateAccuracyScale_one_le line 294
  15. theorem OAI.Erdos3.positiveModerateRetainedBias_spec line 304
  16. def OAI.Erdos3.positiveModerateSpectrumCardBudget line 325
  17. theorem OAI.Erdos3.positiveModerateSpectrumCover_card_budget line 331
  18. theorem OAI.Erdos3.positiveModerateSpectrum_absolute_cap line 342
  19. theorem OAI.Erdos3.weightedPositiveModerateSpectrum_absolute_cap line 357
  20. theorem OAI.Erdos3.weightedAffineModerateGridCoefficient_norm_le_one line 387
  21. theorem OAI.Erdos3.weightedPositiveAffineModerateSpectrum_absolute_cap line 398
  22. def OAI.Erdos3.positiveRetainedFrequencyBound line 438
  23. def OAI.Erdos3.positiveRetainedDenominatorBound line 441
  24. theorem OAI.Erdos3.positiveRetainedFrequencyBound_nonneg line 445
  25. theorem OAI.Erdos3.positiveRetainedDenominatorBound_one_le line 448
  26. theorem OAI.Erdos3.positiveModerateSpectrumCover_character line 454
  27. theorem OAI.Erdos3.positiveModerateSpectrumCover_modes line 466
  28. theorem OAI.Erdos3.positiveCoefficientSource_toNat_spec line 499
  29. theorem OAI.Erdos3.positiveCoefficientSource_fixed_mixture line 510
  30. theorem OAI.Erdos3.principalNormalizedSource_fixed_mixture line 526
  31. theorem OAI.Erdos3.positiveCoefficientSource_fixed_primitive line 539
  32. theorem OAI.Erdos3.positiveCoefficientSource_fixed_scale line 548
  33. theorem OAI.Erdos3.fixedPositiveCoefficientSource_gridCoefficient line 569
  34. theorem OAI.Erdos3.fixedPositiveCoefficientSource_uniform_spectrum_tail line 585