OAI/Combinatorics/SumProduct/Alignment/PolynomialWeyl01.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalFactorPeriods.orderedWord_mem line 22
  2. lemma OAI.RationalFactorPeriods.orderedWord_character line 34
  3. lemma OAI.RationalFactorPeriods.List.prod_finRange_castSucc line 41
  4. lemma OAI.RationalFactorPeriods.word_eq_orderedWord line 47
  5. lemma OAI.NilpotentTaylor.word_zero line 69
  6. lemma OAI.NilpotentTaylor.choose_one_high line 74
  7. lemma OAI.NilpotentTaylor.word_one line 77
  8. lemma OAI.NilpotentTaylor.word_tail_two line 84
  9. theorem OAI.NilpotentTaylor.normalized_taylor line 97
  10. theorem OAI.NilpotentTaylor.normalized_subgroup_taylor line 119
  11. def OAI.PolynomialWeyl.mean line 157
  12. def OAI.PolynomialWeyl.derivative line 159
  13. theorem OAI.PolynomialWeyl.norm_mean_le_one line 162
  14. theorem OAI.PolynomialWeyl.norm_derivative_le_one line 170
  15. theorem OAI.PolynomialWeyl.norm_mean_shift_sub_le line 179
  16. theorem OAI.PolynomialWeyl.norm_expect_sq_le line 212
  17. theorem OAI.PolynomialWeyl.shift_average_error line 223
  18. theorem OAI.PolynomialWeyl.norm_expect_sq_eq line 239
  19. theorem OAI.PolynomialWeyl.van_der_corput line 247
  20. theorem OAI.PolynomialWeyl.pow_le_pow_add_error line 294
  21. theorem OAI.PolynomialWeyl.expect_pow_two_pow_le line 311
  22. def OAI.PolynomialWeyl.differencedMean line 332
  23. theorem OAI.PolynomialWeyl.differencedMean_nonneg line 337
  24. theorem OAI.PolynomialWeyl.differencedMean_le_one line 344
  25. theorem OAI.PolynomialWeyl.iterated_van_der_corput line 357
  26. def OAI.PolynomialWeyl.phase line 398
  27. theorem OAI.PolynomialWeyl.norm_phase line 400
  28. theorem OAI.PolynomialWeyl.phase_add line 403
  29. theorem OAI.PolynomialWeyl.phase_neg line 406
  30. theorem OAI.PolynomialWeyl.phase_sub line 412
  31. theorem OAI.PolynomialWeyl.phase_nat_mul line 415
  32. def OAI.PolynomialWeyl.polynomialPhase line 422
  33. def OAI.PolynomialWeyl.polynomialDifference line 425
  34. theorem OAI.PolynomialWeyl.polynomialPhase_difference line 428
  35. theorem OAI.PolynomialWeyl.taylor_coeff_top line 435
  36. theorem OAI.PolynomialWeyl.polynomialDifference_degree line 447
  37. theorem OAI.PolynomialWeyl.taylor_coeff_below_top line 465
  38. theorem OAI.PolynomialWeyl.polynomialDifference_coeff line 478
  39. def OAI.PolynomialWeyl.linearBound line 486
  40. theorem OAI.PolynomialWeyl.norm_linear_mean_le line 489
  41. def OAI.PolynomialWeyl.weylBound line 519
  42. theorem OAI.PolynomialWeyl.differencedMean_polynomial_le line 524
  43. theorem OAI.PolynomialWeyl.polynomial_weyl_inequality line 547
  44. theorem OAI.PolynomialWeyl.phase_int line 554
  45. theorem OAI.PolynomialWeyl.exists_int_close_of_phase line 563
  46. theorem OAI.PolynomialWeyl.linear_inverse line 591