OAI/Combinatorics/Progressions/Polynomial/TranslationPhaseQuotient.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.weightedSupportLE_moduleFinite line 18
  2. theorem OAI.Erdos3.exponentSum_le_positive_weight line 25
  3. theorem OAI.Erdos3.weightedSupportLE_finrank_le line 30
  4. def OAI.Erdos3.translationPhaseArgument line 53
  5. theorem OAI.Erdos3.translationPhaseArgument_mul line 57
  6. theorem OAI.Erdos3.eval_integer_polynomial_real line 68
  7. theorem OAI.Erdos3.translationPhaseArgument_integer_character line 76
  8. theorem OAI.Erdos3.translationPhaseArgument_majorSymbol line 93
  9. theorem OAI.Erdos3.translationPhaseArgument_fourier_integer line 105
  10. def OAI.Erdos3.translationPhaseFunction line 119
  11. theorem OAI.Erdos3.translationPhaseFunction_integer_lattice line 123
  12. theorem OAI.Erdos3.translationPhaseFunction_norm line 137
  13. theorem OAI.Erdos3.translationPhaseFunction_central line 141
  14. theorem OAI.Erdos3.translationPhaseFunction_on_chart line 155
  15. theorem OAI.Erdos3.translationPhaseFunction_polynomial_input line 166
  16. theorem OAI.Erdos3.real_grid_polynomial_residue_difference line 189
  17. theorem OAI.Erdos3.real_fourierChar_add_integer line 211
  18. theorem OAI.Erdos3.real_fourierChar_sub_star line 220
  19. def OAI.Erdos3.residueAffinePolynomial line 227
  20. theorem OAI.Erdos3.residueAffinePolynomial_eval line 231
  21. theorem OAI.Erdos3.residueAffinePolynomial_totalDegree_le line 243
  22. def OAI.Erdos3.localMajorLowerPhase line 255
  23. theorem OAI.Erdos3.localMajorLowerPhase_totalDegree_le line 259
  24. theorem OAI.Erdos3.localMajorLowerPhase_cancellation line 264
  25. theorem OAI.Erdos3.localMajorPhaseCorrelation line 284
  26. def OAI.Erdos3.floorIntegerPolynomial line 328
  27. theorem OAI.Erdos3.floorIntegerPolynomial_coeff line 331
  28. def OAI.Erdos3.fractionalCoefficientPolynomial line 334
  29. theorem OAI.Erdos3.fractionalCoefficientPolynomial_coeff line 337
  30. theorem OAI.Erdos3.fractionalCoefficientPolynomial_bounds line 343
  31. theorem OAI.Erdos3.floorIntegerPolynomial_isWeightedHomogeneous line 349
  32. theorem OAI.Erdos3.fractionalCoefficientPolynomial_isWeightedHomogeneous line 358
  33. theorem OAI.Erdos3.fractionalCoefficientPolynomial_mass_le_card line 367
  34. theorem OAI.Erdos3.fractionalCoefficientPolynomial_mass_le line 379
  35. theorem OAI.Erdos3.floorIntegerPolynomial_add_fractionalCoefficientPolynomial line 391
  36. theorem OAI.Erdos3.fractionalCoefficientPolynomial_fourierChar line 396
  37. theorem OAI.Erdos3.fractionalCoefficientPolynomial_integer_substitution line 409
  38. theorem OAI.Erdos3.fractionalCoefficientPolynomial_integer_leading_component line 421
  39. theorem OAI.Erdos3.exists_major_polynomial_coefficient_reduction line 437
  40. theorem OAI.Erdos3.translationPhaseArgument_left_increment line 464
  41. theorem OAI.Erdos3.translationPhaseArgument_left_increment_bound line 476
  42. def OAI.Erdos3.integerPolynomialTranslationSubgroup line 514
  43. theorem OAI.Erdos3.translationPhaseFunction_integerSubgroup line 518
  44. def OAI.Erdos3.translationQuotientPhase line 525
  45. theorem OAI.Erdos3.translationQuotientPhase_mk line 532
  46. theorem OAI.Erdos3.translationQuotientPhase_norm line 536
  47. theorem OAI.Erdos3.translationPhaseFunction_cover line 542