OAI/Combinatorics/Progressions/Polynomial/SchmidtShortDualVector.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.norm_linear_interval_sum line 16
  2. theorem OAI.Erdos3.linear_interval_inverse line 33
  3. theorem OAI.Erdos3.polynomial_linear_eval line 46
  4. theorem OAI.Erdos3.linear_polynomial_interval_inverse line 52
  5. theorem OAI.Erdos3.affine_comp_top_coeff line 71
  6. def OAI.Erdos3.affinePhaseRemainder line 85
  7. theorem OAI.Erdos3.affinePhaseRemainder_degree line 88
  8. theorem OAI.Erdos3.affinePhaseRemainder_eval line 100
  9. theorem OAI.Erdos3.affinePhaseRemainder_error line 110
  10. theorem OAI.Erdos3.polynomial_torus_degree_reduction line 130
  11. def OAI.Erdos3.polynomialShiftDifference line 157
  12. theorem OAI.Erdos3.polynomialShiftDifference_eval line 160
  13. theorem OAI.Erdos3.polynomialShiftDifference_degree line 164
  14. theorem OAI.Erdos3.affine_shift_next_coeff line 181
  15. theorem OAI.Erdos3.polynomialShiftDifference_top_coeff line 195
  16. def OAI.Erdos3.intervalPolynomialPhase line 212
  17. theorem OAI.Erdos3.intervalPolynomialPhase_support line 215
  18. theorem OAI.Erdos3.intervalPolynomialPhase_norm_le line 219
  19. theorem OAI.Erdos3.intervalPolynomialPhase_sum line 224
  20. theorem OAI.Erdos3.integerInterval_overlap line 231
  21. theorem OAI.Erdos3.intervalPolynomialPhase_correlation line 238
  22. theorem OAI.Erdos3.integerInterval_overlap_card_lower line 253
  23. theorem OAI.Erdos3.polynomial_weyl_step line 260
  24. theorem OAI.Erdos3.many_polynomial_weyl_shifts line 280
  25. theorem OAI.Erdos3.polynomial_translate_degree line 316
  26. theorem OAI.Erdos3.polynomial_translate_top_coeff line 320
  27. theorem OAI.Erdos3.polynomial_interval_sum_translate line 325
  28. theorem OAI.Erdos3.integerInterval_overlap_length line 336
  29. theorem OAI.Erdos3.integerInterval_overlap_card_le line 340
  30. theorem OAI.Erdos3.quadratic_weyl_many_multiples line 358
  31. def OAI.Erdos3.polynomialExponentialSum line 393
  32. def OAI.Erdos3.LeadingWeylBound line 396
  33. theorem OAI.Erdos3.leadingWeylBound_one line 402
  34. theorem OAI.Erdos3.LeadingWeylBound.on_integer_interval line 415
  35. theorem OAI.Erdos3.quadratic_weyl_inverse_with_denominator_scale line 439
  36. theorem OAI.Erdos3.quadratic_weyl_inverse line 489
  37. theorem OAI.Erdos3.LeadingWeylBound.step line 539
  38. theorem OAI.Erdos3.leadingWeylBound_all_degrees line 631
  39. theorem OAI.Erdos3.polynomial_weyl_inverse line 641
  40. theorem OAI.Erdos3.exists_reciprocal_bias_integer line 657
  41. theorem OAI.Erdos3.polynomial_weyl_inverse_power_bound line 672
  42. def OAI.Erdos3.PolynomialIntervalPowerBound line 720
  43. theorem OAI.Erdos3.polynomial_weyl_inverse_power_interval line 729
  44. theorem OAI.Erdos3.PolynomialIntervalPowerBound.monomial_character_mean line 752
  45. theorem OAI.Erdos3.PolynomialIntervalPowerBound.short_dual_vector line 797
  46. theorem OAI.Erdos3.schmidt_short_dual_vector line 824