OAI/Combinatorics/Progressions/Polynomial/CRTPolynomialChargeBound.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.polynomialTranslate_add_apply line 20
  2. theorem OAI.Erdos3.polynomialTranslate_zero_apply line 30
  3. def OAI.Erdos3.polynomialDifference line 34
  4. theorem OAI.Erdos3.polynomialDifference_apply line 38
  5. theorem OAI.Erdos3.polynomialDifference_commute line 42
  6. theorem OAI.Erdos3.polynomialDifference_degree line 50
  7. theorem OAI.Erdos3.polynomialDifference_eval line 61
  8. theorem OAI.Erdos3.degree_le_one_eq_constant_add_row line 78
  9. theorem OAI.Erdos3.polynomialDifference_C line 94
  10. theorem OAI.Erdos3.polynomialDifference_row line 98
  11. theorem OAI.Erdos3.polynomialDifference_affine line 105
  12. theorem OAI.Erdos3.polynomialDifference_direction_add line 111
  13. theorem OAI.Erdos3.polynomialDifference_direction_smul line 117
  14. def OAI.Erdos3.polynomialIterDifference line 134
  15. theorem OAI.Erdos3.polynomialIterDifference_add line 139
  16. theorem OAI.Erdos3.polynomialIterDifference_smul line 149
  17. theorem OAI.Erdos3.polynomialIterDifference_commute line 158
  18. theorem OAI.Erdos3.polynomialIterDifference_degree line 168
  19. theorem OAI.Erdos3.polynomial_phase_difference_mean_sq_le line 182
  20. theorem OAI.Erdos3.polynomial_phase_iterDifference_bound line 202
  21. theorem OAI.Erdos3.affine_polynomial_phase_mean_zero line 225
  22. theorem OAI.Erdos3.norm_affine_polynomial_phase_mean line 252
  23. theorem OAI.Erdos3.polynomial_phase_bias_le_linearRow_probability line 264
  24. theorem OAI.Erdos3.totalDegree_sub_top_component_le line 276
  25. theorem OAI.Erdos3.polynomialIterDifference_linearRow_top_component line 298
  26. theorem OAI.Erdos3.polynomial_phase_bias_le_top_linearRow_probability line 325
  27. theorem OAI.Erdos3.zmod_polynomial_phase_bias_le_linearRow_probability line 336
  28. theorem OAI.Erdos3.zmod_polynomial_phase_decay_of_top_rank line 348
  29. theorem OAI.Erdos3.polynomialIterDifference_update_add line 382
  30. theorem OAI.Erdos3.polynomialIterDifference_update_smul line 403
  31. def OAI.Erdos3.polynomialIterDifferenceMultilinear line 423
  32. theorem OAI.Erdos3.polynomialIterDifferenceMultilinear_apply line 429
  33. def OAI.Erdos3.polynomialCommonScale line 443
  34. theorem OAI.Erdos3.polynomialCommonScale_monomial line 447
  35. theorem OAI.Erdos3.polynomialCommonScale_homogeneous line 456
  36. theorem OAI.Erdos3.polynomialCommonScale_homogeneousComponent line 468
  37. theorem OAI.Erdos3.polynomialTranslate_top_component line 482
  38. def OAI.Erdos3.polynomialAffineClass line 491
  39. theorem OAI.Erdos3.polynomialAffineClass_eval line 495
  40. theorem OAI.Erdos3.polynomialAffineClass_apply line 503
  41. theorem OAI.Erdos3.polynomialAffineClass_degree line 509
  42. theorem OAI.Erdos3.polynomialAffineClass_mul_eq_constant line 521
  43. theorem OAI.Erdos3.polynomialAffineClass_top_component line 540
  44. theorem OAI.Erdos3.polynomialAffineClass_phase_bias_bound line 547
  45. theorem OAI.Erdos3.polynomialIterDifference_eval line 567
  46. theorem OAI.Erdos3.polynomialIterDifference_topSymbol line 589
  47. theorem OAI.Erdos3.polynomialTranslate_map_coefficients line 607
  48. theorem OAI.Erdos3.polynomialDifference_map_coefficients line 617
  49. theorem OAI.Erdos3.polynomialIterDifference_map_coefficients line 623
  50. theorem OAI.Erdos3.polynomialIterDifference_C_mul line 633
  51. theorem OAI.Erdos3.zmod_mul_denominator_eq_zero_iff line 638
  52. theorem OAI.Erdos3.polynomialIterDifference_scaled_row_reduction line 646
  53. theorem OAI.Erdos3.polynomialIterDifference_scaled_row_probability line 656
  54. theorem OAI.Erdos3.zmod_polynomial_phase_bias_reduced_denominator line 681
  55. theorem OAI.Erdos3.zmod_polynomial_phase_bias_reduced_denominator_of_mul line 699
  56. theorem OAI.Erdos3.tagged_affine_phase_degree line 721
  57. theorem OAI.Erdos3.tagged_affine_phase_top_component line 737
  58. theorem OAI.Erdos3.zmod_tagged_affine_phase_bias_reduced_denominator line 760
  59. theorem OAI.Erdos3.pow_tag_killed line 792
  60. theorem OAI.Erdos3.pow_tag_top_factor line 802
  61. theorem OAI.Erdos3.zmod_primePower_tag_factors line 812
  62. theorem OAI.Erdos3.zmod_primePower_tagged_affine_phase_bias line 835
  63. theorem OAI.Erdos3.zmod_primePower_tagged_affine_phase_bias_at_modulus line 858
  64. def OAI.Erdos3.modularRankDecayExponent line 909
  65. def OAI.Erdos3.modularRankChargeFactor line 912
  66. def OAI.Erdos3.primePowerHomogeneousRankProbability line 914
  67. theorem OAI.Erdos3.norm_le_rpow_div_two_pow line 924
  68. theorem OAI.Erdos3.primePower_row_phase_decay_large line 937
  69. theorem OAI.Erdos3.primePower_polynomial_character_decay line 998
  70. theorem OAI.Erdos3.primePower_polynomial_image_characteristic_decay line 1037
  71. theorem OAI.Erdos3.totalDegree_map_le line 1076
  72. def OAI.Erdos3.integerPolynomialRankProbability line 1083
  73. theorem OAI.Erdos3.map_integerPolynomial_homogeneousComponent line 1093
  74. theorem OAI.Erdos3.primePowerHomogeneousRankProbability_integerPolynomial line 1104
  75. theorem OAI.Erdos3.primePower_crt_coprime line 1128
  76. theorem OAI.Erdos3.crt_integer_polynomial_characteristic_decay line 1134
  77. def OAI.Erdos3.crtPrimePowerPolynomialLaw line 1209
  78. def OAI.Erdos3.crtPrimePowerPolynomialMap line 1213
  79. def OAI.Erdos3.crtPolynomialCharge line 1221
  80. theorem OAI.Erdos3.crt_integer_polynomial_density_order_bounds line 1225
  81. theorem OAI.Erdos3.largestTestedBadDepth_not_bad line 1275
  82. theorem OAI.Erdos3.crtPolynomialCharge_le_of_bad_product line 1283