OAI/Combinatorics/Progressions/Fourier/BohrNiltestBudget.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalTorus.Algebra line 18
  2. instance OAI.Erdos3.RationalTorus.(instance at line 20) line 20
  3. instance OAI.Erdos3.RationalTorus.(instance at line 23) line 23
  4. instance OAI.Erdos3.RationalTorus.(instance at line 26) line 26
  5. instance OAI.Erdos3.RationalTorus.(instance at line 34) line 34
  6. theorem OAI.Erdos3.RationalTorus.lie_eq_zero line 40
  7. def OAI.Erdos3.RationalTorus.basis line 42
  8. theorem OAI.Erdos3.RationalTorus.basis_repr line 46
  9. theorem OAI.Erdos3.RationalTorus.basis_equivFun line 50
  10. theorem OAI.Erdos3.RationalTorus.basis_equivFun_symm line 54
  11. def OAI.Erdos3.RationalTorus.filtration line 59
  12. theorem OAI.Erdos3.RationalTorus.basis_layers line 74
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_step_one_character line 91
  14. def OAI.Erdos3.RationalTorus.lattice line 125
  15. theorem OAI.Erdos3.RationalTorus.lattice_coordinates line 145
  16. theorem OAI.Erdos3.RationalTorus.lattice_inner_grid line 151
  17. theorem OAI.Erdos3.RationalTorus.lattice_outer_grid line 157
  18. def OAI.Erdos3.RationalTorus.nilmanifold line 163
  19. theorem OAI.Erdos3.RationalTorus.nilmanifold_geometry line 167
  20. instance OAI.Erdos3.RationalTorus.instRealTopology line 185
  21. instance OAI.Erdos3.RationalTorus.instRealTopologicalAddGroup line 188
  22. instance OAI.Erdos3.RationalTorus.instRealContinuousSMul line 191
  23. instance OAI.Erdos3.RationalTorus.instRealT2Space line 194
  24. def OAI.Erdos3.RationalTorus.phaseCoordinates line 207
  25. theorem OAI.Erdos3.RationalTorus.phaseCoordinates_one line 211
  26. theorem OAI.Erdos3.RationalTorus.phaseCoordinates_mul line 216
  27. theorem OAI.Erdos3.RationalTorus.phaseCoordinates_inv line 222
  28. theorem OAI.Erdos3.RationalTorus.phaseCoordinates_lattice line 227
  29. def OAI.Erdos3.RationalTorus.phaseProjection line 241
  30. theorem OAI.Erdos3.RationalTorus.phaseProjection_mk line 249
  31. abbrev OAI.Erdos3.RationalTorus.BottomQuotient line 263
  32. theorem OAI.Erdos3.RationalTorus.exists_bottom_quotient_character line 265
  33. theorem OAI.Erdos3.CircleFourier.real_phase_map_lipschitz line 342
  34. theorem OAI.Erdos3.RationalTorus.phaseCoordinates_lipschitz line 367
  35. theorem OAI.Erdos3.RationalTorus.phaseProjection_lipschitz line 392
  36. def OAI.Erdos3.torusPhaseLinear line 420
  37. theorem OAI.Erdos3.torusPhaseLinear_tmul line 424
  38. theorem OAI.Erdos3.torusPhaseLinear_mul line 434
  39. theorem OAI.Erdos3.torusPhaseLinear_inv line 443
  40. theorem OAI.Erdos3.torusPhase_lattice_map line 450
  41. def OAI.Erdos3.nativeTorusProjection line 457
  42. theorem OAI.Erdos3.nativeTorusProjection_mk line 461
  43. def OAI.Erdos3.nativeTorusLocalLift line 465
  44. theorem OAI.Erdos3.nativeTorusLocalLift_mk line 468
  45. theorem OAI.Erdos3.torusPhaseLinear_eq_of_small line 475
  46. theorem OAI.Erdos3.nativeTorusProjection_lipschitz line 485
  47. theorem OAI.Erdos3.nativeTorusLocalLift_lipschitzOn line 503
  48. def OAI.Erdos3.RationalTorus.affineOrbit line 530
  49. theorem OAI.Erdos3.RationalTorus.affineOrbit_coordinates line 536
  50. theorem OAI.Erdos3.RationalTorus.affineOrbit_phases line 545
  51. def OAI.Erdos3.RationalTorus.affineNiltest line 561
  52. theorem OAI.Erdos3.RationalTorus.affineNiltest_eval line 571
  53. theorem OAI.Erdos3.RationalTorus.affineNiltest_evalCyclic line 579
  54. theorem OAI.Erdos3.RationalTorus.affineNiltest_complexity line 585
  55. theorem OAI.Erdos3.exists_cyclic_character_niltest line 601
  56. theorem OAI.Erdos3.torus_reindex_lipschitz line 641
  57. def OAI.Erdos3.RationalTorus.reindexedRealObservable line 657
  58. theorem OAI.Erdos3.RationalTorus.reindexedRealObservable_norm line 661
  59. theorem OAI.Erdos3.RationalTorus.reindexedRealObservable_lipschitz line 667
  60. def OAI.Erdos3.RationalTorus.realAffineNiltest line 678
  61. theorem OAI.Erdos3.RationalTorus.realAffineNiltest_unitInterval line 683
  62. theorem OAI.Erdos3.RationalTorus.realAffineNiltest_evalCyclic line 690
  63. theorem OAI.Erdos3.RationalTorus.realAffineNiltest_complexity line 697
  64. def OAI.Erdos3.CyclicBohr.Set.approximationLipBound line 716
  65. def OAI.Erdos3.CyclicBohr.Set.approximationComplexity line 719
  66. theorem OAI.Erdos3.CyclicBohr.Set.approximationComplexity_nonneg line 722
  67. theorem OAI.Erdos3.CyclicBohr.Set.exists_upperApprox_niltest line 726
  68. theorem OAI.Erdos3.CyclicBohr.Set.exists_lowerApprox_niltest line 757
  69. theorem OAI.Erdos3.CyclicBohr.Set.upperApprox_comparison_of_niltests line 800
  70. theorem OAI.Erdos3.CyclicBohr.Set.average_sub_le_of_niltest_comparison line 810
  71. theorem OAI.Erdos3.CyclicBohr.Set.sum_average_sub_le_of_niltest_comparison line 822
  72. theorem OAI.Erdos3.CyclicBohr.Set.small_sum_average_of_niltest_comparison line 834
  73. theorem OAI.Erdos3.CyclicBohr.Set.coe_approximationLipBound line 859
  74. theorem OAI.Erdos3.CyclicBohr.Set.approximationComplexity_exp_le line 867
  75. theorem OAI.Erdos3.CyclicBohr.Set.card_ratio_ge_exp_width line 902
  76. theorem OAI.Erdos3.CyclicBohr.Set.small_sum_average_of_exponential_niltest_comparison line 922