OAI/Combinatorics/Progressions/Fourier/QuarticBohrProgression.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.BohrProgression.indexedCyclicCharacter line 17
  2. lemma OAI.Erdos3.BohrProgression.indexedCyclicCharacter_zero line 21
  3. lemma OAI.Erdos3.BohrProgression.indexedCyclicCharacter_succ_mem line 24
  4. def OAI.Erdos3.BohrProgression.bohrLatticeMatrixInt line 30
  5. def OAI.Erdos3.BohrProgression.bohrLatticeMatrix line 35
  6. lemma OAI.Erdos3.BohrProgression.bohrLatticeMatrixInt_zero_succ line 39
  7. lemma OAI.Erdos3.BohrProgression.bohrLatticeMatrix_zero_zero line 44
  8. lemma OAI.Erdos3.BohrProgression.bohrLatticeMatrix_zero_succ line 49
  9. lemma OAI.Erdos3.BohrProgression.bohrLatticeMatrix_succ_succ line 54
  10. lemma OAI.Erdos3.BohrProgression.det_bohrLatticeMatrix line 60
  11. lemma OAI.Erdos3.BohrProgression.det_bohrLatticeMatrix_ne_zero line 74
  12. def OAI.Erdos3.BohrProgression.bohrLatticeBasis line 80
  13. lemma OAI.Erdos3.BohrProgression.bohrLatticeBasis_apply line 87
  14. def OAI.Erdos3.BohrProgression.bohrLatticePoint line 94
  15. lemma OAI.Erdos3.BohrProgression.intCastVec_bohrLatticePoint line 98
  16. lemma OAI.Erdos3.BohrProgression.bohrLatticePoint_zero line 106
  17. lemma OAI.Erdos3.BohrProgression.bohrLatticePoint_cast_coordinate line 113
  18. structure OAI.Erdos3.BohrProgression.CyclicCenteredGAP line 129
  19. abbrev OAI.Erdos3.BohrProgression.CyclicCenteredGAP.Param line 136
  20. def OAI.Erdos3.BohrProgression.CyclicCenteredGAP.coeff line 139
  21. def OAI.Erdos3.BohrProgression.CyclicCenteredGAP.eval line 142
  22. def OAI.Erdos3.BohrProgression.CyclicCenteredGAP.carrier line 145
  23. def OAI.Erdos3.BohrProgression.CyclicCenteredGAP.Proper line 148
  24. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.card_carrier_of_proper line 151
  25. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.coeff_abs_le line 157
  26. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.coeff_sub_abs_le_two_mul line 166
  27. def OAI.Erdos3.BohrProgression.bohrSuccessiveCertificate line 178
  28. def OAI.Erdos3.BohrProgression.bohrCertificateCoeff line 190
  29. lemma OAI.Erdos3.BohrProgression.bohrCertificateCoeff_spec line 197
  30. def OAI.Erdos3.BohrProgression.bohrCertificatePoint line 207
  31. lemma OAI.Erdos3.BohrProgression.intCastVec_bohrCertificatePoint line 212
  32. lemma OAI.Erdos3.BohrProgression.bohrCertificatePoint_independent line 226
  33. lemma OAI.Erdos3.BohrProgression.bohrCertificate_scale_pos line 233
  34. def OAI.Erdos3.BohrProgression.bohrProgressionRadius line 251
  35. def OAI.Erdos3.BohrProgression.bohrCyclicProgression line 257
  36. lemma OAI.Erdos3.BohrProgression.bohrProgressionRadius_mul_scale_le line 264
  37. lemma OAI.Erdos3.BohrProgression.abs_intCast_bohrCertificatePoint_le line 285
  38. def OAI.Erdos3.BohrProgression.bohrCertificateCombination line 301
  39. lemma OAI.Erdos3.BohrProgression.bohrCertificateCombination_cast_coordinate line 306
  40. lemma OAI.Erdos3.BohrProgression.abs_intCast_bohrCertificateCombination_le line 324
  41. lemma OAI.Erdos3.BohrProgression.eval_bohrCyclicProgression line 375
  42. lemma OAI.Erdos3.BohrProgression.int_eq_zero_of_cast_zmod_eq_zero_of_abs_lt line 387
  43. theorem OAI.Erdos3.BohrProgression.bohrCyclicProgression_proper line 401
  44. lemma OAI.Erdos3.BohrProgression.matrixOf_bohrLatticeBasis line 460
  45. lemma OAI.Erdos3.BohrProgression.abs_det_matrixOf_bohrLatticeBasis line 468
  46. lemma OAI.Erdos3.BohrProgression.inv_scale_le_two_mul_bohrProgressionRadius_add_one line 476
  47. theorem OAI.Erdos3.BohrProgression.bohrCyclicProgression_card_lower_bound line 493
  48. theorem OAI.Erdos3.BohrProgression.bohrCyclicProgression_carrier_subset line 588
  49. theorem OAI.Erdos3.BohrProgression.exists_proper_progression_subset line 622
  50. lemma OAI.Erdos3.BohrProgression.minkowskiSecondConstant_le_exp line 666
  51. lemma OAI.Erdos3.BohrProgression.progression_size_factor_lower_bound line 684
  52. theorem OAI.Erdos3.BohrProgression.exists_large_proper_progression line 727
  53. def OAI.Erdos3.BohrProgression.CyclicCenteredGAP.zero line 755
  54. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.zero_proper line 760
  55. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.zero_carrier line 765
  56. theorem OAI.Erdos3.BohrProgression.exists_large_proper_progression_all line 775
  57. theorem OAI.Erdos3.BohrProgression.exists_proper_progression_of_quartic_bounds line 799